Closure-Creating Interpreters

Topics

• Environment-based evaluation: ρ ⊢ e ⇓ v
• Natural deduction rules for an extended λ-calculus
• From rules to a working interpreter
• Closures: capturing the environment at definition time

Introduction

In this lecture we will build an interpreter for a language that extends the λ-calculus with integers, arithmetic, let-binding, and if0. This lecture ties together several topics we have been studying—lambda calculus and natural deduction—and shows how to turn a mathematical specification directly into a working interpreter.

By the end of the lecture, we will have a working, Turing-complete programming language.

In the previous lecture, we studied the λ-calculus as a term rewriting system. We will return to rewriting rules and substitution after Spring break. Today, instead, we take a different approach: we give an environment-based semantics using natural deduction, and translate it directly into a Racket interpreter.

The Language

We extend the λ-calculus with integers, unary negation, binary addition, let, and if0:

e ∈ Expr ::=
    | x                              ← Variable reference
    | i                              ← Integer literal
    | (- e)                          ← Unary negation
    | (+ e₀ e₁)                     ← Binary addition
    | (if0 e_g e_t e_f)                ← Conditional (zero test)
    | (let ([x e]) e_b)              ← Let binding
    | (λ (x) e)                      ← Lambda abstraction
    | (e₀ e₁)                       ← Application

The Racket predicate expr? checks membership in this language:

