Section 23 Want more of a challenge? View in iconic form (experimental)

---

       # MATH some pure lambda calculus definitions - optional
       # these definitions are not quite what we want
       # since thinking of everything as a function requires headscratching
       # it would be better to use these as a parallel means of evaluation
       # ... for expressions
[hear] (define pure-if /
         ? x /
         ? y /
         ? z /
         x (y) (z));

[hear] (define pure-true / ? y / ? z / y);

[hear] (define pure-false / ? y / ? z / z);

[hear] (define pure-cons /
         ? x /
         ? y /
         ? z /
         pure-if (z) (x) (y));

[hear] (define pure-car / ? x / x (pure-true));

[hear] (define pure-cdr / ? x / x (pure-false));

[hear] (define zero / ? f / ? x / x);

[hear] (define one / ? f / ? x / f (x));

[hear] (define two / ? f / ? x / f (f (x)));

[hear] (define succ /
         ? n /
         ? f /
         ? x /
         f ((n (f)) (x)));

[hear] (define add / ? a / ? b / (a (succ)) (b));

[hear] (define mult /
         ? a /
         ? b /
         (a (add / b)) (zero));

[hear] (define pred /
         ? n /
         pure-cdr /
         (n (? p /
             pure-cons
              (succ /
               pure-car /
               p)
              (pure-car /
               p)))
         (pure-cons (zero) (zero)));

[hear] (define is-zero /
         ? n /
         (n (? dummy / pure-false) (pure-true)));

[hear] (define fixed-point /
         ? f /
         (? x / f (x (x))) (? x / f (x (x))));

       # .. but for rest of message will assume that define does fixed-point for us
       # now build a link between numbers and church number functions
[hear] (define unchurch /
         ? c /
         c (? x / + (x) 1) 0);

[hear] (= 0 (unchurch / zero));

[hear] (= 1 (unchurch / one));

[hear] (= 2 (unchurch / two));

[hear] (define church /
         ? x /
         if (= 0 (x))
          (zero)
          (succ /
           church /
           - (x) 1));