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:
  1. Click on the 5. toolset in the Toolbar and select the first tool (Polygon ).
  2. Draw a triangle in the Graphics area (on the right) by creating three points, and then click on the first point again.
  3. Click on the last, empty line in the Algebra view (on the left) and type Relation(a+b,c) and press ENTER.
  4. 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.
  5. 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

At the moment, you can safely try the following examples:

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

  1. I restart my blog… (28 September 2020)
  2. A new GeoGebra version with better angle bisectors… (29 September 2020)
  3. Better language support… (6 October 2020)
  4. Detection of perpendicular lines… (19 October 2020)
  5. Points attached to an algebraic curve… (31 October 2020)
  6. Explore envelopes easily! (11 November 2020)
  7. Offsets of a trifolium (17 November 2020)
  8. Ellipsograph of Archimedes as a simple LEGO construction (18 November 2020)
  9. Pete-Dőtsch theorem (29 December 2020)
  10. Comparison improvements (25 January 2021)
  11. ApplyMap (26 January 2021)
  12. Discovering geometric inequalities (27 October 2021)
  13. Proving inequalities (28 October 2021)
  14. Supporting logic in function calculus (2 November 2021)
  15. Supporting logic with technology: Part 2 (12 February 2022)

Zoltán Kovács
Linz School of Education
Johannes Kepler University
Altenberger Strasse 69
A-4040 Linz