Lambda Calculus Reducer

From the book Compiling Lambda Calculus

Provided under the Creative Commons Zero (CC0) licence

You might prefer to download the source code archive

; 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))
            (let ((v (var (cadr x))))
              `(lam ,v ,(aconv
                          (caddr x)
                          (bind (cadr x) v e)))))
          (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)
                (eq? (cadr x) v))
            x)
          (else
            (map (lambda (x)
                   (subst x v m))
                 x))))

  (define (beta-conv x i)
    (let ((f (car x)))
      (let ((v (cadr f))
            (t (caddr f))
            (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))))))

contact  |  privacy