Lambda calculus is very small and still "Turing complete" language. However, because of its simplicity and small size, it is very hard to write real programs - even harder than in assembly language. Most of the materials demonstrating programming in lambda calculus> use meta-variables. For instance, TRUE is defined as and after that, TRUE is used instead of given expression. If such meta-variables are used, lambda-expressions are much shorter and more readable, however, there is no essential difference, since before reduction, all meta-variables are "expanded" into real lambda-expressions. I already implemented support for reduction of lambda expressions in my Newlisp library. The code that deals with meta-variables is rather simple. It is just recursive substitution of meta-variable's value for meta-variable itself. You can see how it works in my previous post, now updated.  |
Lambda Calculus Meta-variables Supported in my Newlisp Library.
Some Basic Concepts Implemented and Reduced in Lambda-calculus.
; After support for meta-variables in lambda-calculus is integrated ; in my Newlisp library, I can easily demonstrate few fundamental ; concepts: Boolean constants, integers, IF, predecessor, successor, ; multiplication and recursion are implemented in lambda calculus ; and how reduction of the expressions really looks like. ; ; At the end, factorial function is implemented - this time without ; full reduction, because even reduction of (FACTORIAL 0) is too ; large to be published in blog. However, you can try it for yourself. ; ; Watch out: it is frequently said this can be done, but it is ; rarely actually done. ; ; LOADING LIBRARY ; (setf [print.supressed] true [println.supressed] true) (load "http://instprog.com/Instprog.default-library.lsp") (setf [print.supressed] nil [println.supressed] nil) ;--------------------------------------------------------------- (setf TRUE '(^ x .(^ y . x))) (expand-and-reduce^ '((TRUE a) b) ; <- lambda-expression 5000 ; <- max number of expansions ; and reductions true) ; <- true if output is needed ;--------------------------------------------------------------- ; ; EXPANSION AND REDUCTION OF ((TRUE a) b) ; ; 1. ==[ original ]==> ((TRUE a) b) ; 2. ==[ expanded ]==> (((^x.(^y.x)) a) b) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> (((^x.(^y.x)) a) b) ; 2. ==[ beta ]==> ((^y.a) b) ; 3. ==[ alpha ]==> ((^x.a) b) ; 4. ==[ beta ]==> a ; ; REDUCED TO NORMAL FORM. ; ;--------------------------------------------------------------- (setf FALSE '(^ x . (^ y . y))) (expand-and-reduce^ '((FALSE a) b) 5000 true) ;--------------------------------------------------------------- ; ; EXPANSION AND REDUCTION OF ((FALSE a) b) ; ; 1. ==[ original ]==> ((FALSE a) b) ; 2. ==[ expanded ]==> (((^x.(^y.y)) a) b) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> (((^x.(^y.y)) a) b) ; 2. ==[ beta ]==> ((^y.y) b) ; 3. ==[ alpha ]==> ((^x.x) b) ; 4. ==[ beta ]==> b ; ; REDUCED TO NORMAL FORM. ; ;--------------------------------------------------------------- (setf IF '(^ v .(^ t . (^ f . ((v t) f))))) (expand-and-reduce^ '(((IF a) b) c) 5000 true) ;--------------------------------------------------------------- ; ; EXPANSION AND REDUCTION OF (((IF a) b) c) ; ; 1. ==[ original ]==> (((IF a) b) c) ; 2. ==[ expanded ]==> ((((^v.(^t.(^f.((v t) f)))) a) b) c) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((((^v.(^t.(^f.((v t) f)))) a) b) c) ; 2. ==[ alpha ]==> ((((^x.(^y.(^z.((x y) z)))) a) b) c) ; 3. ==[ eta ]==> ((((^x.(^y.(x y))) a) b) c) ; 4. ==[ eta ]==> ((((^x.x) a) b) c) ; 5. ==[ beta ]==> ((a b) c) ; ; REDUCED TO NORMAL FORM. ; ;--------------------------------------------------------------- (expand-and-reduce^ '(((IF TRUE) a) b) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (((IF TRUE) a) b) ; ; 1. ==[ original ]==> (((IF TRUE) a) b) ; 2. ==[ expanded ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.x))) a) b) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.x))) a) b) ; 2. ==[ alpha ]==> ((((^x.(^y.(^z.((x y) z))))(^u.(^v.u))) a) b) ; 3. ==[ eta ]==> ((((^x.(^y.(x y)))(^u.(^v.u))) a) b) ; 4. ==[ alpha ]==> ((((^x.(^y.(x y)))(^z.(^u.z))) a) b) ; 5. ==[ eta ]==> ((((^x.x)(^z.(^u.z))) a) b) ; 6. ==[ alpha ]==> ((((^x.x)(^y.(^z.y))) a) b) ; 7. ==[ beta ]==> (((^y.(^z.y)) a) b) ; 8. ==[ alpha ]==> (((^x.(^y.x)) a) b) ; 9. ==[ beta ]==> ((^y.a) b) ; 10. ==[ alpha ]==> ((^x.a) b) ; 11. ==[ beta ]==> a ; ; REDUCED TO NORMAL FORM. ; (expand-and-reduce^ '(((IF FALSE) a) b) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (((IF FALSE) a) b) ; ; 1. ==[ original ]==> (((IF FALSE) a) b) ; 2. ==[ expanded ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.y))) a) b) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((((^v.(^t.(^f.((v t) f))))(^x.(^y.y))) a) b) ; 2. ==[ alpha ]==> ((((^x.(^y.(^z.((x y) z))))(^u.(^v.v))) a) b) ; 3. ==[ eta ]==> ((((^x.(^y.(x y)))(^u.(^v.v))) a) b) ; 4. ==[ alpha ]==> ((((^x.(^y.(x y)))(^z.(^u.u))) a) b) ; 5. ==[ eta ]==> ((((^x.x)(^z.(^u.u))) a) b) ; 6. ==[ alpha ]==> ((((^x.x)(^y.(^z.z))) a) b) ; 7. ==[ beta ]==> (((^y.(^z.z)) a) b) ; 8. ==[ alpha ]==> (((^x.(^y.y)) a) b) ; 9. ==[ beta ]==> ((^y.y) b) ; 10. ==[ alpha ]==> ((^x.x) b) ; 11. ==[ beta ]==> b ; ; REDUCED TO NORMAL FORM. ; (setf APPLY '(^ v .(^ f . (v f)))) (expand-and-reduce^ '((APPLY a) b) 5000 true) ;---------------------------------------------------------------- ; ; EXPANSION AND REDUCTION OF ((APPLY a) b) ; ; 1. ==[ original ]==> ((APPLY a) b) ; 2. ==[ expanded ]==> (((^v.(^f.(v f))) a) b) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> (((^v.(^f.(v f))) a) b) ; 2. ==[ alpha ]==> (((^x.(^y.(x y))) a) b) ; 3. ==[ eta ]==> (((^x.x) a) b) ; 4. ==[ beta ]==> (a b) ; ; REDUCED TO NORMAL FORM. ; ;---------------------------------------------------------------- ; Y-combinator is tool that could be used for implementation of ; recursion (setf Y '(^ f . ((^ x . (f (x x))) (^ x . (f (x x)))))) (expand-and-reduce^ '(Y g) 12 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (Y g) ; ; 1. ==[ original ]==> (Y g) ; 2. ==[ expanded ]==> ((^f.((^x.(f (x x)))(^x.(f (x x))))) g) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((^f.((^x.(f (x x)))(^x.(f (x x))))) g) ; 2. ==[ alpha ]==> ((^x.((^y.(x (y y)))(^z.(x (z z))))) g) ; 3. ==[ beta ]==> ((^y.(g (y y)))(^z.(g (z z)))) ; 4. ==[ alpha ]==> ((^x.(g (x x)))(^y.(g (y y)))) ; 5. ==[ beta ]==> (g ((^y.(g (y y)))(^y.(g (y y))))) ; 6. ==[ alpha ]==> (g ((^x.(g (x x)))(^y.(g (y y))))) ; 7. ==[ beta ]==> (g (g ((^y.(g (y y)))(^y.(g (y y)))))) ; 8. ==[ alpha ]==> (g (g ((^x.(g (x x)))(^y.(g (y y)))))) ; 9. ==[ beta ]==> (g (g (g ((^y.(g (y y)))(^y.(g (y y))))))) ; 10. ==[ alpha ]==> (g (g (g ((^x.(g (x x)))(^y.(g (y y))))))) ; 11. ==[ beta ]==> (g (g (g (g ((^y.(g (y y)))(^y.(g (y y)))))))) ; 12. ==[ alpha ]==> (g (g (g (g ((^x.(g (x x)))(^y.(g (y y)))))))) ; ; UNREDUCED: MAX NUMBER OF REDUCTIONS REACHED. ; ; Take a look on the way "reduced" lambda-expression looks like; ; ; (Y g) is reduced to (g (Y g))! If we use some more complicated ; formula instead of g, and normal order of reduction, then ; g will be evaluated first. ; (setf ZERO '(^ f . (^ x . x))) (expand-and-reduce^ ZERO 5000 true) ;--------------------------------------------------------------- ; ; EXPANSION AND REDUCTION OF (^f.(^x.x)) ; ; 1. ==[ original ]==> (^f.(^x.x)) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> (^f.(^x.x)) ; 2. ==[ alpha ]==> (^x.(^y.y)) ; ; REDUCED TO NORMAL FORM. ; ;--------------------------------------------------------------- (setf SUCCESSOR '(^ n . (^ f . (^ x . (f ((n f) x)))))) (expand-and-reduce^ '(SUCCESSOR ZERO) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (SUCCESSOR ZERO) ; ; 1. ==[ original ]==> (SUCCESSOR ZERO) ; 2. ==[ expanded ]==> ((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))) ; 2. ==[ alpha ]==> ((^x.(^y.(^z.(y ((x y) z)))))(^u.(^v.v))) ; 3. ==[ beta ]==> (^y.(^z.(y (((^u.(^v.v)) y) z)))) ; 4. ==[ alpha ]==> (^x.(^y.(x (((^z.(^u.u)) x) y)))) ; 5. ==[ beta ]==> (^x.(^y.(x ((^u.u) y)))) ; 6. ==[ alpha ]==> (^x.(^y.(x ((^z.z) y)))) ; 7. ==[ beta ]==> (^x.(^y.(x y))) ; 8. ==[ eta ]==> (^x.x) ; ; REDUCED TO NORMAL FORM. ; (setf ONE '(^ x . x)) (expand-and-reduce^ '(SUCCESSOR (SUCCESSOR ZERO)) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (SUCCESSOR (SUCCESSOR ZERO)) ; ; 1. ==[ original ]==> (SUCCESSOR (SUCCESSOR ZERO)) ; 2. ==[ expanded ]==> ((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))) ; 2. ==[ alpha ]==> ((^x.(^y.(^z.(y ((x y) z)))))((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))) ; 3. ==[ beta ]==> (^y.(^z.(y ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) y) z)))) ; 4. ==[ alpha ]==> (^x.(^y.(x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p))) x) y)))) ; 5. ==[ beta ]==> (^x.(^y.(x (((^u.(^v.(u (((^w.(^p.p)) u) v)))) x) y)))) ; 6. ==[ alpha ]==> (^x.(^y.(x (((^z.(^u.(z (((^v.(^w.w)) z) u)))) x) y)))) ; 7. ==[ beta ]==> (^x.(^y.(x ((^u.(x (((^v.(^w.w)) x) u))) y)))) ; 8. ==[ alpha ]==> (^x.(^y.(x ((^z.(x (((^u.(^v.v)) x) z))) y)))) ; 9. ==[ beta ]==> (^x.(^y.(x (x (((^u.(^v.v)) x) y))))) ; 10. ==[ alpha ]==> (^x.(^y.(x (x (((^z.(^u.u)) x) y))))) ; 11. ==[ beta ]==> (^x.(^y.(x (x ((^u.u) y))))) ; 12. ==[ alpha ]==> (^x.(^y.(x (x ((^z.z) y))))) ; 13. ==[ beta ]==> (^x.(^y.(x (x y)))) ; ; REDUCED TO NORMAL FORM. ; (setf ZERO? '(^ n . ((n (TRUE FALSE)) TRUE))) (expand-and-reduce^ '(ZERO? ZERO) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (ZERO? ZERO) ; ; 1. ==[ original ]==> (ZERO? ZERO) ; 2. ==[ expanded ]==> ((^n.((n (TRUE FALSE)) TRUE))(^f.(^x.x))) ; 3. ==[ expanded ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))(^f.(^x.x))) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))(^f.(^x.x))) ; 2. ==[ alpha ]==> ((^x.((x ((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w))))(^q.(^r.r))) ; 3. ==[ beta ]==> (((^q.(^r.r))((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w))) ; 4. ==[ alpha ]==> (((^x.(^y.y))((^z.(^u.z))(^v.(^w.w))))(^p.(^q.p))) ; 5. ==[ beta ]==> ((^y.y)(^p.(^q.p))) ; 6. ==[ alpha ]==> ((^x.x)(^y.(^z.y))) ; 7. ==[ beta ]==> (^y.(^z.y)) ; 8. ==[ alpha ]==> (^x.(^y.x)) ; ; REDUCED TO NORMAL FORM. ; (expand-and-reduce^ '(ZERO? (SUCCESSOR ZERO)) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (ZERO? (SUCCESSOR ZERO)) ; ; 1. ==[ original ]==> (ZERO? (SUCCESSOR ZERO)) ; 2. ==[ expanded ]==> ((^n.((n (TRUE FALSE)) TRUE))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))) ; 3. ==[ expanded ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((^n.((n ((^x.(^y.x))(^x.(^y.y))))(^x.(^y.x))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))) ; 2. ==[ alpha ]==> ((^x.((x ((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w))))((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))) ; 3. ==[ beta ]==> ((((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))((^y.(^z.y))(^u.(^v.v))))(^w.(^p.w))) ; 4. ==[ alpha ]==> ((((^x.(^y.(^z.(y ((x y) z)))))(^u.(^v.v)))((^w.(^p.w))(^q.(^r.r))))(^x1.(^y1.x1))) ; 5. ==[ beta ]==> (((^y.(^z.(y (((^u.(^v.v)) y) z))))((^w.(^p.w))(^q.(^r.r))))(^x1.(^y1.x1))) ; 6. ==[ alpha ]==> (((^x.(^y.(x (((^z.(^u.u)) x) y))))((^v.(^w.v))(^p.(^q.q))))(^r.(^x1.r))) ; 7. ==[ beta ]==> ((^y.(((^v.(^w.v))(^p.(^q.q)))(((^z.(^u.u))((^v.(^w.v))(^p.(^q.q)))) y)))(^r.(^x1.r))) ; 8. ==[ alpha ]==> ((^x.(((^y.(^z.y))(^u.(^v.v)))(((^w.(^p.p))((^q.(^r.q))(^x1.(^y1.y1)))) x)))(^z1.(^u1.z1))) ; 9. ==[ beta ]==> (((^y.(^z.y))(^u.(^v.v)))(((^w.(^p.p))((^q.(^r.q))(^x1.(^y1.y1))))(^z1.(^u1.z1)))) ; 10. ==[ alpha ]==> (((^x.(^y.x))(^z.(^u.u)))(((^v.(^w.w))((^p.(^q.p))(^r.(^x1.x1))))(^y1.(^z1.y1)))) ; 11. ==[ beta ]==> ((^y.(^z.(^u.u)))(((^v.(^w.w))((^p.(^q.p))(^r.(^x1.x1))))(^y1.(^z1.y1)))) ; 12. ==[ alpha ]==> ((^x.(^y.(^z.z)))(((^u.(^v.v))((^w.(^p.w))(^q.(^r.r))))(^x1.(^y1.x1)))) ; 13. ==[ beta ]==> (^y.(^z.z)) ; 14. ==[ alpha ]==> (^x.(^y.y)) ; ; REDUCED TO NORMAL FORM. ; (setf MULTIPLY '(^ m . (^ n . (^ f . (m (n f)))))) (expand-and-reduce^ '((MULTIPLY (SUCCESSOR (SUCCESSOR ZERO))) (SUCCESSOR (SUCCESSOR ZERO))) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF ((MULTIPLY (SUCCESSOR (SUCCESSOR ZERO)))(SUCCESSOR (SUCCESSOR ZERO))) ; ; 1. ==[ original ]==> ((MULTIPLY (SUCCESSOR (SUCCESSOR ZERO)))(SUCCESSOR (SUCCESSOR ZERO))) ; 2. ==[ expanded ]==> (((^m.(^n.(^f.(m (n f)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> (((^m.(^n.(^f.(m (n f)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x)))))((^n.(^f.(^x.(f ((n f) x)))))((^n.(^f.(^x.(f ((n f) x)))))(^f.(^x.x))))) ; 2. ==[ alpha ]==> (((^x.(^y.(^z.(x (y z)))))((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2))))) ; 3. ==[ beta ]==> ((^y.(^z.(((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1))))(y z))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2))))) ; 4. ==[ alpha ]==> ((^x.(^y.(((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))))(x y))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1))))) ; 5. ==[ beta ]==> (^y.(((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) y))) ; 6. ==[ alpha ]==> (^x.(((^y.(^z.(^u.(z ((y z) u)))))((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x))) ; 7. ==[ beta ]==> (^x.((^z.(^u.(z ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) z) u))))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x))) ; 8. ==[ alpha ]==> (^x.((^y.(^z.(y ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) y) z))))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x))) ; 9. ==[ beta ]==> (^x.(^z.((((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) z)))) ; 10. ==[ alpha ]==> (^x.(^y.((((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))) x)((((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))(((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))((^x2.(^y2.(^z2.(y2 ((x2 y2) z2)))))(^u2.(^v2.v2)))) x)) y)))) ; 11. ==[ beta ]==> (^x.(^y.(((^u.(^v.(u ((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))) u) v)))) x)((((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))(((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))((^x2.(^y2.(^z2.(y2 ((x2 y2) z2)))))(^u2.(^v2.v2)))) x)) y)))) ; 12. ==[ alpha ]==> (^x.(^y.(((^z.(^u.(z ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) z) u)))) x)((((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))(((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))((^r1.(^x2.(^y2.(x2 ((r1 x2) y2)))))(^z2.(^u2.u2)))) x)) y)))) ; 13. ==[ beta ]==> (^x.(^y.((^u.(x ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) x) u)))((((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))(((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))((^r1.(^x2.(^y2.(x2 ((r1 x2) y2)))))(^z2.(^u2.u2)))) x)) y)))) ; 14. ==[ alpha ]==> (^x.(^y.((^z.(x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x) z)))((((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) y)))) ; 15. ==[ beta ]==> (^x.(^y.(x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x)((((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) y))))) ; 16. ==[ alpha ]==> (^x.(^y.(x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p))) x)((((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y))))) ; 17. ==[ beta ]==> (^x.(^y.(x (((^u.(^v.(u (((^w.(^p.p)) u) v)))) x)((((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y))))) ; 18. ==[ alpha ]==> (^x.(^y.(x (((^z.(^u.(z (((^v.(^w.w)) z) u)))) x)((((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y))))) ; 19. ==[ beta ]==> (^x.(^y.(x ((^u.(x (((^v.(^w.w)) x) u)))((((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y))))) ; 20. ==[ alpha ]==> (^x.(^y.(x ((^z.(x (((^u.(^v.v)) x) z)))((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y))))) ; 21. ==[ beta ]==> (^x.(^y.(x (x (((^u.(^v.v)) x)((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y)))))) ; 22. ==[ alpha ]==> (^x.(^y.(x (x (((^z.(^u.u)) x)((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r)))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y)))))) ; 23. ==[ beta ]==> (^x.(^y.(x (x ((^u.u)((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r)))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y)))))) ; 24. ==[ alpha ]==> (^x.(^y.(x (x ((^z.z)((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y)))))) ; 25. ==[ beta ]==> (^x.(^y.(x (x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q)))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y))))) ; 26. ==[ alpha ]==> (^x.(^y.(x (x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p)))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y))))) ; 27. ==[ beta ]==> (^x.(^y.(x (x (((^u.(^v.(u (((^w.(^p.p)) u) v))))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y))))) ; 28. ==[ alpha ]==> (^x.(^y.(x (x (((^z.(^u.(z (((^v.(^w.w)) z) u))))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) y))))) ; 29. ==[ beta ]==> (^x.(^y.(x (x ((^u.((((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)(((^v.(^w.w))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) u))) y))))) ; 30. ==[ alpha ]==> (^x.(^y.(x (x ((^z.((((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))) x)(((^z1.(^u1.u1))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) z))) y))))) ; 31. ==[ beta ]==> (^x.(^y.(x (x ((((^u.(^v.(^w.(v ((u v) w)))))((^p.(^q.(^r.(q ((p q) r)))))(^x1.(^y1.y1)))) x)(((^z1.(^u1.u1))(((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))((^q1.(^r1.(^x2.(r1 ((q1 r1) x2)))))(^y2.(^z2.z2)))) x)) y)))))) ; 32. ==[ alpha ]==> (^x.(^y.(x (x ((((^z.(^u.(^v.(u ((z u) v)))))((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1)))) x)(((^y1.(^z1.z1))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y)))))) ; 33. ==[ beta ]==> (^x.(^y.(x (x (((^u.(^v.(u ((((^w.(^p.(^q.(p ((w p) q)))))(^r.(^x1.x1))) u) v)))) x)(((^y1.(^z1.z1))(((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))((^p1.(^q1.(^r1.(q1 ((p1 q1) r1)))))(^x2.(^y2.y2)))) x)) y)))))) ; 34. ==[ alpha ]==> (^x.(^y.(x (x (((^z.(^u.(z ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) z) u)))) x)(((^x1.(^y1.y1))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y)))))) ; 35. ==[ beta ]==> (^x.(^y.(x (x ((^u.(x ((((^v.(^w.(^p.(w ((v w) p)))))(^q.(^r.r))) x) u)))(((^x1.(^y1.y1))(((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))((^w1.(^p1.(^q1.(p1 ((w1 p1) q1)))))(^r1.(^x2.x2)))) x)) y)))))) ; 36. ==[ alpha ]==> (^x.(^y.(x (x ((^z.(x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x) z)))(((^r.(^x1.x1))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y)))))) ; 37. ==[ beta ]==> (^x.(^y.(x (x (x ((((^u.(^v.(^w.(v ((u v) w)))))(^p.(^q.q))) x)(((^r.(^x1.x1))(((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))((^v1.(^w1.(^p1.(w1 ((v1 w1) p1)))))(^q1.(^r1.r1)))) x)) y))))))) ; 38. ==[ alpha ]==> (^x.(^y.(x (x (x ((((^z.(^u.(^v.(u ((z u) v)))))(^w.(^p.p))) x)(((^q.(^r.r))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y))))))) ; 39. ==[ beta ]==> (^x.(^y.(x (x (x (((^u.(^v.(u (((^w.(^p.p)) u) v)))) x)(((^q.(^r.r))(((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))((^u1.(^v1.(^w1.(v1 ((u1 v1) w1)))))(^p1.(^q1.q1)))) x)) y))))))) ; 40. ==[ alpha ]==> (^x.(^y.(x (x (x (((^z.(^u.(z (((^v.(^w.w)) z) u)))) x)(((^p.(^q.q))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y))))))) ; 41. ==[ beta ]==> (^x.(^y.(x (x (x ((^u.(x (((^v.(^w.w)) x) u)))(((^p.(^q.q))(((^r.(^x1.(^y1.(x1 ((r x1) y1)))))((^z1.(^u1.(^v1.(u1 ((z1 u1) v1)))))(^w1.(^p1.p1)))) x)) y))))))) ; 42. ==[ alpha ]==> (^x.(^y.(x (x (x ((^z.(x (((^u.(^v.v)) x) z)))(((^w.(^p.p))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y))))))) ; 43. ==[ beta ]==> (^x.(^y.(x (x (x (x (((^u.(^v.v)) x)(((^w.(^p.p))(((^q.(^r.(^x1.(r ((q r) x1)))))((^y1.(^z1.(^u1.(z1 ((y1 z1) u1)))))(^v1.(^w1.w1)))) x)) y)))))))) ; 44. ==[ alpha ]==> (^x.(^y.(x (x (x (x (((^z.(^u.u)) x)(((^v.(^w.w))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) y)))))))) ; 45. ==[ beta ]==> (^x.(^y.(x (x (x (x ((^u.u)(((^v.(^w.w))(((^p.(^q.(^r.(q ((p q) r)))))((^x1.(^y1.(^z1.(y1 ((x1 y1) z1)))))(^u1.(^v1.v1)))) x)) y)))))))) ; 46. ==[ alpha ]==> (^x.(^y.(x (x (x (x ((^z.z)(((^u.(^v.v))(((^w.(^p.(^q.(p ((w p) q)))))((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))) x)) y)))))))) ; 47. ==[ beta ]==> (^x.(^y.(x (x (x (x (((^u.(^v.v))(((^w.(^p.(^q.(p ((w p) q)))))((^r.(^x1.(^y1.(x1 ((r x1) y1)))))(^z1.(^u1.u1)))) x)) y))))))) ; 48. ==[ alpha ]==> (^x.(^y.(x (x (x (x (((^z.(^u.u))(((^v.(^w.(^p.(w ((v w) p)))))((^q.(^r.(^x1.(r ((q r) x1)))))(^y1.(^z1.z1)))) x)) y))))))) ; 49. ==[ beta ]==> (^x.(^y.(x (x (x (x ((^u.u) y))))))) ; 50. ==[ alpha ]==> (^x.(^y.(x (x (x (x ((^z.z) y))))))) ; 51. ==[ beta ]==> (^x.(^y.(x (x (x (x y)))))) ; ; REDUCED TO NORMAL FORM. ; (setf PREDECESSOR '(^ n . (((n (^ p . (^ z . ((z (SUCCESSOR (p TRUE))) (p TRUE))))) (^ z . ((z ZERO) ZERO))) FALSE))) (expand-and-reduce^ '(PREDECESSOR ONE) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; EXPANSION AND REDUCTION OF (PREDECESSOR ONE) ; ; 1. ==[ original ]==> (PREDECESSOR ONE) ; 2. ==[ expanded ]==> ((^n.(((n (^p.(^z.((z (SUCCESSOR (p TRUE)))(p TRUE)))))(^z.((z ZERO) ZERO))) FALSE))(^x.x)) ; 3. ==[ expanded ]==> ((^n.(((n (^p.(^z.((z ((^n.(^f.(^x.(f ((n f) x)))))(p (^x.(^y.x)))))(p (^x.(^y.x)))))))(^z.((z (^f.(^x.x)))(^f.(^x.x)))))(^x.(^y.y))))(^x.x)) ; ; META-VARIABLES EXPANDED. ; ; 1. ==[ start ]==> ((^n.(((n (^p.(^z.((z ((^n.(^f.(^x.(f ((n f) x)))))(p (^x.(^y.x)))))(p (^x.(^y.x)))))))(^z.((z (^f.(^x.x)))(^f.(^x.x)))))(^x.(^y.y))))(^x.x)) ; 2. ==[ alpha ]==> ((^x.(((x (^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r)))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1))))(^r1.r1)) ; 3. ==[ beta ]==> ((((^r1.r1)(^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r)))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1))) ; 4. ==[ alpha ]==> ((((^x.x)(^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r)))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1))) ; 5. ==[ beta ]==> (((^y.(^z.((z ((^u.(^v.(^w.(v ((u v) w)))))(y (^p.(^q.p)))))(y (^r.(^x1.r))))))(^y1.((y1 (^z1.(^u1.u1)))(^v1.(^w1.w1)))))(^p1.(^q1.q1))) ; 6. ==[ alpha ]==> (((^x.(^y.((y ((^z.(^u.(^v.(u ((z u) v)))))(x (^w.(^p.w)))))(x (^q.(^r.q))))))(^x1.((x1 (^y1.(^z1.z1)))(^u1.(^v1.v1)))))(^w1.(^p1.p1))) ; 7. ==[ beta ]==> ((^y.((y ((^z.(^u.(^v.(u ((z u) v)))))((^x1.((x1 (^y1.(^z1.z1)))(^u1.(^v1.v1))))(^w.(^p.w)))))((^x1.((x1 (^y1.(^z1.z1)))(^u1.(^v1.v1))))(^q.(^r.q)))))(^w1.(^p1.p1))) ; 8. ==[ alpha ]==> ((^x.((x ((^y.(^z.(^u.(z ((y z) u)))))((^v.((v (^w.(^p.p)))(^q.(^r.r))))(^x1.(^y1.x1)))))((^z1.((z1 (^u1.(^v1.v1)))(^w1.(^p1.p1))))(^q1.(^r1.q1)))))(^x2.(^y2.y2))) ; 9. ==[ beta ]==> (((^x2.(^y2.y2))((^y.(^z.(^u.(z ((y z) u)))))((^v.((v (^w.(^p.p)))(^q.(^r.r))))(^x1.(^y1.x1)))))((^z1.((z1 (^u1.(^v1.v1)))(^w1.(^p1.p1))))(^q1.(^r1.q1)))) ; 10. ==[ alpha ]==> (((^x.(^y.y))((^z.(^u.(^v.(u ((z u) v)))))((^w.((w (^p.(^q.q)))(^r.(^x1.x1))))(^y1.(^z1.y1)))))((^u1.((u1 (^v1.(^w1.w1)))(^p1.(^q1.q1))))(^r1.(^x2.r1)))) ; 11. ==[ beta ]==> ((^y.y)((^u1.((u1 (^v1.(^w1.w1)))(^p1.(^q1.q1))))(^r1.(^x2.r1)))) ; 12. ==[ alpha ]==> ((^x.x)((^y.((y (^z.(^u.u)))(^v.(^w.w))))(^p.(^q.p)))) ; 13. ==[ beta ]==> ((^y.((y (^z.(^u.u)))(^v.(^w.w))))(^p.(^q.p))) ; 14. ==[ alpha ]==> ((^x.((x (^y.(^z.z)))(^u.(^v.v))))(^w.(^p.w))) ; 15. ==[ beta ]==> (((^w.(^p.w))(^y.(^z.z)))(^u.(^v.v))) ; 16. ==[ alpha ]==> (((^x.(^y.x))(^z.(^u.u)))(^v.(^w.w))) ; 17. ==[ beta ]==> ((^y.(^z.(^u.u)))(^v.(^w.w))) ; 18. ==[ alpha ]==> ((^x.(^y.(^z.z)))(^u.(^v.v))) ; 19. ==[ beta ]==> (^y.(^z.z)) ; 20. ==[ alpha ]==> (^x.(^y.y)) ; ; REDUCED TO NORMAL FORM. ; (setf FACTORIAL '(Y (^ f . (^ n .((((IF ZERO?) n) ONE) ((MULTIPLY n) (f (PREDECESSOR n)))))))) (expand-and-reduce^ '(FACTORIAL (SUCCESSOR (SUCCESSOR ONE))) 5000 true) ;--------------------------------------------------------------- ; ;---------------------------------------------------------------; Roughly ten minutes and 100000 of lines later, on my computer ; ; ... ; ; 2379. ==[ beta ]==> (^x.(^y.(x (x (x (x (x (x ((^u.u) y))))))))) ; 2380. ==[ alpha ]==> (^x.(^y.(x (x (x (x (x (x ((^z.z) y))))))))) ; 2381. ==[ beta ]==> (^x.(^y.(x (x (x (x (x (x y)))))))) ; ; REDUCED TO NORMAL FORM. ; ; EVERYTHING WORKS! (exit) |
Subscribe to:
Posts (Atom)