# 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 $(\lambda x . t) s$ will reduce to $t[x := s]$, that is, $t$ with all $x$ within $t$ replaced to $s$.

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.

Advertisements