Metamath
Bram pointed me to this thesis
on implementing real numbers within HOL. I heartily recommend this
thesis to people following this thread (if any). It's very interesting
to compare to Metamath's construction of the reals. Unfortunately,
these constructions are not compatible. One significant difference is
that Metamath seems to support partial functions, so 1/0 is not in the
range of the divide function, while HOL wants to have total functions
within the type, so 1/0 must have some value (Harrison chooses 0
to simpify the details). As such, proofs from one probably can't be
easily ported to the other without serious handwork.
I feel I understand Metamath
reasonably well now. It has some issues, but it's overwhelming
strength is that it's simple. For example, I believe that a
fully function proof verifier could be done in about 300 lines of
Python. I wonder how many lines of Python a corresponding verifier for
HOL would be; I'd guess around an order of magnitude larger. That kind
of difference has profound implications. Norm Megill is certainly to
be commended for the "simplicity engineering" he's put into Metamath.
For the purpose of putting doing Web-distributed proofs, Metamath has
a few shortcomings. I think they can be fixed, especially given the
underlying simplicity. I'll talk about these problems and possible
fixes over the next few days.
Definitions in Metamath have two closely related problems. Definitions
are introduced exactly the same way as axioms. As such, it's far from
obvious when a definition is "safe". For example, you could add
definitions for the untyped lambda calculus, which would introduce the
Russell set paradox. The second problem is that there is a single
namespace for newly defined constants. You wouldn't be able to combine
proofs from two different sources if they defined the same constant
two different ways.
Here's my proposal to fix these problems. Choose a highly restricted
subclass of definitions that is clearly safe. For example, you could
say that any definition of the form "newconst x y z = A" or "newconst
x y z <-> phi", with newconst not appearing in A or phi, is
acceptable. I propose to introduce new syntax that clearly identifies
such definitions. You could use existing syntax, so that such
definitions become axioms, but can be checked easily, or you could
have other syntax that sets the new constant apart from its "macro
expansion". That's a style preference.
Now let's talk about namespaces. I have a strong preference for using
hashes as global names, because (assuming the hash function is
strong), you don't get collisions. As such, it should be possible to
mix together arbitrary proofs without danger. Here's an outline
proposal.
Take the definition axiom, and replace the newly defined constant with
some token, say $_. Hash the result. That is the "global name". When
you're developing proofs, you'll probably want a (more or less)
human-readable "pet name", but this is actually irrelevant for
verification. Here's an example in Metamath notation.
Here's Metamath's definition of the empty set
$( Declare the symbol for the empty or null set. $)
$c (/) $. $( null set $)
$( Extend class notation to include the empty set. $)
c0 $a class (/) $.
$( Designate x as a set variable for use within the null set definition. $)
$v x $.
$f set x $.
$( Define the empty set. $)
dfnul2 $a |- (/) = { x | -. x = x } $.
So here's what gets hashed:
$a class $_ $. $f set x $. $a |- $_ = { x | -. x = x } $.
Take the SHA-1 hash of this string. Then I propose that
#274b1294a7d734a6e3badbf094190f46166159e4 can be used (as both a label
and a constant, as these namespaces are independent) whenever the
empty set is needed. A proof file would of course bind this string to
a shorter name, such as (/). When importing a proof file from another,
the binding would be local to the file. (Currently, Metamath has only
a file include facility similar to C's preprocessor #include, but an
import facility with better namespace management would be quite a
straightforward addition, especially considering that Metamath already
has ${ $} scoping syntax).
Obviously, there are some details to be worked out, particularly
nailing down exactly what gets hashed, but I think the idea is
sound.
Schooling
Alan's Mindstorms arrived a couple of days ago. These promise to be
quite fun (and of course educational :). So far, he's settling into
first grade very easily. We begin the half-homeschooling starting on
Monday.
Even so, I get the sense that Max is going to be the one most into
computers. He's learning the OS X interface impressively well. Last
time we resumed the computer, a folder was highlighted, and he said,
"it's clicked." Then, when I ran Stuffit to unpack a game demo, he
noted the icon and said, "it's squishing it." He's also the one that
said, "I love Alan's 'puter".