;; The first three lines of this file were inserted by DrRacket. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#reader(lib "htdp-advanced-reader.ss" "lang")((modname 2015-12-02-lerner) (read-case-sensitive #t) (teachpacks ()) (htdp-settings #(#t constructor repeating-decimal #t #t none #f () #f)))
(define (eternity x) (eternity x))

#;(define (length l)
  (cond
    [(empty? l) 0]
    [else (add1 (length (rest l)))]))

#;(define length0
  (λ(l)
    (cond
      [(empty? l) 0]
      [else (add1 (eternity (rest l)))])))
#;(define length1
  (λ(l)
    (cond
      [(empty? l) 0]
      [else (add1 (length0 (rest l)))])))
#;(define length2
  (λ(l)
    (cond
      [(empty? l) 0]
      [else (add1 (length1 (rest l)))])))
(define (make-length LEN)
  (λ(l)
    (cond
      [(empty? l) 0]
      [else (add1 (LEN (rest l)))])))
(define length0 (make-length eternity))
(define length1 (make-length length0))
(define length2 (make-length (make-length (make-length eternity))))
(define (make-fact FACT)
  (λ(n)
    (cond
      [(zero? n) 1]
      [else (* n (FACT (sub1 n)))])))
;((make-fact (make-fact (make-fact (make-fact eternity)))) 3)

(define Y ; eager version: actually works in Racket
  (λ(F)
    ((λ(f) (f f))
     (λ(f) (F (λ(x) ((f f) x)))))))
#;(define Y-lazy ; only works in a lazy language; will loop forever in Racket
  (λ(F)
    ((λ(f) (f f))
     (λ(f) (F (f f))))))

(define factorial
  (Y (λ(fact)
         (λ(n)
           (cond
             [(zero? n) 1]
             [else (* n (fact (sub1 n)))])))))
(define len
  (Y (λ(lng)
         (λ(l)
           (cond
             [(empty? l) 0]
             [else (add1 (lng (rest l)))])))))

#|
Observation:
len ==behaves the same as== (make-length len)
Or in other words, len is a "fixed point" of the make-length function

But the amazing part is,
len ==behaves the same as== (Y make-length)
so,
(Y make-length) = (make-length (Y make-length))
In other words, Y is the function that takes a function and computes its fixed point,
and that fixed point behaves as if it were a recursively defined function!
|#



#|#|#|#|#|#|#|#| JUST TO SHOW WE CAN |#|#|#|#|#|#|#|#

;; Here's the code from last time...

;; BOOLEANS (over-eager!)
(define TRUE (λ(x) (λ(y) x)))
(define FALSE (λ(x) (λ(y) y)))
(define IF
  (λ(c) (λ(t) (λ(f)
                ((c t) f)))))
;; LAZY BOOLEANS (because laziness is sometimes a virtue)
;; **calls** the t or f arguments it gets, as functions of zero arguments
;; But we don't have to change the definitions of TRUE or FALSE,
;; just how we call IF.
;; NOTE: In order to have functions with zero arguments,
;; we have to bump up to Advanced Student Language...finally!
(define LAZY-IF
  (λ(c) (λ(t) (λ(f)
                (((c t) f))))))
(define (BOOL->bool b) ((b true) false))

(check-expect (((IF TRUE) 5) 6) 5)
(check-expect (((IF FALSE) 5) 6) 6)

;; PAIRS
(define PAIR (λ(x) (λ(y) (λ(s) ((s x) y)))))
(define FST (λ(p) (p (λ(x) (λ(y) x)))))
(define SND (λ(p) (p (λ(x) (λ(y) y)))))

(check-expect (FST ((PAIR 4) 5)) 4)
(check-expect (SND ((PAIR 4) 5)) 5)

;; NUMBERS
(define ZERO (λ(f) (λ(x) x)))
(define ONE (λ(f) (λ(x) (f ((ZERO f) x)))))
(define TWO (λ(f) (λ(x) (f ((ONE f) x)))))
(define THREE (λ(f) (λ(x) (f ((TWO f) x)))))
(define FOUR (λ(f) (λ(x) (f ((THREE f) x)))))
(define FIVE (λ(f) (λ(x) (f ((FOUR f) x)))))

