27 October 2021

Embedding Tarski in GeoGebra deliversdiscovery 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.

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:
• Compare $$a^2+b^2$$ and $$c^2$$ in an arbitrary triangle. The Pythagorean theorem states equality here, but only for right triangles. Is there a generalization?
• Draw a regular pentagon and compare one of its diagonals to one of the sides. Can you get the golden ratio in its exact form? To achieve this, please follow these steps:
1. Click on the 5. toolset in the Toolbar and select the second tool (Regular Polygon ).
2. Draw a regular pentagon by selecting two points to designate one side. You will obtain the pentagon ABCDE.
3. Connect vertices A and C by selecting the 3. toolset in the Toolbar and the 3. tool in it (Segment ). This segment will be denoted as k.
4. Click on the 8. toolset in the Toolbar and select the 7. tool (Relation ).
5. Click on segment k and segment AB consecutively.
6. GeoGebra will inform you that k does not have the same length as f (here AB is automatically denoted by f). Now click on the More... button to obtain the expected result.
7. Finally you can safely close the popup window by clicking OK.

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.