Lambda calculus implementation in Scheme

Lambda calculus is a formal system for representing computation. As with most formal systems and mathematics, it relies heavily on substitution.

We will start by implementing a subst procedure that accepts an expression e, a source src and a destination dst which will replace all occurences of src with dst in e.

(define (subst e src dst)
  (cond ((equal? e src) dst)
        ((pair? e) (cons (subst (car e) src dst)
                         (subst (cdr e) src dst)))
        (else e)))

Trying it a couple of times:

> (subst '(lambda (x) x) 'x 'y)
'(lambda (y) y)
> (subst '(lambda (x) x) '(lambda (x) x) 'id)
'id

Next, based on this substitution we need to implement a beta-reduce procedure that, for a lambda expression will reduce to , that is, with all within replaced to .

Our procedure will consider 3 cases:

1. Lambda expression that accepts zero args – in which case we just return the body without any substitutions
2. Lambda expression that accepts a single argument – in which case we substitute every occurrence of that argument in the body with what’s passed to the expression and return the body
3. Lambda expression that accepts multiple arguments – in which case we substitute every occurrence of the first argument in the body with what’s passed to the expression and return a new lambda expression

Before implementing the beta reducer, we will implement a predicate lambda-expr? that returns true if the expression is a lambda expression, and false otherwise:

(define (lambda-expr? e)
  (and (pair? e)
       (equal? (car e) 'lambda)
       (list? (cadr e))))

Here’s the helper procedure which accepts a lambda expression e and a single argument x to pass to the expression:

(define (beta-reduce-helper e x)
  (cond ((and (lambda-expr? e)
              (pair? (cadr e))
              (pair? (cdadr e)))
         ; lambda expr that accepts multiple args
         (list 'lambda
               (cdadr e)
               (subst (caddr e) (caadr e) x)))
        ((and (lambda-expr? e)
              (pair? (cadr e)))
         ; lambda expr that accepts a single arg
         (subst (caddr e) (caadr e) x))
        ((and (lambda-expr? e)
              (equal? (cadr e) '()))
         ; lambda expr with zero args
         (caddr e))
        (else e)))

Then, our procedure beta-reduce will accept variable number of arguments, and apply each one of them to beta-reduce-helper:

(define (beta-reduce l . xs)
  (if (pair? xs)
      (apply beta-reduce
             (beta-reduce-helper l (car xs))
             (cdr xs))
      l))

Testing these with a few cases:

> (beta-reduce '(lambda (x y) x) 123)
'(lambda (y) 123)
> (beta-reduce '(lambda (x y) y) 123)
'(lambda (y) y)
> (beta-reduce '(lambda (x) (lambda (y) x)) 123)
'(lambda (y) 123)
> (beta-reduce '(lambda (x) (lambda (y) y)) 123)
'(lambda (y) y)

However, note this case:

> (beta-reduce '(lambda (n f x) (f (n f x))) '(lambda (f x) x))
'(lambda (f x) (f ((lambda (f x) x) f x)))

It seems that we can further apply beta reductions to simplify that expression. For that, we will implement lambda-eval that will recursively evaluate lambda expressions to simplify them:

(define (lambda-eval e)
  (cond ((can-beta-reduce? e) (lambda-eval (apply beta-reduce e)))
        ((pair? e) (cons (lambda-eval (car e))
                         (lambda-eval (cdr e))))
        (else e)))

But, what does it mean for an expression e to be beta reducible? The predicate is simply:

(define (can-beta-reduce? e)
  (and (pair? e) (lambda-expr? (car e)) (pair? (cdr e))))

Great. Let’s try a few examples now:

> ; Church encoding: 1 = succ 0
> (lambda-eval '((lambda (n f x) (f (n f x))) (lambda (f x) x)))
'(lambda (f x) (f x))
> ; Church encoding: 2 = succ 1
> (lambda-eval '((lambda (n f x) (f (n f x))) (lambda (f x) (f x))))
'(lambda (f x) (f (f x)))
> ; Church encoding: 3 = succ 2
> (lambda-eval '((lambda (n f x) (f (n f x))) (lambda (f x) (f (f x)))))
'(lambda (f x) (f (f (f x))))

There’s our untyped lambda calculus 🙂

There are a couple of improvements that we can do, for example implement define within the system to define variables with values. Another neat addition would be to extend the system with a type checker.

EDIT: As noted by a reddit user, the substitution procedure is not considering free/bound variables. Here’s a gist that implements that as well.