(define (expr? e)
  (match e
    [(? symbol? x) #t]
    [`(,(? expr? e0) ,(? expr? e1)) #t]
    [`(λ (,(? symbol? x)) ,(? expr? e-body)) #t]
    [(? integer? i) #t]
    [`(- ,(? expr? e)) #t]
    [`(+ ,(? expr? e0) ,(? expr? e1)) #t]
    [`(let ([,(? symbol? x) ,(? expr? e)]) ,(? expr? e-b)) #t]
    [`(if0 ,(? expr? e-guard) ,(? expr? e-true) ,(? expr? e-false)) #t]
    [_ #f]))

Here are some example expressions in our language:

'((λ (x) x) 42)
'(+ 10 (- 3))
'(let ([x 5]) (+ x x))
'(let ([x 10]) (let ([y 7]) (+ x (- y))))
'(let ([x 100]) (let ([f (λ (y) (+ x y))]) (f 23)))
'(if0 0 111 222)
'(if0 (+ 1 2) 0 (+ 40 2))

The Evaluation Relation

In previous lectures we used the judgement e ⇓ v (“expression e evaluates to value v”). Now our language has variables, so we need an environment ρ that maps variables to values:

ρ ⊢ e ⇓ v   “In environment ρ, expression e evaluates to value v”

The environment ρ is a finite map from variable names to values. We write ρ(x) for looking up x in ρ, and ρ[x ↦ v] for extending ρ with a new binding.

Natural Deduction Rules

We now give the natural deduction rules for the non-lambda fragment of the language. Each rule is shown as a proof tree.

Exercise 1

Exercise 2

From Rules to Interpreter

We can read the judgement ρ ⊢ e ⇓ v as a function from (ρ, e) to v. The structure of e tells us exactly which rule to use—if e is a variable, we must use Var; if it is (+ e₀ e₁), we must use Add; and so on. Each premise that involves a recursive judgement becomes a recursive call.

This gives us a direct strategy: pattern-match on e, and for each form, translate the corresponding natural deduction rule into code.

;; interp0 : Env × Expr → Value
;; Handles everything except lambdas and application
(define (interp0 env e)
  (match e
    ;; (Var)
    [(? symbol? x)
     (hash-ref env x)]
    ;; (Int)
    [(? integer? i) i]
    ;; (Neg)
    [`(- ,e) (- (interp0 env e))]
    ;; (Add)
    [`(+ ,e0 ,e1)
     (let ([v0 (interp0 env e0)]
           [v1 (interp0 env e1)])
       (+ v0 v1))]
    ;; (If0-True) and (If0-False)
    [`(if0 ,e-guard ,e-true ,e-false)
     (let ([vg (interp0 env e-guard)])
       (if (= vg 0)
           (interp0 env e-true)
           (interp0 env e-false)))]
    ;; (Let)
    [`(let ([,x ,e0]) ,e-body)
     (let ([v (interp0 env e0)])
       (interp0 (hash-set env x v) e-body))]
    ;; Not done yet...
    [`(λ (,x) ,e) 'todo]
    [`(,e0 ,e1) 'todo]))

We can already run this interpreter on the non-lambda fragment:

(interp0 (hash) '(+ 10 (- 3)))            ;; ⟹ 7
(interp0 (hash) '(let ([x 5]) (+ x x)))   ;; ⟹ 10
(interp0 (hash) '(let ([x 10])
                    (let ([y 7])
                      (+ x (- y)))))       ;; ⟹ 3
(interp0 (hash) '(if0 0 111 222))          ;; ⟹ 111
(interp0 (hash) '(if0 (+ 1 2) 0 (+ 40 2)));; ⟹ 42

The Closure Question

Now comes the most important question of the lecture: how do we represent λ?

A first idea is to simply save the program text: represent (λ (x) (+ x 3)) as exactly (λ (x) (+ x 3)). At runtime, this would correspond to a function pointer to compiled code.

Unfortunately, this does not work. Consider:

((λ (x) (λ (y) (+ y x))) 23)

The return value is (λ (y) (+ y x)), which captures the value of x. If we only save the text, we lose the fact that x = 23. Here is another example:

(let ([x 100])
  (let ([f (λ (y) (+ x y))])
    (f 23)))

When f is called, its body (+ x y) needs x = 100, but x is not in scope at the call site—it was in scope when f was defined.

Substitution approach: The λ-calculus handles this via substitution: whenever we apply a function, we substitute the argument into the body. But substitution on a term of size n requires O(n) work, and we do it at every function call.

Closures approach: Instead, most languages use closures. A closure bundles together:

1. The raw text of the lambda: (λ (x) e)
2. The environment ρ in which the lambda was defined

We write closures as ⟨λ (x) e , ρ⟩. Intuitively, a closure is a suspended computation together with the environment necessary to run it later.

Lambda and Application Rules

Important: we evaluate the body in ρ’ (the environment from when the function was defined), not in ρ (the environment at the call site). This is called lexical scoping.

Exercise 3

Complete Interpreter

Values in our language are now either integers or closures:

(define (value? v)
  (match v
    [(? integer? i) #t]
    [`(clo (λ (,x) ,e) ,(? hash? env)) #t]
    [_ #f]))

The complete interpreter adds two cases—Lam and App—to interp0:

(define (interp1 env e)
  (match e
    ;; (Var)
    [(? symbol? x) (hash-ref env x)]
    ;; (Int)
    [(? integer? i) i]
    ;; (Neg)
    [`(- ,e) (- (interp1 env e))]
    ;; (Add)
    [`(+ ,e0 ,e1)
     (let ([v0 (interp1 env e0)]
           [v1 (interp1 env e1)])
       (+ v0 v1))]
    ;; (If0-True) and (If0-False)
    [`(if0 ,e-guard ,e-true ,e-false)
     (let ([vg (interp1 env e-guard)])
       (if (= vg 0)
           (interp1 env e-true)
           (interp1 env e-false)))]
    ;; (Let)
    [`(let ([,x ,e0]) ,e-body)
     (let ([v (interp1 env e0)])
       (interp1 (hash-set env x v) e-body))]
    ;; (Lam) — simply return a closure
    [`(λ (,x) ,e+) `(clo (λ (,x) ,e+) ,env)]
    ;; (App) — expect e0 to evaluate to a closure
    [`(,e0 ,e1)
     (match (interp1 env e0)
       [`(clo (λ (,x) ,e+) ,env+)
        (define new-env (hash-set env+ x (interp1 env e1)))
        (interp1 new-env e+)])]))

Let’s test it:

(interp1 (hash) '((λ (x) x) 42))
;; ⟹ 42

(interp1 (hash) '(let ([x 100])
                    (let ([f (λ (y) (+ x y))])
                      (f 23))))
;; ⟹ 123

(interp1 (hash) '(let ([apply (λ (f) (f 5))])
                    (apply (λ (x) (+ x 1)))))
;; ⟹ 6

(interp1 (hash) '(let ([make-adder
                         (λ (x)
                           (λ (y)
                             (+ x y)))])
                    ((make-adder 10) 7)))
;; ⟹ 17

Optional Exercises

The following exercises are optional, for extra practice building proof trees.

Advanced, Optional: Certifying Interpreters

Our interpreter directly mirrors the natural deduction rules: each match clause corresponds to exactly one rule, and each recursive call corresponds to a premise. Because of this tight correspondence, we can extend the interpreter to generate proof trees—certificates that the evaluation followed the rules correctly.

The idea: instead of returning just a value, each clause also returns a proof tree node recording which rule was applied. The extension to interp1 is minimal—every clause wraps its result in a pair (cons value proof), and recursive calls destructure these pairs with match-define. (If you haven’t seen match-define before: (match-define (cons a b) expr) binds a to the car and b to the cdr of expr.)

Formatting helpers

Expressions are plain S-expression data, so Racket’s ~a (display) prints them correctly. We only need custom formatters for environments (Racket hashes display as #hash(...)) and closures:

(define (fmt-env env)
  (if (hash-empty? env) "{}"
      (format "{~a}"
        (string-join
          (for/list ([k (sort (hash-keys env) symbol<?)])
            (format "~a ↦ ~a" k (fmt-val (hash-ref env k))))
          ", "))))

(define (fmt-val v)
  (match v
    [(? integer?) (~a v)]
    [`(clo (λ (,x) ,e) ,env)
     (format "⟨λ (~a) ~a , ~a⟩" x e (fmt-env env))]))

(define (fmt-judge env e v)
  (format "~a ⊢ ~a ⇓ ~a" (fmt-env env) e (fmt-val v)))

The certifying interpreter

Compare each clause to interp1—the evaluation logic is identical. The only change is that each clause now returns (cons value proof-node), where the proof node has the uniform shape (RuleName premise ... --- conclusion):

(define (interp-cert env e)
  (match e
    [(? symbol? x)
     (define v (hash-ref env x))
     (cons v `(Var ,(format "~a(~a) = ~a" (fmt-env env) x (fmt-val v))
                   --- ,(fmt-judge env e v)))]
    [(? integer? i)
     (cons i `(Int --- ,(fmt-judge env e i)))]
    [`(- ,e0)
     (match-define (cons v0 pf0) (interp-cert env e0))
     (define v (- v0))
     (cons v `(Neg ,pf0 ,(format "v = ~a" v)
                   --- ,(fmt-judge env e v)))]
    [`(+ ,e0 ,e1)
     (match-define (cons v0 pf0) (interp-cert env e0))
     (match-define (cons v1 pf1) (interp-cert env e1))
     (define v (+ v0 v1))
     (cons v `(Add ,pf0 ,pf1 ,(format "v = ~a + ~a" v0 v1)
                   --- ,(fmt-judge env e v)))]
    [`(if0 ,e-guard ,e-true ,e-false)
     (match-define (cons vg pfg) (interp-cert env e-guard))
     (if (= vg 0)
         (match (interp-cert env e-true)
           [(cons v pf)
            (cons v `(If0-True ,pfg ,pf
                               --- ,(fmt-judge env e v)))])
         (match (interp-cert env e-false)
           [(cons v pf)
            (cons v `(If0-False ,pfg ,(format "~a ≠ 0" vg) ,pf
                                --- ,(fmt-judge env e v)))]))]
    [`(let ([,x ,e0]) ,e-body)
     (match-define (cons v0 pf0) (interp-cert env e0))
     (match-define (cons v pf-body)
       (interp-cert (hash-set env x v0) e-body))
     (cons v `(Let ,pf0 ,pf-body --- ,(fmt-judge env e v)))]
    [`(λ (,x) ,e+)
     (define v `(clo (λ (,x) ,e+) ,env))
     (cons v `(Lam --- ,(fmt-judge env e v)))]
    [`(,e0 ,e1)
     (match-define (cons v0 pf0) (interp-cert env e0))
     (match-define (cons v1 pf1) (interp-cert env e1))
     (match v0
       [`(clo (λ (,x) ,e+) ,env+)
        (match-define (cons v pf-body)
          (interp-cert (hash-set env+ x v1) e+))
        (cons v `(App ,pf0 ,pf1 ,pf-body
                      --- ,(fmt-judge env e v)))])]))

Serializing proofs

The proof trees produced by interp-cert are nested Racket lists. A small serializer converts them to the S-expression string format that the proof tree viewer understands:

(define (proof->sexp pf)
  (match pf
    [`(,name ,@rest)
     (format "(~a)"
       (string-join
         (cons (format "(~a :right)" name)
               (for/list ([x (in-list rest)])
                 (cond
                   [(equal? x '---) "---"]
                   [(string? x) (format "\"~a\"" x)]
                   [else (proof->sexp x)])))
         " "))]))

(define (prove e)
  (proof->sexp (cdr (interp-cert (hash) e))))

Try it

Download the complete file (includes interp1, interp-cert, and the serializer): closures.rkt

Run it in DrRacket or from the command line:

racket closures.rkt

The output includes proof tree S-expressions like:

(displayln (prove '(+ 3 5)))
(displayln (prove '((λ (x) (+ x 1)) 5)))
(displayln (prove '(let ([x 10]) ((λ (y) (+ x y)) 7))))

Then paste the result into the viewer below to see the proof tree:

Summary

• We introduced the judgement ρ ⊢ e ⇓ v, which extends big-step semantics with an environment for variable bindings.

• We gave natural deduction rules for each syntactic form, and translated them directly into an interpreter by pattern-matching on the expression.

• The key insight was the move from substitution to closures. A closure ⟨λ (x) e , ρ⟩ pairs a lambda with its defining environment, enabling efficient lexical scoping without rewriting program text.

• After Spring break, we will return to the rewriting view of the λ-calculus (reduction rules and substitution) and connect it to the environment-based semantics developed today.