; 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.