;; In this note, we take a look at the famous Y combinator.
;;   Read about Lambda calculus in 4.2 of the Mitchell textbook,
;;   then read the Wikipedia page---it has surprisingly good
;;   examples: https://en.wikipedia.org/wiki/Lambda_calculus

;; Pay special attention to the explanations of
;;   free vs bound variables, and the "Reduction" subsection.  

;; A note on the presumed order of grouping: \a.\b.\c.\d a b c d 
;;   means \a.(\b.(\c.(\d. ((a b) c) d) . For function application,
;;   "a b c" means "((a b) c)" , and is different from "a (b c)". 
;;   This is just a convention for what to do when functions
;;   can be applied to functions: in what order to apply them.
;;   It might seem that the other way would be more natural, but it
;;   actually ends up in heavier formulas.

;; ------------------------------------------------------------------
;; In the class, we looked at the example of how to read \x.\x.x 
;;   (I will be writing \ for λ because Haskell uses that notation;
;;   imagine that \ has a tiny leg making it into a λ). This should be
;;   read as \x.(\x.x) (well, λx.(λx.x), but you get the idea).
;; 
;; In this example, the 3rd x is bound to the inner \x (the 2nd 
;;   occurrence of x). whereas the outer \x (1st occurrence of x)
;;   is not bound to anything. In other words, this is exactly
;;   like (lambda (x) (lambda (x) x)): if you apply it, the first
;;   "x" argument will be ignored:

;$ gcl
;>(funcall ((lambda (x) (lambda (x) x)) 'a) 'b)
; 
; B
;
;$ sbcl 
;CL-USER(1): (funcall ((lambda (x) (lambda (x) x)) 'a) 'b)
;
; in: FUNCALL ((LAMBDA (X) (LAMBDA (X) X)) 'A)
;     ((LAMBDA (X) (LAMBDA (X) X)) 'A)
; ==>
;   (SB-C::%FUNCALL (LAMBDA (X) (LAMBDA (X) X)) 'A)
; 
; caught STYLE-WARNING:
;   The variable X is defined but never used.
; 
; compilation unit finished
;   caught 1 STYLE-WARNING condition
;
; B
;; ------------------------------------------------------------------

;; Note that SBCL even tries to warn you that you don't use one
;;  of the X variables!

;; So you can rewrite (alpha-reduce, in fancy terms) \x.\x.x as 
;;   \y.\x.x or as \x.\y.y --- but not as \y.\x.y 

;; Work through the next example: that \x.\y.x cannot have "x" replaced
;;   by "y", giving \y.\y.y . Indeed, the former is a function of x and y
;;   that ignores its second argument and returns the second, 
;;   whereas the latter, as we just saw, is a function that ignores 
;;   the first and returns the second!

;; Figuring out such notation can be frustrating. This is why the Dutch 
;;  logician Nicolaas De Bruijn came up with a way of writing lambda 
;;  expressions with no named variables at all! His method very much
;;  resembles what Elisp does when compiling references to arguments
;;  of its lambdas: discards the names and goes by numbers (positions 
;;  of arguments on the stack).

;; read the first screenful of examples in 
;;   https://en.wikipedia.org/wiki/De_Bruijn_index :
;;   - \x.\y.x is \\ 2                               [i.e.,  λ λ 2]
;;   - \x.\y.\z.x z (y z) is \\\ 3 1 (2 1)           [i.e.,  λ λ λ 3 1 (2 1)]
;;   - λz. (λy. y (λx. x)) (λx. z x) is λ (λ 1 (λ 1)) (λ 2 1)

;; When in doubt, write and run it in LISP! :)

;; If you are curious, in Haskell the equivalent of 
;;  ((lambda (x) (+ x 1)) 5) => 6 is
;;      (\x -> x+1) 5        => 6

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

;;   Y combinator  

;;----------------------------------------------------------------------------
;; Building up recursion with pure lambdas: 

;; Let's say we want to try writing a recursive lambda. But of course
;;  a lambda is an _anonymous_ function: it has no name. So it cannot
;;  refer to itself in its body: there's nothing in the language to
;;  refer to itself by! Of course, LABELS exists exactly to solve this
;;  problem, and DEFUN must also work around it, but both include
;;  some tricky side-effects on the symbols being defined. What if
;;  we wanted to make do with just lambdas?

;; It's a fundamental property of nature that we can actually achieve
;;  recursion with just lambdas. The most generic way of doing so
;;  is the "Y combinator", but it can also be done in case-by case basis
;;  for every function that we want to recurse.

;; A first step is writing a lambda of two arguments, f and n, that
;;  looks _almost_ like a recursive function. It must call "f" in its
;;  body, except "f" is the argument of an enclosing lambda:

;; let's call this a "proto-recursive lambda"
(lambda (f)
  (lambda (n)
    (if (zerop n)
        1
        (* n (funcall f (1- n))))))

;; So far so good, but we can't really call it as we call a normal
;;  function. We want "f" to refer to the function _itself_,
;;  arithmetic and all, but that means we need to apply it to itself
;;  somehow when we call it the first time. And then we want the next
;;  expansion to apply itself again, and again. So we need _two_
;;  self-applications: one at the top level, and one in the body.

;; The formal proof of the Y combinator gives us hope that such
;;  perpetual rewriting---until we run into a bounding condition
;;  like 0 for an integer argument or a nil for a list---is possible.

;; So here are two examples that work:
 
;; factorial:
(funcall 
 ((lambda (h) (funcall h h))  ; top self-application
  (lambda (f)
    (lambda (n)
      (if (zerop n)
          1
          (* n (funcall (funcall f f) (1- n)))))))  ; second self-application
 5) ;                   ^^^^^^^^^^^^^  <--- we want just f here in a normal recursive DEFUN!
; => 120, test for others!

;; list length:
(funcall 
 ((lambda (h)
    (funcall h h))
  (lambda (f)
    (lambda (l)
      (cond
        ((null l) 0 )
        (t (1+
            (funcall (funcall f f)
                     (cdr l))))))))
 '(a b c d e))
; => 5, test for others!

;; So, the amazing thing is that this works. Work through these examples by hand
;;  to get a feel for why!

;; These examples are adapted from Scheme examples in 
;;   https://stackoverflow.com/questions/10499514/y-combinator-discussion-in-the-little-schemer/11864862#11864862
;; and
;;   https://stackoverflow.com/questions/7719004/in-scheme-how-do-you-use-lambda-to-create-a-recursive-function .
;; Both of these provide good explanations of why this works.

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

;; The Y combinator is the general way of injecting a self-application
;;  into a function written as the "proto-recursive" lambda above. 
 
;; This simple form of Y suffices for single-argument recursive lambdas:
(defun Y1 (f)
  (funcall (lambda (x) (funcall x x))
           (lambda (y)
             (lambda (z)  ; this extra lambda requires additional explanation
               (funcall
                (funcall f (funcall y y)) 
                z)))))

;; This works! Notice that the factorial is written with just a single "f", with 
;;   no tricky self-application---the two self-applications needed are taken care of in Y1.
(funcall 
 (Y1 
  (lambda (f)
    (lambda (n)
      (if (zerop n)
          1
          (* n (funcall f (1- n)))))))
 5)
; => 120  

;; Same deal for list length:
(funcall 
 (Y1 
  (lambda (f)
    (lambda (lst)
      (cond ((null lst) 0)
            (t (1+ (funcall f (cdr lst))))))))
 '(a b c d))
; => 4

;; A more general form, for functions with more than one argument: 
(defun Y (f)
  (funcall (lambda (x) (funcall x x))
           (lambda (y)
             (funcall f (lambda (&rest args)
                          (apply (funcall y y) args))))))

;; or a different form, with the extra lambda in a different position:
(defun Y2 (f)
  (funcall (lambda (x) (funcall x x))
           (lambda (y)
             (lambda (&rest args)
               (apply
                (funcall f (funcall y y)) 
                args)))))

;; works for single-argument functions, obviously:
(funcall 
 (Y 
  (lambda (f)
    (lambda (n)
      (if (zerop n)
          1
          (* n (funcall f (1- n)))))))
 8)
;=> 40320

(funcall 
 (Y2 
  (lambda (f)
    (lambda (n)
      (if (zerop n)
          1
          (* n (funcall f (1- n)))))))
 8)

;; But also works for lambdas of arity 2:

(funcall 
 (Y2
  (lambda (f)
    (lambda (n acc)
      (if (zerop n)
          acc
          (funcall f (1- n) (* n acc))))))
 5 1)
;=> 120

(funcall 
 (Y
  (lambda (f)
    (lambda (n acc)
      (if (zerop n)
          acc
          (funcall f (1- n) (* n acc))))))
 5 1)
;=> 120

(funcall 
 (Y1
  (lambda (f)
    (lambda (lst acc)
      (if (null lst)
          acc
          (funcall f (cdr lst) (1+ acc)))))) 
 '(a b c d) 0)
;=> 4

;; The above would fail for Y1, with an arity ("wrong number of arguments") error. 

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

;; The extra lambda is important. The reason for this is the so-called "applicative" 
;;   order of argument evaluation in LISP and Scheme: all arguments are evaluated 
;;   before the function call. In the theoretical Y-combinator as above, this
;;   causes infinite recursion before the specialized function for the particular task
;    (the "proto-recursive lambda" fed to it, or "g" in the in-class derivation)
;;   comes into play at all. So we need to postpone the call to that function with that
;;   extra lambda.  

;; So this doesn't work, runs into an infinite loop

(defun Y3 (f)
  (funcall (lambda (x) (funcall x x))
           (lambda (y)
               (funcall
                (funcall f (funcall y y)) 
))))

; This runs out of stack:
(funcall (Y3 (lambda (f)
              (lambda (n)
                (if (zerop n)
                    1
                    (* n (funcall f (1- n)))))))
         3) ; or for 2 or for 1 or for 0, still infinite looping.

; This too loops forever, despite not really being recursive at all (always returning 0):
(funcall (Y3 (lambda (f)
              (lambda (n) 0))))

;; The culprit is the "applicative" order of evaluation in LISP/Scheme
;;   vs the implicit "normal" one in classic Lambda calculus:
;; https://stackoverflow.com/questions/7719004/in-scheme-how-do-you-use-lambda-to-create-a-recursive-function
;; https://stackoverflow.com/questions/16258308/two-layer-y-style-combinator-is-this-common-does-this-have-an-official-name

; Whereas this works:
(funcall (Y1 (lambda (f)
              (lambda (n) 0)))
         0)
;=> 0 

(funcall (Y2 (lambda (f)
              (lambda (n) 0)))
         0)
;=> 0