;; load the file and try the following examples
;; 
;; (decodeNum (encode 88))
;; (decodeNum (succ (encode 5)))
;; (decodeNum (pred (encode 72)))
;; (decodeBool (iszero (encode 0)))
;; (decodeBool (iszero (encode 42)))
;; (decodeNum (add (cons (encode 3) (encode 99))))
;; (decodeNum (mult (cons (encode 2) (encode 5))))
;; ...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Abbreviations

(define I (lambda (x) x))
(define K (lambda (x y) x))

;; Encoding of booleans in the call-by-value lambda calculus

(define True (lambda (x y) (x)))
(define False (lambda (x y) (y)))

(define decodeBool (lambda (b) (b (lambda () #t) (lambda () #f))))

;; (Church)-encoding of numerals in the lambda calculus

(define encode
  (lambda (n)
    (lambda (f x) (iterate f n x))))

(define iterate
  (lambda (f n x)
    (if (zero? n)
	x
	(f (iterate f (sub1 n) x)))))

(define decodeNum (lambda (cn) (cn add1 0)))

(define zz (encode 0))
(define oo (encode 1))

;; Basic functions on Church-numerals (successor, predecessor, test for zero)

(define succ
  (lambda (x)
    (lambda (f y)
      (f (x f y)))))

(define pred
  (lambda (x)
    (lambda (f y)
      ((x (lambda (p) (lambda (q) (q (p f)))) (lambda (z) (K y z))) I))))

(define iszero
  (lambda (x)
    (x (lambda (y) False) True)))

;; More functions on numerals

(define Yv
  (lambda (f)
    ((lambda (x) (f (lambda (z) ((x x) z))))
     (lambda (x) (f (lambda (z) ((x x) z)))))))

;; I am not encoding pairs since that's part of the homework

(define add
  (Yv (lambda (f)
	(lambda (args)
	  (let ([x (car args)] [y (cdr args)])
	    ((iszero x)
	     (lambda () y)
	     (lambda () (f (cons (pred x) (succ y))))))))))

;; that's the one I couldn't do in class :-)

(define mult
  (Yv (lambda (f)
	(lambda (args)
	  (let ([x (car args)] [y (cdr args)])
	    ((iszero x)
	     (lambda () zz)
	     (lambda () ((iszero (pred x))
			 (lambda () y)
			 (lambda ()
			   (add (cons y (f (cons (pred x) y)))))))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;