=======================[ Lambda Calculus ]=======================

Resources---pick one or two, based on your preferred learning style.
I ordered them roughly in the order from more hands-on to more mathematical,
but even so there's no telling which one works best for you until you try.

https://hbr.github.io/Lambda-Calculus/lambda2/lambda.html
https://tgdwyer.github.io/lambdacalculus/
https://lucasfcosta.com/2018/07/29/An-Introduction-to-Lambda-Calculus-Part-1.html
https://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf
https://personal.utdallas.edu/~gupta/courses/apl/lambda.pdf or https://arxiv.org/pdf/1503.09060
https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf
https://www.cs.jhu.edu/~jason/465/readings/lambdacalc.html
https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html

De Bruijn's index form of writing lambdas is absolutely crucial for understanding both lambda
calculus theory and any modern compilation: https://en.wikipedia.org/wiki/De_Bruijn_index .
You will be asked to implement parts of it.

For eLisp bytecode:
  https://rocky.github.io/elisp-bytecode.pdf 

K = \x . \y . x   [this means \x . (\y . x), lambda bodies associate to the right]
                  [  so this is (lambda (x) (lambda (y) x))                      ]

I = \x . x        [identity function]

K I -> (\x.(\y.x)) (\x'.x')  ->  \y.(\x'.x') -> \x.\y.y   [this is called KI]

We can use K and KI to represent Boolean true and false:
K   "true"
KI  "false"

With these, the ogical operators NOT, AND, OR can be realized as combinators:

-------------[ NOT ]-------------

NOT b := b false true  = (b false) true
                          ^^^^^^^^------remember that in λ-calculus functions calls associate to the left. It takes getting used to.

NOT true = (true false) true -> (\x\y.x \x'\y'.y') true  ->  \x'\y'.y' = KI/false  
                                    \y.\x'\y'.y'

NOT false = (false false) true -> (\x\y.y  \x'\y'.y') true -> (\y.y) true -> true  
                                        \y.y

Hooray, we have a NOT with the correct truth table. 

-------------[ AND ]-------------

AND a b :=  a b false  . This means ((a b) false), so we can first compute (a b) for
                           difference truth tables combinations of true and false,
			   and then apply the result to the fixed false.

   a        b                          (apply to)
  true     true                          false
(\x.\y.x  \x'.\y'.x') -> \y.\x'.\y'.x'
                                        \x''.\y''.y''  -> \x'.\y'.x' = true


  true     false                         
(\x.\y.x  \x'.\y'.y') -> \y.\x'.\y'.y'   
                                        \x''.\y''.y'' -> \x'.\y'.y' = false

  false    true
(\x.\y.y  \x'.\y'.x') -> \y.y
                                        false     -> false

  false    false
(\x.\y.y  \x'.\y'.y') -> \y.y
                                        false     -> false 

So we have the correct truth table for AND, as modeled by ((a b) KI) on K as true and KI as false.

-------------[ OR ]-------------

OR  a b :=  a true b

   a                                      b 
  true      true                           
(\x.\y.x  \x'.\y'.x') -> \y.\x'.\y'.x'
                           \y.true
                                        true   -> true
					false  -> true

  false    true
(\x.\y.y  \x'.\y'.x') ->  \y.y   
                                        true   -> true
					false  -> false


So the OR truth table also checks out!

;;;;------------------------------------------------------------------------------------

;;; We can check this in eLisp (with the caveat that with more complex combinators eLisp's
;;;   eager evaluation will get in the way; but we are fine with K, KI, and the boolean ops)

(setq K (lambda (x)
	  (lambda (y) x)))
(closure (t) (x) #'(lambda (y) x))

(setq KI (lambda (x)
	   (lambda (y) y)))
(closure (t) (x) #'(lambda (y) y))

(funcall K KI)
(closure ((x closure (t) (x) #'...) t) (y) x)

(funcall (funcall K KI) K)
(closure (t) (x) #'(lambda (y) y))

;;; Due to the way eLisp closures are readable (see https://nullprogram.com/blog/2013/12/30/),
;;;   we can even compare the results with equals (when simple enough):

(equal (funcall (funcall K KI) K)
       KI)
t

(equal (funcall (funcall KI KI) K)
       K)
t

(equal (funcall (funcall KI KI) K)
       KI)
nil

(equal (funcall (funcall K KI) K)
       K)
nil

;; AND a b = (a b) false

(funcall (funcall K K) KI)   ; K , i.e. true AND true -> true
(closure (t) (x) #'(lambda (y) x))

(funcall (funcall K KI) KI) ; KI , i.e. true AND false -> false
(closure (t) (x) #'(lambda (y) y))

(funcall (funcall KI K) KI) ; KI , i.e. false AND true -> false
(closure (t) (x) #'(lambda (y) y))

(funcall (funcall KI KI) KI) ; KI , i.e. false AND false  -> false
(closure (t) (x) #'(lambda (y) y))

;; Check the truth table for OR!


;;; A model for natural numbers 

;; The theory of natural numbers is that there is one "base" of them (say, "0" or "1", depending
;;   on which book you read), and then all other natural numbers are made by calling the Successor
;;   function:

;; "n+1" is  Succ "n" 
;; 0
;; 1=Succ 0
;; 2=Succ (Succ 0)
;; 3=Succ (Succ (Succ 0))
;; ...
;; Note the right-associativity here: everything else in these notes and in lambda calculus
;;      notattion associtaes to the left, f g h x meaning ((f g) h) x)

"0" = \f.\x.x       <<-- a.k.a. KI
"1" = \f.\x.f x
"2" = \f.\x.f (f x)
"3" = \f.\x.f (f (f x))

Succ n = \nfx. f (n f x)

                              0                    0
Succ 0 -> (\nfx. f(n f x)) \f'x'.x' -> \fx. f( (\f'x'.x') f x ) -> \fx. f x  == 1
                                               ^^^^^^^^^^^^        <<--- left-associative
                                                  \x'.x'   
                                                  ^^^^^^^^^^^
                                                      x

                                 1                        1
Succ 1 -> (\nfx. f(n f x)) (\f'x'.f' x') -> \fx. f( (\f'x'.f' x') f x ) -> \fx.f (f x) == 2
                                                    ^^^^^^^^^^^^^^^
                                                        \x'.f x'
                                                        ^^^^^^^^^^^^^^ 
                                                             f x

                                 2                              2
Succ 2 -> (\nfx. f(n f x)) (\f'x'. f' (f' x')) -> \fx. f( (\f'x'. f' (f' x')) f x ) -> \fx.f(f(f x)) ==3  
                                                          ^^^^^^^^^^^^^^^^^^^^^
                                                                \x'.f (f x')  
                                                                ^^^^^^^^^^^^^^^^^ 
                                                                    f(f x)  

;; and so on.

;; If you are mathematically inclined, you could prove by induction that  Succ "n" -> "n+1" for any "n",
;; defined as above. We'll mention induction in class on Thursday.