(define (NUM->num n) ((n add1) 0))

(check-expect (NUM->num ZERO) 0)
(check-expect (NUM->num ONE) 1)
(check-expect (NUM->num TWO) 2)
(check-expect (NUM->num THREE) 3)
(check-expect (NUM->num FOUR) 4)
(check-expect (NUM->num FIVE) 5)


(define ADD1
  (λ(n)
    (λ(f) (λ(x) (f ((n f) x))))))
(check-expect (NUM->num (ADD1 FOUR)) 5)

(define ADD (λ(m) (λ(n) ((m ADD1) n))))
(check-expect (NUM->num ((ADD TWO) THREE)) (NUM->num FIVE))

(define MUL (λ(m) (λ(n) ((m (ADD n)) ZERO))))
(check-expect (NUM->num ((MUL TWO) THREE)) (NUM->num (ADD1 FIVE)))

(define SUB1
  (local ((define (row->row r)
            ((PAIR (ADD1 (FST r))) (FST r))))
    (λ(n)
      (SND ((n row->row) ((PAIR ZERO) ZERO))))))
(check-expect (NUM->num (SUB1 FIVE)) 4)

(define SUB (λ(m) (λ(n) ((n SUB1) m))))
(check-expect (NUM->num ((SUB FIVE) THREE)) (NUM->num TWO))
(check-expect (NUM->num ((SUB THREE) FIVE)) (NUM->num ZERO))

(define ZERO?
  (λ(n) ((n (λ(dont-care-at-all) FALSE)) TRUE)))
(check-expect (BOOL->bool (ZERO? ZERO)) true)
(check-expect (BOOL->bool (ZERO? ONE)) false)

(define (FACT n)
  (((LAZY-IF (ZERO? n))
    (λ() ONE))
   (λ() ((MUL n) (FACT (SUB1 n))))))
(check-expect (NUM->num (FACT ZERO)) 1)
(check-expect (NUM->num (FACT FIVE)) 120)


#|#|#|#|#|#|#|#|#| AND NOW FOR THE FINAL STEP |#|#|#|#|#|#|#|#|#
(define FACT-maker
  (λ(FACT)
    (λ(n)
      (((LAZY-IF (ZERO? n))
        (λ() ONE))
       (λ() ((MUL n) (FACT (SUB1 n))))))))
(define FACT2 (Y FACT-maker))

(check-expect (NUM->num (FACT2 FIVE)) 120)

;; We've managed to define factorial using *nothing* but lambdas!

#|
Just for kicks: let's expand every single definition we have, until nothing remains:
(Y FACT-maker)
==
((λ(F)
    ((λ(f) (f f))
     (λ(f) (F (λ(x) ((f f) x))))))
 (λ(FACT)
   (λ(n)
     (((LAZY-IF (ZERO? n))
       (λ() ONE))
      (λ() ((MUL n) (FACT (SUB1 n))))))))
==
((λ(F)
    ((λ(f) (f f))
     (λ(f) (F (λ(x) ((f f) x))))))
 (λ(FACT)
   (λ(n)
     (((LAZY-IF (ZERO? n))
       (λ() ONE))
      (λ() ((MUL n) (FACT (SUB1 n)))))))))
==
((λ(F)
   ((λ(f) (f f))
    (λ(f) (F (λ(x) ((f f) x))))))
 (λ(FACT)
   (λ(n)
     ((((λ(c) (λ(t) (λ(f) (((c t) f)))))
        ((λ(n) ((n (λ(dont-care-at-all) (λ(x) (λ(y) y)))) (λ(x) (λ(y) x)))) n))
       (λ() ONE))
      (λ() ((MUL n) (FACT (SUB1 n))))))))
