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)

No comments:

Post a Comment