27 October 2021
Embedding Tarski in GeoGebra delivers
discovery of geometric inequalities on the web
After a couple of weeks of work I am happy to announce that GeoGebra is now
able to discover geometric inequalities in its web version. In this blog entry you can try it on your own.
Please follow these steps:
-
Click on the 5. toolset in the Toolbar and select the first tool (Polygon
).
- Draw a triangle in the Graphics area (on the right) by creating three points, and then click on the first point again.
-
Click on the last, empty line in the Algebra view (on the left) and type Relation(a+b,c) and press ENTER.
-
GeoGebra will inform you that \(a+b\) and \(c\) differ. But by clicking on the More... button
some further computation will start. In a couple of seconds you will obtain the triangle inequality.
-
Finally you can safely close the popup window by clicking OK.
Technical background
The computations are performed here by the web version of
Tarski,
a program that is able to symbolically solve
systems of inequalities, and allowing quantifiers as well.
Compilation of Tarski for the web was not completely straightforward. The first steps were described
in my blog. Additionally, Tarski had to be compiled as a JS module by using
the linker flags
SINGLE_FILE,
MODULARIZE and a unique
EXPORT_NAME had to be given.
The first flag helped in embedding the .wasm object in the .js file to simplify inclusion of the WebAssembly code
in a webpage. The second and third flags allowed that Tarski did not conflict with another WebAssembly module:
in GeoGebra we already use Giac in the same way.
Loading Tarski for the web can be performed with the following JS code:
Tarski().then(function(Module) {
var numcells = 50000000;
var timeout = 5;
TARSKIINIT = Module.cwrap("TARSKIINIT", 'void', ['number', 'number']);
TARSKIEVAL = Module.cwrap("TARSKIEVAL", "string", ["string"]);
TARSKIEND = Module.cwrap("TARSKIEND", "void", []);
TARSKIINIT(numcells, timeout);
});
Using an embedded version of Tarski is beneficial also for the desktop version. It does not require the
external
realgeom application any longer. Now the
important parts of realgeom are
embedded in GeoGebra Discovery.
This accelerates the startup of GeoGebra Discovery a lot! If you are interested, you can give
the
new desktop version a try by downloading it.
Embedding Tarski into the desktop version was more or less smooth. Here the only challenge was
to carefully communicate with
SWIG that Tarski will be a
package and not a standalone application.
Further experiments
Speed issues
The examples provided above are all managable and stable. Of course, there are many examples that
are more challenging or even infeasible to compute. Here I focus on another example, namely
Bottema's theorem 5.3 (published in the book Geometric Inequalities, 1968,
co-authored with Djordjevic, Janic, Mitrinovic and Vasic). It is about comparing the
perimeter \(a+b+c\) and the circumradius \(R\) of an arbitrary triangle. One can show that
\[a+b+c\le3\sqrt3\cdot R\] for all triangles.
It turns out that different geometric realizations may lead to different computations
with different difficulties. To define the radius one needs to create the circumcenter first,
and then one of the three vertices must be chosen to designate the circumradius, but this choice
is actually free: it depends on the user. But the computational complexity depends a lot on
the user's decision!
For example, we can learn that connecting the circumcenter
with point A is the preferred method, and choosing the perpendicular bisectors for sides b
and c results in the fastest computation. Other choices (like A plus a and b
or b plus a and b) will, in our tests, usually result in twice slower
computations, or, what is even worse (like selecting C or a and b),
the computation may take lots of minutes or even hours...
What does this mean in numbers? We focus on the fastest method, that is, we choose to designate R by connecting
A and the circumcenter which will be defined as the intersection of perpendicular bisectors
for sides b and c. We compared the timings on four platforms.
First, a Linux system was tried with a CPU Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz. Here the timing was 631
milliseconds on the desktop version of GeoGebra Discovery, not bad.
The same test in Google Chrome 95.0.4638.54 gave 6886 ms, almost ten times slower
than in the desktop version. In Firefox 93.0 the timing was 21842 ms: another three times slower. This is
clearly not acceptable any longer in a classroom situation.
For the web platforms we started some further experiments. Web browser improvements promise the
nearby implementation of
C++ exceptions
that are programmed now by using various hacks in JavaScript.
By using the experimental feature
wasm-exceptions (and recompiling Tarski accordingly) we can speed up
the computation to get 4266 ms in Google Chrome 95 and to get 15924 ms in Firefox Nightly 95.0a1 (2021-10-24).
So we can spare quite a lot of time! But still, there is some bottleneck somewhere, because the
web version is still much behind the desktop version in performance.
Entries on topic GeoGebra
- I restart my blog… (28 September 2020)
- A new GeoGebra version with better angle bisectors… (29 September 2020)
- Better language support… (6 October 2020)
- Detection of perpendicular lines… (19 October 2020)
- Points attached to an algebraic curve… (31 October 2020)
- Explore envelopes easily! (11 November 2020)
- Offsets of a trifolium (17 November 2020)
- Ellipsograph of Archimedes as a simple LEGO construction (18 November 2020)
- Pete-Dőtsch theorem (29 December 2020)
- Comparison improvements (25 January 2021)
- ApplyMap (26 January 2021)
- Discovering geometric inequalities (27 October 2021)
- Proving inequalities (28 October 2021)
- Supporting logic in function calculus (2 November 2021)
- Supporting logic with technology: Part 2 (12 February 2022)
- Difficulty of geometry statements (30 July 2024)
|
Zoltán Kovács
Linz School of Education
Johannes Kepler University
Altenberger Strasse 69
A-4040 Linz
|