Re: equational proof checker for lambda calculus?

Klaus Ebbe Grue <grue@diku.dk> · Thu, 20 Nov 2003 10:51:48 +0100 (MET)

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

On Sat, 15 Nov 2003 jhines@haverford.edu wrote:

> Does there exist a simple proof checker for equational proofs
> with format something like this?
>
> ( (\x. (x x)) (\y. (y (\z. z))) )
> = beta-reduce
> ( (\x. (x (\y. y))) (\z. (z (\w. w))) )
> = beta-reduce
> ( (\x. (x (\y. y))) (\z. z) )
> = beta-reduce
> ( (\x. x) (\y.y) )
> = beta-expand
> ( (\x. (x x)) (\y.y) )

A system (with the preliminary name "Logiweb") that does just that is
currently used by first year students at Diku (Dept.comp.sci/Univ.Copenhagen).
A release for a broader audience is due for the beginning of next year, if
you can wait for that.

The format of the proof would be

L lemma A: ( (\x. (x x)) (\y. (y (\z. z))) ) = ( (\x. (x x)) (\y.y) )

L proof of A:
L1: Algebra > ( (\x. (x x)) (\y. (y (\z. z))) ) ;
L2: beta-reduce > ( (\x. (x (\y. y))) (\z. (z (\w. w))) ) ;
L3: beta-reduce > ( (\x. (x (\y. y))) (\z. z) ) ;
L4: beta-reduce > ( (\x. x) (\y.y) ) ;
L5: beta-reduce > ( (\x. (x x)) (\y.y) )

The lemma and proof may reside on different web pages so that the teacher
may formulate the lemma and the students may formulate the proof.

The editor is WYSIWYG, syntax directed, and one may choose to use e.g.
Greek letters instead of backslash and beta-reduce. TeX may be used for
making a high quality print.

Above, L is the name of a theory that allows beta-reduction and algebraic
proofs. The system also supports Hilbert style proofs. L1..L5 are optional
line numbers useful for referencing. Many parentheses could be omitted if
one tells the priority and associativity of the operators to the system.

For more, see http://www.diku.dk/~grue. In particular, see the
"Mathematics and Computation" entry and the "Logiweb" entry on that page.
The system itself will appear on that page when matured for external use.

Cheers,
Klaus Grue