A practical lambdacalculator 2.2 review
DownloadA practical lambdacalculator is a normalorder evaluator for the untyped lambdacalculus, extended with convenient commands and shor


A practical lambdacalculator is a normalorder evaluator for the untyped lambdacalculus, 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 alphaconversion, print all defined shortcuts and evaluation flags, etc.
Terms to evaluate and commands are entered at a readevalprintloop (REPL) "prompt" or "included" from a file by a special command. A Haskell branch is an embedding of the lambda calculator (as a domainspecific 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 betasubstitutions, 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 normalorder 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. We're proposing what seems to be an efficient and elegant technique that can be implemented through intuitive rewriting 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 lambdacalculator "reparses" the result after the successful reduce step. The source and the target languages of our "parser" (lambdacalculator) 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 lambdaterms in Twelf.
The following examples show that lambdacalculus becomes a domainspecific language embedded into Haskell:
> c0 = f ^ x ^ x  Church numeral 0
> succ = c ^ f ^ x ^ f # (c # f # x)  Successor
> c1 = eval $ succ # c0  preevaluate 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 preevaluate (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 lambdacalculus can be useful for theorem proving, even over universallyquantified formulas.
The calculator implements Dr. Fairbairn's suggestion to limit the depth of printed terms. This makes it possible to evaluate and print some divergent terms (socalled taildivergent 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 lambdacalculus and Haskell play together.
A practical lambdacalculator 2.2 search tags