#lang racket
;; Using Racket lambdas in the style of lambda calculus,
;; we can build the Church encodings and easily evaluate
;; expressions in the lambda calculus.  However, note that,
;; as Racket lambdas, they will always follow the Racket
;; evaluation rules, which, while valid lambda calculus
;; evaluation rules, are not always the ideal choice
;; (among more options).
(define True   (lambda (x) (lambda (y) x)))
(define False  (lambda (x) (lambda (y) y)))
(define Cond   (lambda (condVal) (lambda (thenVal) (lambda (elseVal) ((condVal thenVal) elseVal)))))
(define Zero   (lambda (x) (lambda (z) z)))
(define One    (lambda (x) (lambda (z) (x z))))
(define Succ   (lambda (x) (lambda (y) (lambda (z) (y ((x y) z))))))
(define Plus   (lambda (w) (lambda (x) (lambda (y) (lambda (z) ((x y) ((w y) z)))))))
(define Mult   (lambda (x) (lambda (y) (((y (Plus x)) Zero)))))
(define IsZero (lambda (x) (x ((lambda (y) False) True))))
(define Pair   (lambda (m) (lambda (n) (lambda (b) (((Cond b) m) n)))))
(define First  (lambda (p) (p True)))
(define Second (lambda (p) (p False)))
(define PZero  ((Pair Zero) Zero))
(define PSucc  (lambda (n) ((Pair (Second n)) (Succ (Second n)))))
(define Pred   (lambda (n) (First ((n PSucc) PZero))))

;; Beware the Y combinator encoding as *Racket* lambdas.
;; Racket's evaluation rules will choose a non-terminating series of reductions when applying Y,
;; even though there exists another that reaches a normal form.
(define Y      (lambda (f) ( (lambda (x) (f (x x))) (lambda (x) (f (x x))))))

;; Function to be used by Y to implement factorial.
(define F      (lambda (f) (lambda (n) (((Cond (IsZero n)) One) ((Mult n) (f (Pred n)))))))

;; So, for example, this definition of Fact will never reach a normal form
;; under Racket's evaluation rules.

;; (define Fact   (Y F))

;; Even this call, where we avoid trying to evaluate Y F early to bind to Fact,
;; will never reach a normal form under Racket's evaluation rules.

;; (define fact-one ((Y F) One)

;; Why do you think this happens even though there does exist a valid series
;; of reduction steps that results in the right normal form answer?


;; Racket functions that help construct and destruct lambda terms.

;; Create the Church encoding of natural number x, given as a Racket number.
(define (n x)
  (if (= n 0)
      Zero
      (Succ (n (- x 1)))))

;; Convert Church encodings to Racket equivalents.
(define (Lambda->Number   x) ((x (lambda (y) (+ y 1))) 0))
(define (Lambda->Bool     x) ((x #t) #f))
(define (Lambda->Pair f s x) (cons (f (x True)) (s (x False))))

;; How to use this lambda calculus representation:
;;
;; Write x as x
;; Write (\x.e) as (lambda (x) e).
;; Write (e1 e2) as (e1 e2).
;;
;; To convert a Church encoding of a number or boolean to a Racket expression,
;; Write (Lambda->Number e) or (Lambda->Bool e) or (Lambda->Pair f s e),
;; where f and s are Racket functions to convert the two pieces of the pair
;; to Racket expressions.
;;
;; For example, this produces '(0 . 2):
(define pair-zero-two  (Lambda->Pair Lambda->Number Lambda->Number ((Pair Zero) (Succ One))))