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:

- Lambda expression that accepts zero args – in which case we just return the body without any substitutions
- 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
- 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.