Ars Mathematica

This is a test post to see what’s involved in uploading images.

This is of course the Sierpinski carpet. What’s interesting to me is that many objects that, in a previous age dominated by a picture of the physical world as a continuum, seemed deeply pathological, have straightforward computer-language descriptions. For example, you can check whether or not a point in the plane is on the Sierpinksi plane by looking at the ternary expansion of its coordinates, which is a couple of lines of computer code. From the point of view of the computer, the Sierpinksi carpet is not much more complicated than a parabola. I suspect that the popularity of fractals marks a change in the popular imagination of the dominant metaphor for mathematics, from mathematics as mechanics to mathematics as computer program.

While thin on details, I found the article A new efficient algorithm for computing Gröbner basis intriguing. While a naive implementation of Gröbner bases is easy to come by, as a practical algorithm it is highly sensitive to the order in which you add new polynomials to the basis. This has given rise to a whole literature on strategies to add new polynomials. In the paper, Faugere seems to suggest that the whole question can be bypassed, and that polynomials can be added to the basis in bulk by using sparse linear algebra techniques.

This is more of a computer programming post than a math post, but since we all use TeX, I thought it might be of general interest. I came across this paper by Heckman and Wilhelm, which describes how to implement TeX’s algorithm for typesetting math formulas in a functional language (namely, ML). We see the output of this algorithm every time we look at a math paper, but until now it lacked a precise formal description other than what was embedded Knuth’s Pascal code. Since Knuth wrote TeX back when computers were much slower and compilers were much dumber, the code contains many hand optimizations that make the logic hard to follow. (The algorithm itself is too complicated to lend itself to a purely verbal description.) By rewriting it in a functional language, the authors are able to turn the algorithm into a well-defined mathematical function.

The BHK interpretation of intuitionistic logic articulates the sense in which intuitionistic logic captures constructive reasoning. Statements that involve logical connectives are interpreted as constructions that transform proofs of simpler statements into proofs of more complicated statements. The interpretation requires a primitive notion of what it means to give a construction function that turn objects and proofs into another proof.

Generally, the BHK interpretation is invoked as a piece of metamathematical reasoning, with the actual definition of a constructive function left to the particular theory under development. This puzzled me, since there is a natural notion of construction: one given by an arbitrary Turing machine. At first, I chalked it up to a philosophical unwillingness to accept the Church-Turing thesis, but I think I’ve identified the real problem: it doesn’t work.

For the BHK interpretation to work, Turing machines that represent constructions must be total functions. Worse, to satisfy the philosophical aim of constructivism, they must be provably total in a constructive system. But a simple diagonal argument shows that there exists total functions that are not provably total in any constructive system since we would expect the valid proofs in such a system to be recursively enumerable. You can simply identify constructions with those provably total in a specific system, but philosophically the diagonal argument is constructively valid: given any recursively enumerable axiomatization of valid constructions, I can give you an explicit construction that is different from every element of that enumeration, and for any given element an explicit proof that it’s different.

The way this issue is handled in the realizability interpretation (and therefore the effective topos) is by identifying the constructions as those functions that are provably total in Heyting arithmetic, the intuitionistic analogue of Peano arithmetic.

As we all know, crime on the internet knows no national boundaries, as Scott Aaronson has learned. Australian fashion models have taken to stealing the contents of his quantum mechanics lectures in order to sell printers. Mark my words, next they’ll be using quantum mechanics to rob banks and assassinate major world leaders.

Sorry for the radio silence; I’ve been under the weather lately.

Is there any major theorem in mathematics drier than Gentzen’s cut elimination theorem. I feel guilty for picking on proof theory, since it is an undeservedly unfashionable area of mathematics (it’s probably better known by computer scientists than mathematicians at this point). I feel guilty for picking on the cut elimination theorem in particular, since it’s an important ingredient in the proof that Goodstein’s theorem is independent of Peano arithmetic, which is one of my favorite theorems. But, I had to read the statement of the theorem forty-nine times before I got what it was trying to say. I have yet to make it all the way through the proof before blacking out.

I was trying to think of a theorem in a more-fashionable area of mathematics that is particularly dry. The best I could come up with the Riemann-Roch theorem (for curves). I know what it says. I know what it’s good for. I just can’t bring myself to like it.

A new revision of the standard for the Scheme programming language, the Revised⁶ Report on the Algorithmic Language Scheme, has been approved. The draft standard and other information can be found at r6rs.org.

The changes seem to be aimed at enhancing portability between implementations of Scheme. Opinions, both pro and con, can be gleaned from the online ratification process.

I just discovered a shocking lacuna in my linking strategy. I have never linked to the acknowledgements page for the Scheme shell reference manual. If you ever write a book, this is the only appropriate model to follow.

Does anyone understand the claim being made here in this New York Times article? There is some sense in which the creators of the Chinook checkers-playing program have shown that Chinook cannot ever lose at checkers, but the article includes the caveat:

Even with the advances in computers over the past two decades, it is still impossible, in practical terms, to compute moves for all 500 billion billion board positions. Instead, the researchers took the usual starting position and then looked only at the positions that would occur during the normal course of play.

Do they mean that from the normal starting position that Chinook cannot lose? Or does checkers have stylized openings the way chess does, and they mean that Chinook cannot lose from any of those openings?

I neglected to put up a post about the first issue of the Bulletin of the AMS for 2007. Here’s some of the highlights:

• K. Soundararajan describes a recent result of Goldston, Pintz, and Yildirim on gaps between primes. The article provides a taste of what analytic number theory is like.
• Jaikumar Radhakrishnan and Madhu Sudan provide an introduction to Dinur’s proof of the PCP theorem. The PCP theorem, one of the most surprising complexity theory results of the last twenty years. Dinur’s proof is not the original, but provides a new approach to the topic.
• Svetlana Katok and Ilie Ugarcovici explain the relationship between symbolic dynamics and differential geometry. Symbolic dynamics fits perfectly in the computer era, so it always seemed bizarre to me that it was invented purely as a technique in differential geometry.

Now to write up the second issue before the third issue comes out…