I spoke at TEDx University of Ljubljana. The topic was how programming influences various aspects of life. I showed the audence how a bit of simple programming can reveal the beauty of mathematics. Taking John Baez’s The Bauty of Roots as an inspiration, I drew a very large image (20000 by 17500 pixels) of all roots of all polynomials of degree at most 26 whose coefficients are $-1$ or $1$. That’s 268.435.452 polynomials and 6.979.321.752 roots. It is two degrees more than Sam Derbyshire’s image, so consider the race to be on! Who can give me 30 degrees?
A student of mine worked on a project to produce beautiful pictures of Costa’s minimal surface with the PovRay ray tracer. For this purpose she needed to triangulate the and compute normals to it at the vertices. It is not too hard to do the latter part, and the Internet offers several ways of doing it, but the normals are a bit tricky. If anyone can calculate them with paper and pencil I’d like to hear about it.
I went back to my undergraduate days when I actually did differential geometry and churned out the normals with Mathematica. It took a bit of work, kind advice from my colleague Pavle Saksida, and a pinch of black magic (to extract the Delaunay triangulation from Mathematica), so I thought I might as well publish the result at my GitHub costa-surface repository. The code is released into public domain. Have fun making pictures of Costa’s surface! Here is mine (deliberately non-fancy):
I spent a week trying to implement higher-order pattern unification. I looked at couple of PhD dissertations, talked to lots of smart people, and failed because the substitutions were just getting in the way all the time. So today we are going to bite the bullet and implement de Bruijn indices and explicit substitutions.
The code is available on Github in the repository andrejbauer/tt (the
I am on a roll. In the second post on how to implement dependent type theory we are going to:
- Spiff up the syntax by allowing more flexible syntax for bindings in functions and products.
- Keep track of source code locations so that we can report where the error has occurred.
- Perform normalization by evaluation.
I am spending a semester at the Institute for Advanced Study where we have a special year on Univalent foundations. We are doing all sorts of things, among others experimenting with type theories. We have got some real experts here who know type theory and Coq inside out, and much more, and they’re doing crazy things to Coq (I will report on them when they are done). In the meanwhile I have been thinking how one might implement dependent type theories with undecidable type checking. This is a tricky subject and I am certainly not the first one to think about it. Anyhow, if I want to experiment with type theories, I need a small prototype first. Today I will present a very minimal one, and build on it in future posts.
Make a guess, how many lines of code does it take to implement a dependent type theory with universes, dependent products, a parser, lexer, pretty-printer, and a toplevel which uses line-editing when available?