# 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));