A practical lambda-calculator 2.2

A practical lambda-calculator is a normal-order evaluator for the untyped lambda-calculus, extended with convenient commands and shortcuts to make programming in it more productive.

Shortcuts are distinguished constants that represent terms. Commands define new shortcuts, activate tracing of all reductions, compare terms modulo alpha-conversion, print all defined shortcuts and evaluation flags, etc.

Terms to evaluate and commands are entered at a read-eval-print-loop (REPL) "prompt" or "included" from a file by a special command. A Haskell branch is an embedding of the lambda calculator (as a domain-specific language) into Haskell. The calculator can be used interactively within Hugs or GHCi.

The present calculator implements what seems to be an efficient and elegant algorithm of normal order reductions. The algorithm is "more functional" than the traditionally used approach.

The algorithm seems identical to that employed by yacc sans one critical difference. The calculator also takes a more "functional" approach to the hygiene of beta-substitutions, which is achieved by coloring of identifiers where absolutely necessary. This approach is "more functional" because it avoids a global counter or the threading of the paint bucket through the whole the process. The integration of the calculator with Haskell lets us store terms in variables and easily and intuitively combine them.

The traditional recipe for normal-order reductions includes an unpleasant phrase "cook until done". The phrase makes it necessary to keep track of reduction attempts, and implies an ugly iterative algorithm. Were proposing what seems to be an efficient and elegant technique that can be implemented through intuitive re-writing rules.

Our calculator, like yacc, possesses a stack and works by doing a sequence of shift and reduce steps. The only significant difference from yacc is that the lambda-calculator "reparses" the result after the successful reduce step. The source and the target languages of our "parser" (lambda-calculator) are the same; therefore, the parser can indeed apply itself.

The parsing stack can be made implicit. In that case, the algorithm can be used for normalization of typed lambda-terms in Twelf.

The following examples show that lambda-calculus becomes a domain-specific language embedded into Haskell:

> c0 = f ^ x ^ x -- Church numeral 0
> succ = c ^ f ^ x ^ f # (c # f # x) -- Successor

> c1 = eval $ succ # c0 -- pre-evaluate other numerals
> c2 = eval $ succ # c1
> c3 = eval $ succ # c2
> c4 = eval $ succ # c3

It is indeed convenient to store terms in Haskell variables and pre-evaluate (i.e., normalize) them. They are indeed terms. We can always ask the interpreter to show the term. For example, show c4 yields (f. (x. f (f (f (f x))))).

let mul = a ^ b ^ f ^ a # (b # f) -- multiplication
eval $ mul # c1 ---> (b. b), the identity function
eval $ mul # c0 ---> (b. (f. (x. x))), which is "const 0"

These are algebraic results: multiplying any number by zero always gives zero. We can see now how lambda-calculus can be useful for theorem proving, even over universally-quantified formulas.

The calculator implements Dr. Fairbairns suggestion to limit the depth of printed terms. This makes it possible to evaluate and print some divergent terms (so-called tail-divergent terms):

Lambda_calc> let y_comb = f^((p^p#p) # (c ^ f#(c#c))) in eval $ y_comb#c
c (c (c (c (c (c (c (c (c (c (...))))))))))

It is amazing how well lambda-calculus and Haskell play together.