# Lambda Calculus Reducer

From the book Compiling Lambda Calculus

Provided under the Creative Commons Zero (CC0) licence

```; Lambda Calculus Reducer
; By Nils M Holm, 2016
;
; Provided under the Creative Common Zero (CC0) license
; (https://creativecommons.org/publicdomain/zero/1.0/)
;
; From the book COMPILING LAMBDA CALCULUS, http://t3x.org/clc/
;
; Example: (reduce '((lam x (lam y x)) M))  ->>  (lam y2 M)

(define (alpha-conv x)

(define id 0)

(define (var x)
(set! id (+ 1 id))
(string->symbol
(string-append
(symbol->string x)
(number->string id))))

(define (bind x v e)
(cons (cons x v) e))

(define (aconv x e)
(cond ((assq x e)
=> cdr)
((not (pair? x))
x)
((eq? 'lam (car x))
`(lam ,v ,(aconv
(else
(map (lambda (x)
(aconv x e))
x))))

(aconv x '()))

(define (reduce x)

(define (subst x v m)
(cond ((eq? x v)
m)
((not (pair? x))
x)
((and (eq? (car x) 'lam)
x)
(else
(map (lambda (x)
(subst x v m))
x))))

(define (beta-conv x i)
(let ((f (car x)))
(m (red (cadr x) (+ 1 i))))
(red (subst t v m) (+ 1 i)))))

(define (lambda? x)
(and (pair? x)
(eq? 'lam (car x))))

(define (app? x)
(and (pair? x)
(lambda? (car x))))

(define (normal? x)
(cond ((not (pair? x)))
((app? x) #f)
(else
(not (memq #f (map normal? x))))))

(define (indent i)
(let loop ((i i))
(if (not (zero? i))
(begin (display "  ")
(loop (- i 1))))))

(define (red x i)
(cond ((normal? x)
x)
((app? x)
(indent i)
(display x)
(newline)
(let ((m (red (beta-conv x i) i)))
(indent i)
(display "--> ")
(display m)
(newline)
m))
(else
(red (map (lambda (x)
(red x i))
x)
i))))

(red (alpha-conv x) 0))```

## Sample Programs

```(define succ  '(lam n (lam f (lam x (f ((n f) x))))))
(define plus  '(lam m (lam n (lam f (lam x ((m f) ((n f) x)))))))
(define times '(lam m (lam n (lam f (m (n f))))))
(define exp   '(lam m (lam n (n m))))
(define pred  '(lam n (lam f (lam x
(((n (lam g (lam h (h (g f))))) (lam u x)) (lam u u))))))
(define minus `(lam m (lam n ((n ,pred) m))))

(define zero  '(lam f (lam x x)))
(define one   '(lam f (lam x (f x))))
(define two   '(lam f (lam x (f (f x)))))
(define three '(lam f (lam x (f (f (f x))))))
```