Well, I tried to fix the problems you mention. Results attached.

I'm sorry I can't get it to work. The simplest example passes: Lambda> :t eval (A (L x0 x0) x1) eval (A (L x0 x0) x1) :: Next X but even anything more complex seems to fail: Lambda> :t eval (A (L x0 x0) (A x0 x0)) eval (A (L x0 x0) (A x0 x0)) :: Eval (A (L X X) (A X X)) a => a The reduce functions seems to do better: Lambda> :t reduce (A (L x0 x0) (L x1 x1)) reduce (A (L x0 x0) (L x1 x1)) :: (L (Next X) (Next X),T) but fails on more complex examples: Lambda> :t reduce (A (L x0 (L x1 (A x0 x1))) x2) reduce (A (L x0 (L x1 (A x0 x1))) x2) :: Reduce (A (L X (L (Next X) (A X (Next X)))) (Next (Next X))) (L a (A b c)) d => (L a (A b c),d)

I have managed to do without de Brujin notation. It seems that you've implemented something like the calculus of explicit substitutions. The latter has a 'shift' operation to shift up all the variables: s0 -> s1, s1 -> s2, etc.

I'll try to come up with a regression test suite You may want to try evaluating the following terms:

((lambda (x) (x x)) (lambda (y) (y z))) ==> (z z) (lambda (a) ((lambda (x) (lambda (a) (x a))) a)) ==> (lambda (a) (lambda (a-new) (a a-new))) ; compute a*(a+b) ( (lambda (a) (lambda (b) (lambda (f) (a (lambda (x) ((b f) ((a f) x))))))) (lambda (f) (lambda (x) (f (f x)))) ; Numeral 2 (lambda (f) (lambda (x) (f x))) ; Numeral 1 ) ==> numeral for 6 These are some of the tests from my meta-lambda calculator. The normal-order evaluator recipe includes a "repeat until done" phrase. This is one of the challenging aspects: keeping track when done. It seems there is a simpler, purely recursive way of performing the normal reductions. First we need a more general notation for applications: (A t (C t1 (C t2 CNil))) is the same as ((A t t1) t2). The algorithm can be expressed as a sequence of the following re-writing rules, which must be tried in the order given: ; The top-level is a lambda-term: reduce inside Eval (L x body) -> (L x (Eval body)) ; The top-most leftmost is a redex ; Reduce it and retry from the top Eval ((L x body) term) -> Eval (Beta x body term) ; The topmost is a nested application ; Unfold using the associativity rule: ; If (a b) is not a redex and a is not a pair, we try reducing b ; If (a b) is not a redex and a is a pair (x y), we unfold this ; as (x y b) and repeat. Eval ((x) rest) -> Eval (x rest) ; (x) is the same as x Eval ((x y . in-rest) . rest) -> Eval (Append (x y . in-rest) rest) ; In topmost (x y z ...), x is not an appl and not an abst ; It is equivalent to ((x y) z ...) ; Try to reduce y, z, etc. separately Eval (x y . rest) -> (A x (Map Eval (y . rest))) ; The topmost is (x) -- remove the extra parens Eval (term) -> Eval term Eval var -> var This algorithm has been literally implemented in http://pobox.com/~oleg/ftp/Computation/rewriting-rule-lambda.txt (in a continuation-passing-style).