Documents‎ > ‎

Rationale

The design of Ghilbert has evolved over many years. Some of the design decisions may seem odd, but every aspect has been thought through carefully. That's not to say that it can't be further improved - in particular, it seems plausible that the definition mechanism may be made more powerful. In any case, this document tries to set out the reasoning behind some of those decisions.

S-expressions

Most theorem proving environments choose a syntax which is some form of compromise between standard, readable mathematical syntax and an unambiguous representation easy to parse and suitable to formal manipulation. Metamath, in particular, uses a very clever syntax where terms are a sequence of tokens, each with both an ASCII representation (easy to type) and a graphic representation (both a GIF image and a Unicode string). The resulting expressions are fairly readable, even to one without exposure to Metamath. Most expressions are infix, and the overall grammar is carefully constructed to be unambiguous.

Yet, Metamath's approach to syntax has some problems. In particular, it's very brittle with respect to extension. Certain forms which would be unproblematic in ordinary mathematics (like postfix ! for factorial) would, in fact, cause the Metamath grammar to become ambigous. Since there's no automatic checking of this, it's possible to introduce unsoundness into the system simply by introducing richer syntax.

Ghilbert's approach is to use the simplest possible representation of terms. S-expressions are nearly trivial to parse, clearly unambiguous, and extensible without limit. They're somewhat familiar and readable to people with a computer science background (especially programmers with LISP experience), but admittedly don't look much like real math.

But the intent is not for people to spend a lot of time with S-expressions (even though that is what I'm doing now). Rather, tools should take care to present the underlying concepts using the most beautiful and familiar mathematical typesetting available. My early experiements (see this PDF of a snapshot of set.mm) are very encouraging. In particular, such an approach lets you use precedence rules to get rid of a great many parentheses.

ASCII

Another difficult decision was whether to restrict names to ASCII or to allow Unicode. Ultimately, I went with ASCII for a number of reasons.
[...]


Comments