anatoli <anatoli at yahoo> wrote:

Attached are two interpreters: one for untyped lambda calculus,

I'm afraid the attached interpreter can't be an implementation of the lambda calculus. For one thing, it lacks the hygiene of substitutions: Lambda> :t lambdaEval (A (L X (L Y (A X Y))) T) lambdaEval (A (L X (L Y (A X Y))) T) :: L Y (A T Y) That's OK. However, Lambda> :t lambdaEval (A (L X (L Y (A X Y))) Y) lambdaEval (A (L X (L Y (A X Y))) Y) :: L Y (A Y Y) That is wrong! The correct answer is: L Yfresh (A Y Yfresh) The interpreter in question doesn't appear to be able to manufacture fresh identifiers (i.e., fresh types). Without an ability to expand the set of available identifiers, the capture-free substitution is impossible. Furthermore, some terms fail to evaluate: Lambda> :t lambdaEval (A (L X (A X X)) T) lambdaEval (A (L X (A X X)) T) :: Eval (A (L X (A X X)) T) a => a Lambda> :t lambdaEval (A (A (L X X) T) Y) lambdaEval (A (A (L X X) T) Y) :: Eval (A (A (L X X) T) Y) a => a which is not the result one would've expected. Finally, the interpreter doesn't actually find the normal form. The rule

instance Eval (L v e) (L v e)

prevents any reductions under lambda. True, call-by-name or call-by-value interpreters stop short of reducing the body of a lambda form. Normal or applicative order interpreters however -- in order to find the beta-eta-normal form -- should seek and attempt any reduction. The hygienic substitution (with alpha-conversion if necessary) and the repeated identification of the leftmost outermost redex are actually quite challenging. We can guarantee the hygienic substitution if we implement the de Bruijin notation for lambda terms. Another, related technique is coloring of existing identifiers. A macro-expander of R5RS Scheme macros implements the coloring to ensure the hygiene of macro expansions. The macro-expander can be cajoled into painting identifiers on our demand, which has been used in a macro-expand-time lambda calculator. In Haskell, we have to paint manually. A variable in a typechecker-time lambda-calculator has to be represented by a type like Vr (Succ (Succ (Succ Zero))) X. The latter component is the "name" and the former is the color. The Eval and Subst relations should be extended with color_in and color_out type parameters (perhaps with a dependency: term color_in -> color_out). The only non-trivial use of colors is in doing a substitution (L var body)[exp/var']. The bound variable has to be repainted before the substitution in the body. The beta-substitutor itself can do the repainting.