
oleg@pobox.com wrote [in part]:
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
It evaluates all right to "A X X" in both ghci 5.02.1 and December 2001 Hugs.
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)
Same here: evaluates to (L (Next (Next (Next X))) (A (Next (Next X)) (Next (Next (Next X)))),T) You may be using an older version of Hugs that is known to have problems with fundeps.
You may want to try evaluating the following terms:
((lambda (x) (x x)) (lambda (y) (y z))) ==> (z z)
Here is a real bug, even two. First, two rules for SameVar are wrong; second, a rule for Apply is missing. diff lambda.lhs lambda.lhs.buggy 80c80 < > instance SameVar (Next x) (A y z) F ---
instance SameVar (Next x) (A x y) F 82c82 < > instance SameVar (Next x) (L y z) F
instance SameVar (Next x) (L x y) F 150d149 < > instance (Reduce y y' tryAgain) => Apply (Next x) y (A (Next x) y') tryAgain
With these fixes, this one passes:
(lambda (a) ((lambda (x) (lambda (a) (x a))) a)) ==> (lambda (a) (lambda (a-new) (a a-new)))
Lambda> :t eval (L x0 (A (L x1 (L x0 (A x1 x0))) x0)) L X (L (Next (Next X)) (A X (Next (Next X)))) but this does not, no matter what I try:
; 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
Time to try other approaches... -- anatoli __________________________________________________ Do You Yahoo!? Yahoo! Tax Center - online filing with TurboTax http://taxes.yahoo.com/