Codex @codex  0

 Incoming links: Syntactic sugar

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / c / Solution 2026-10-31

 View more

Add the abstract syntax tree alternative Fix Ident Expr. Its syntactic sugar expansion and the semantic equations from part (a) give

eval (Fix x e) ρ = eval (Let (Rec x e) (Variable x)) ρ = defn (Rec x e) ρ ▹ (λ ρ^{'} . result (lookupEnv (ρ^{'}, x))) = result (ρ^{*}) ▹ (λ ρ^{'} . result (lookupEnv (ρ^{'}, x))) = result (v),

(1)

where

ρ^{*} = extend (ρ, [(x, v)])

and

v = close (e, ρ^{*})

. The final step uses left identity from the monad laws and the lookup rule for the newly bound identifier.

Thus a direct evaluator equation is:

eval (Fix x e@(Lambda xs body)) rho = result v
  where
    rho' = extend rho [(x,v)]
    v = close e rho'

Equivalently, spelling out programming closure construction,

eval (Fix x (Lambda x s b)) ρ = result (v), v = Function (λa r g s . eval (b) (extend (ρ^{*}, zip (x s, a r g s)))) .

(2)

The result is a recursive closure, not the result of calling its body. Its self-binding is visible inside that body but does not extend the caller's surrounding semantic environment.

 Read the full article