In their book (see here), Harold and Andrea begin with a program POLY: steps for a turtle tracing polygons on the plane. A polygon is a closed path: we can see that clearly from outside, but how does a turtle know its path is closed from inside, without measuring its coordinates ? They discuss this in detail, leading to:
- Closed Path Theorem: the total turning along any closed path in the plane is an integer multiple of 360°. That integer is called the winding number of the closed path.
- Simple Closed Path Theorem: a simple closed path, which is non-crossing, in the plane has winding number ±1.
- Whitney-Graustein Theorem: two closed paths in the plane can be deformed into one another if and only if they have the same winding number.
They proved the first, gave a detail sketch of the second, and showed only half of the third — all using elementary topology. As an application of these ideas, they put a stop condition for POLY (so turtle really knows its path is closed), worked out the symmetry of the polygon from the input parameters of POLY, and taught the turtle to escape a fair maze via Pledge algorithm.
Then they let the turtle wander on the sphere, a curved surface that can still be visualized. The turtle will find that Closed Path Theorem breaks down. They showed skillfully how the theorem can be restored, by introducing an intrinsic turning that serves to measeure curvature. The whole discussion makes use of elementary topology of surfaces.
Of course, they let the turtle wander on the torus, the Möbius strip, even Klein’s bottle — leading to this result:
- Gauss-Bonnet Theorem – for any closed surface, the total curvature K and Euler characteristic χ are related by K = 2πχ.
Eventually they let the turtle wander in Einstein’s curved spacetime – a curved 3D (simplify to 2D space + time) that can only be viewed from inside. It’s amazing that they can talked about differential geometry and Lorentz transform using only diagrams!
For my project, I plan to follow the book’s approach, with the following:
- Formalize topology of closed path, hence proving Whitney-Graustein Theorem
- Formalize topology of closed surfaces, hence proving Gauss-Bonnet Theorem
Pledge algorithm of solving maze can be formally verified as a result. I am not sure if its recreational use is of any benefit in serious research.