Alfa is a WYSIWYG proof editor. It allows you to, interactively
and incrementally, define theories (axioms and inference rules),
formulate theorems and construct proofs of the theorems. All steps in
the proof construction are immediately checked by the system and no
erroneous proofs can be constructed. The logical framework used is one
of Thierry Coquand's versions of Per Martin-Löf's Type Theory.
Alternatively, you can view Alfa as a syntax-directed editor for a
small purely functional programming language with a type system that
provides dependent types. The editor immediately checks that
programs you enter are syntactically correct and type correct.
Alfa is largely inspired by Window-Alf [AGNvS94], implemented
by Lena Magnusson and Johan Nordlander, and has a
similar user interface.
The plan is that Alfa should improve on Window-Alf by
- allowing the user to define how proof terms should be
presented on the screen (and on paper). This includes simple
things like argument hiding and infix operators, but also more
advanced mathematical notation and natural deduction style proof
trees and other representations of proofs. Alfa should also
allow you to produce documents where explanatory text and proof
fragments are interleaved.
- using ideas from hypertext and Web browser to allow the user to
efficiently navigate through large proofs and libraries.
Some of this has been implemented. As shown in Figure 90,
proofs can be presented in natural deduction style. Figure 90. Window dump of Alfa, illustrating the construction
of a simple proof in natural deduction style.
Whereas Window-Alf was implemented in Standard ML (proof engine)
and C++ & Interviews (user interface), Alfa is implemented entirely in
Haskell, using Fudgets for the user interface. At the time of
writing, the source code
consists of about 8000 lines, distributed as
follows:
- The proof engine by Thierry Coquand. 2700 lines. This includes a parser and parser combinators (480 lines).
- Extensions and improvements of the Fudget library. 1900 lines. The largest part of this is the new fudgets for displaying
structured graphics (described in Chapter 27) and
syntax-directed editing. It also includes a new file-selection
window and a string-entry window with immediate syntax
checking and feedback via a smiley (see
Figure 91). Although the development of these were
prompted the Alfa project, they are general enough to be used
in other contexts.
Figure 91. The smiley indicates whether there is a
syntactic error in the input.
- The Alfa User Interface. 3400 lines. The largest parts are
the implementation of the WYSIWYG style editing operations (1000
lines) and the code for drawing/building abstract syntax trees
used by the syntax-directed editor fudget (800 lines).
In addition, Aarne Ranta has supplied 2100 lines with support for
natural language. Some of this code had been integrated in Alfa,
but this work was in a rather experimental stage.
More detailed and up-to-date information on Alfa is available on
the WWW [Hal97].