==
((λ(F)
   ((λ(f) (f f))
    (λ(f) (F (λ(x) ((f f) x))))))
 (λ(FACT)
   (λ(n)
     ((((λ(c) (λ(t) (λ(f) (((c t) f)))))
        ((λ(n) ((n (λ(dont-care-at-all) (λ(x) (λ(y) y)))) (λ(x) (λ(y) x)))) n))
       (λ() (λ(f) (λ(x) (f (((λ(f) (λ(x) x)) f) x))))))
      (λ() ((MUL n) (FACT (SUB1 n))))))))
==
((λ(F)
   ((λ(f) (f f))
    (λ(f) (F (λ(x) ((f f) x))))))
 (λ(FACT)
   (λ(n)
     ((((λ(c) (λ(t) (λ(f) (((c t) f)))))
        ((λ(n) ((n (λ(dont-care-at-all) (λ(x) (λ(y) y)))) (λ(x) (λ(y) x)))) n))
       (λ() (λ(f) (λ(x) (f (((λ(f) (λ(x) x)) f) x))))))
      (λ() (((λ(m) (λ(n) ((m ((λ(m) (λ(n) ((m (λ(n) (λ(f) (λ(x) (f ((n f) x)))))) n))) n))
                          (λ(f) (λ(x) x))))) n) (FACT (SUB1 n))))))))
==
((λ(F)
   ((λ(f) (f f))
    (λ(f) (F (λ(x) ((f f) x))))))
 (λ(FACT)
   (λ(n)
     ((((λ(c) (λ(t) (λ(f) (((c t) f)))))
        ((λ(n) ((n (λ(dont-care-at-all) (λ(x) (λ(y) y)))) (λ(x) (λ(y) x)))) n))
       (λ() (λ(f) (λ(x) (f (((λ(f) (λ(x) x)) f) x))))))
      (λ() (((λ(m) (λ(n) ((m ((λ(m) (λ(n) ((m (λ(n) (λ(f) (λ(x) (f ((n f) x)))))) n))) n))
                          (λ(f) (λ(x) x))))) n)
            (FACT ((λ(n)
                     (SND ((n (λ(r)
                                ((PAIR (ADD1 (FST r))) (FST r)))) ((PAIR ZERO) ZERO)))) n))))))))
==
|#
(define FACT3
  ((λ(F)
    ((λ(f) (f f))
     (λ(f) (F (λ(x) ((f f) x))))))
   (λ(FACT)
     (λ(n)
       ((((λ(c) (λ(t) (λ(f) (((c t) f)))))
          ((λ(n) ((n (λ(dont-care-at-all) (λ(x) (λ(y) y)))) (λ(x) (λ(y) x)))) n))
         (λ() (λ(f) (λ(x) (f (((λ(f) (λ(x) x)) f) x))))))
        (λ() (((λ(m) (λ(n) ((m ((λ(m) (λ(n) ((m (λ(n) (λ(f) (λ(x) (f ((n f) x)))))) n))) n))
                            (λ(f) (λ(x) x))))) n)
              (FACT ((λ(n)
                       ((λ(p) (p (λ(x) (λ(y) y))))
                        ((n (λ(r) (((λ(x) (λ(y) (λ(s) ((s x) y))))
                                    ((λ(n) (λ(f) (λ(x) (f ((n f) x)))))
                                     ((λ(p) (p (λ(x) (λ(y) x)))) r)))
                                   ((λ(p) (p (λ(x) (λ(y) x)))) r))))
                         (((λ(x) (λ(y) (λ(s) ((s x) y)))) (λ(f) (λ(x) x))) (λ(f) (λ(x) x)))))) n)))))))))
;; And just to be sure...
(check-expect (NUM->num (FACT3 FIVE)) 120)
(check-expect (NUM->num (FACT3 (ADD1 FIVE))) 720)

;; Which goes to show that merely because you *can* write it this way doesn't mean it's at all legible!!
;; Amusingly, if you run the code above, only one lambda in the whole expression is never evaluated.
;; That lambda corresponds to the second zero in the first row of the table for SUB1...which is indeed
;; the only value we completely ignore.