Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / c

Add the abstract syntax tree alternative Fix Ident Expr. Its syntactic sugar expansion and the semantic equations from part (a) givewhere ${\rho }^{\ast }=\mathrm{extend}(\rho ,[(x,v)])$ and $v=\mathrm{close}(e,{\rho }^{\ast })$. 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,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.