A syntactic-reduction-based interpreter for the lambda-calculus

lambda-reduce.rkt

#lang racket

; A simple CBV syntactic reduction machine for the lamda-calculus.

; + numbers

; <exp> ::= <var>
;        |  <num>
;        |  (λ (<var>) <exp>)
;        |  (+ <exp> <exp>)
;        |  (<exp> <exp>)


; <var> is a single symbol

; Example: ((λ (f) (f f)) (λ (g) (g g)))


; Substitution (!not capture-avoiding!)

; {a/v}n  => n

; {a/v}v  => a
; {a/v}v' => v'     (v' != v)

; {a/v}(λ (v) e) => (λ (v) e)
; {a/v}(λ (v') e) => (λ (v') {a/v}e)        (v' != v)

; {a/v}(+ f e) => (+ {a/v}f {a/v}e)

; {a/v}(f e) => ({a/v}f {a/v}e)


(define (sub var arg exp)
  (match exp
    [(? number?)  exp]
    
    [(? symbol?)  (if (eq? var exp)
                      arg
                      exp)]
    
    [`(λ (,v) ,e) (if (eq? v var)
                      `(λ (,v) ,e)
                      `(λ (,v) ,(sub var arg e)))]
    
    [`(+ ,e1 ,e2)     `(+ ,(sub var arg e1)
                          ,(sub var arg e2))]
    
    [`(,f ,e)     `(,(sub var arg f)
                    ,(sub var arg e))]))
                       
     
; β-reduction

; ((λ (v) e) a) => {a/v}e

(define (β exp)
  (match exp
    [`((λ (,v) ,e) ,a)
     (sub v a e)]))


(define (atom? exp)
  (match exp
    [`(λ (,_) ,_)  #t]
    [(? number?)   #t]
    [(? symbol?)   #t]
    [else          #f]))



; call-by-value (strict) reduction:

(define (reduce exp)
  (match exp
    [(? symbol?)   exp]
    [(? number?)   exp]
    [`(λ (,v) ,e)  exp]
    
    [`(+ ,(and e1 (? number?)) ,(and e2 (? number?)))
     (+ e1 e2)]
    
    [`(+ ,e1 ,e2)
     `(+ ,(reduce e1) ,(reduce e2))]
    
    [`((λ (,v1) ,e1) ,(? atom?))
     ;=>
     (β exp)]
    
    [`((λ (,v1) ,e1) ,a)
     ;=>
     `((λ (,v1) ,e1) ,(reduce a))]
    
    [`(,f ,a)
     ;=>
     `(,(reduce f) ,a)]))



; reduce* reduces until there's no more:

(define (reduce* exp)
  
  (define next (reduce exp))
  
  (if (equal? exp next)
      next
      (reduce* next)))
    

; Example:

(reduce* `((λ (x) (+ x 3)) 10))