Lambda Calculus Meta-variables Supported in my Newlisp Library.



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

'(^ x .(^ y . x))),

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.




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)