Lambda over types.
oleg@pobox.com
oleg@pobox.com
Fri, 5 Apr 2002 13:51:10 -0800 (PST)
> 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).