; Lambda Calculus
;
; This blog post is a valid Scheme program. You can run it with a Scheme
; interpreter of your choice.
;
; The lambda calculus is a "model" of computation, meaning it is a set of
; rules that, when executed, can compute things for some formal definition
; of computation which I'll skip over here. In its most basic form, the
; lambda calculus has three types of values:
;
;   variables
;   lambda expressions (function definitions)
;   applications (function calls)
;
; Since we're going to implement a lambda calculus interpreter here, we'll
; need a concrete syntax, and since this is Scheme we'll do the following:
;
; * Variables will be symbols
; * Lambdas will be three-element lists: the symbol lam, then the variable,
;   then the function body
; * Applications will be three-element lists: the symbol app, then the
;   function, then the argument value being supplied.
;
; We'll define some predicates that recognize these three types of value, and
; that recognize values in general:

(import (scheme small) ; the base language
        (srfi 1))      ; the list library, including first/second/third

(define var? symbol?)

(define (lam? v)
  (and (list? v)
       (= (length v) 3)
       (equal? (first v) 'lam)
       (var? (second v))
       (val? (third v))))

(define lam-arg second)
(define lam-body third)

(define (app? v)
  (and (list? v)
       (= (length v) 3)
       (equal? (first v) 'app)
       (val? (second v))
       (val? (third v))))

(define app-expr second)
(define app-val third)

(define (val? v)
  (or (var? v) (lam? v) (app? v)))

; That having been done, we can easily write expressions out, like this. Note
; that we're quoting these expressions with ' so they won't be treated as
; Scheme code.

'x 'y
'(lam x x)
'(lam x (lam y x))
'(app (lam x x) (lam x x))

; That's pretty cool, but right now these are just values. We need to add some
; meaning to them - that is, to give them some semantics. We'll define a
; notion of "reducing" an expression by applying the outermost application,
; if there is one. For example, if we have:
;
;   (app (lam x (lam z z)) (lam y y))
;
; then the outermost application has function:
;
;   (lam x (lam z z))
;
; being applied to argument:
;
;   (lam y y)
;
; To reduce this application, we substitute (lam y y) in for everywhere x
; appears as a value in the body of the function, which yields:
;
;   (lam z z)
;
; since x doesn't appear anywhere in the body.
;
; However, there's a problem. Suppose that instead, we had this expression,
; which has identical meaning[1]:
;
;   (app (lam x (lam x x)) (lam y y))
;
; If we simply replace every x that is a value in the body with (lam y y),
; we'll get:
;
;   (lam x (lam y y))
;
; which is not the same thing. The problem here is that there are two
; conflicting bindings of x, and the "inner" one should be replacing the
; "outer" one and therefore the inner x in the nested lambda's body should
; not have been replaced. This behavior is called "variable shadowing" or
; "variable hiding" and will probably be familiar from most programming
; languages.
;
; To avoid this type of problem, we can do a process known as "renaming", by
; which we change the name of a specific variable within a lambda expression.
; This is not trivial to do; for example, if we were going to rename x to y
; in:
;
;   (lam x (lam x x))
;
; we should produce (lam y (lam x x)), without renaming the "inner" x. If we
; were to produce (lam y (lam x y)) the meaning of the expression would change,
; and if we were to produce (lam y (lam y y)) (i.e. replace *all* occurences
; of x) then the renaming process wouldn't help us avoid variable conflicts in
; the first place.
;
; This gives us two algorithms we're going to want: renaming and reduction. In
; actual lambda calculus, because of how computer scientists are about greek
; letters, these are called "alpha-renaming" (or "alpha-conversion") and
; "beta-reduction". Notionally, we'll use alpha-renaming to avoid variable
; conflicts while we repeatedly beta-reduce until we can beta-reduce no further.
;
; So, when do we alpha-rename, and what do we rename things to? The answer to
; the latter is obvious: "something not already used", since then it can't
; conflict with an existing variable. As for the former - we can simply rename
; function arguments when we're about to apply those functions, which is easy
; to detect and guarantees correctness. We need to be careful in the process,
; or else we might rename something that doesn't actually refer to the argument,
; but the algorithm to do it looks like this.
;
; This function renames x to n in e:
(define (rename e x n)
  (cond
    ((var? e)
     (if (equal? e x)
         n
         e))
    ((lam? e)
     (if (equal? (lam-arg e) x)
         e
         (list 'lam (lam-arg e) (rename (lam-body e) x n))))
    ((app? e)
     (list 'app (rename (app-expr e) x n) (rename (app-val e) x n)))))

; So we could now do, say:
(rename 'x 'y 'z)               ; yielding x
(rename '(lam x y) 'y 'z)       ; yielding (lam x z)
(rename '(lam x x) 'x 'z)       ; yielding (lam x x)

; As mentioned above, we want to alpha-rename when we're about to apply a
; function, and we want to alpha-rename to a fresh variable, so let's define
; a useful function, which will take a lambda expression and rename its argument
; to a fresh name within its body. First:
(define fresh-name
  (let ((i 0))
    (lambda ()
      (set! i (+ i 1))
      (string->symbol
        (string-append "fresh-" (number->string i))))))

(define (rename-arg f)
  (when (not (lam? f))
        (error "rename-arg" f))
  (let ((s (fresh-name)))
    (list 'lam s (rename (lam-body f) (lam-arg f) s))))

; Alright. Now that we've implemented renaming, there's a few different ways we
; could do beta-reduction. One approach is to rewrite terms by substitution,
; so for example if we were evaluating:
;
;   (app (lam x y) z)
;
; we'd go through y, replacing every instance of x with an instance of z. In
; fact, the rename function we have above does exactly this substitution, if
; we relax the restriction that n is a variable name and instead allow for it
; to be any expression.
;
; If we wanted to do that, it'd look like this. This function is a single step
; of the evaluation process:

(define (step-subst e)
  (cond
    ((var? e) e)
    ((lam? e) e)
    ((and (app? e) (lam? (app-expr e)))
     (rename (lam-body (app-expr e))
             (lam-arg (app-expr e))
             (app-val e)))
    ((app? e)              ; app without a lambda in the expr slot yet
     (list 'app (step-subst (app-expr e)) (app-val e)))
    (else (error "cannot beta-reduce" e))))

; And now one can write things like:

(step-subst '(app (lam x x) y))      ; evaluates to y

; Or even:

(step-subst '(app (lam x (app x x)) (lam x (app x x))))

; which yields itself, since taking
;
;   (lam x (app x x))
;
; and applying it to itself causes:
;
;   (replace '(app x x) 'x '(lam x (app x x)))
;
; which is, of course, (app (lam x (app x x)) (lam x (app x x))) again.

; There's a problem, though: this function only steps once. In theory, we'd
; like to write something like this:
;
;   (define (eval-subst e)
;     (if (done? e)
;         e
;         (eval-subst (step-subst e))))
;
; but it's not so clear how to write that done? predicate. In fact, to do so
; we'll have to introduce the notion of a "normal form", and then repeatedly
; step our evaluator until we reach a normal form... but that can wait for
; next time. Thanks for reading :)

; [1]: Specifically, it has identical meaning because it is alpha-equivalent
;      to the previous example, or because the two forms can be renamed into
;      each other.