30 Mar 2003 raph   » (Master)


The last couple of weeks have been really hard on my productivity. I feel like I've been getting behind on a bunch of things, including design and coding work on Fitz, the IJS 1.0 spec, a command-line version of the trust metric, and other things.

I'm feeling a bit more productive now and hope to catch up over the next few weeks.


During times of stress, I find it comforting to muse on proofs. The idea of mathematical certainty, is soothing to me.

Much of my thinking is directed towards a scheme for portable and modular proofs. For one, there are many different axiom systems, of various strengths. Most proof systems simply choose one. The problem with this is that proofs can be ported to a system with a stronger axiom system, but not in general to a weaker one.

Further, if you have a minimalist set of axioms (such as second order arithmetic or Zermelo-Fraenkel set theory), then you want to construct a rich library of objects (many flavors of numbers, sequences, functions, etc.) on top of it. In many cases, there will be more than one viable construction (for example, reals can be infinite binary expansions, Dedekind cuts, or the Harrison's clever HOL construction). Proofs shouldn't depend on the details of the construction used. A proof over the reals should go through exactly the same no matter which construction of the reals undergirds it.

So I've been thinking along the ideas of modules and interfaces. The axioms of complex arithmetic would be one example of an interface. A proof over complex numbers imports this interface. A module representing a construction of complex numbers would import the HOL primitive axiom interface and export the complex number interface.

Each module can be checked individually, to make sure that the exports are justified in terms of the imports. Then, you can check a whole pile of modules, by instantiating the abstract interfaces in each "import" and "export" with concrete replacements. For example, the abstract addition function is replaced with a definition appropriate to the chosen construction. The whole thing checks if each import (after instantiation) is satisfied by a matching export (again, after instantiation) from a previous module (ie, no import cycles allowed).

Thus, you could fairly easily check a proof over complex numbers in any one of the axiom schemes powerful enough to represent them. Just supply the construction appropriate to the primitive axioms.

Not all proofs will check in all axiom systems, of course. In general, a proof module should be conservative in what it imports, so that it will check in the largest range of axiom systems. This principle also ensures that proofs can be ported to the widest range of other systems.

I hope to write about these ideas in more detail, including why it's important. It's obvious to me, but other people seem to need convincing. That sounds quite a bit like Ivan Sutherland's recipe for successful research: do something you think is easy, but everybody else thinks is hard.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!