1 Mar 2004 raph   » (Master)


CodeCon was great fun, and I'm really glad I went. The highlight was the Google party. How good was that? Let's put it this way: I was so absorbed with intense conversations that I completely missed Knuth crashing it.


elanthis: yes, IMHO of course. I've got one more in the pipeline, and very possibly some more coming.


Ghilbert was cited in a recent preprint by Carlos T. Simpson. One of the central themes of this paper is a preference for untyped, set-theory flavored math as opposed to the more type-flavored variety you see in systems such as HOL, NuPRL, and Coq. He's also not a big fan of the constructive flavor of the latter two systems (meaning that x || !x is not an axiom).

The main thing I'm doing in Ghilbert now is constructing HOL in set theory. It's slow and steady progress, and very satisfying. One issue I'm running into, though, is HOL's epsilon operator. Essentially, if f is a function from some type T to bool, then epsilon(f) chooses a value (of type T) for which f is true. This construction is very useful, but does pose some challenges.

In the special case where there is only one value for which f is true, there's no problem (in this case, the similar "iota" operator suffices). But it's not hard to come up with situations in which f might hold for infinitely many values, and choosing one out of the many is a problem. If you accept the Axiom of Choice, it tells you that it can be done, but it doesn't tell you which value to choose. So it doesn't provide much help for actually constructing HOL in set theory.

The HOL documentation adds further twists to the story. The HOL description document contains a paragraph (at the end of section 1.1) suggesting that the universe of HOL terms is actually a pretty small set (by the standards of set theory, anyway - it's still quite infinite), and that it should be possible to choose an element from any subset quite straightforwardly, even without assuming the axiom of choice. I am beginning to get a vague sense what they're talking about, but don't really understand it. If anyone out there reading could explain it to me, I'd really appreciate it. If not, I think I know who to ask.

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!