Operational & Denotational Semantics

Consider the C expression i++ + i++. Every C programmer knows it is undefined behavior, but why? The C standard says the order of side effects between sequence points is unspecified — but to state that precisely, you need a formal model of what 'order of side effects' means in the first place. Natural language is too ambiguous.

Formal semantics solves this by giving a program a mathematical denotation — an object in some precisely defined mathematical universe. Once that is done:

• Equivalence becomes set/function equality: two programs are equivalent iff their denotations are equal.
• Correctness of compilation becomes: the compiled program's denotation equals the source program's denotation.
• Type soundness becomes: if the type system accepts a program, its denotation satisfies a safety predicate.

The three main styles differ in what mathematical universe they use:

All three are provably interchangeable for a well-behaved language — one of the landmark results in the field.

Before writing semantic rules, we need a language to give semantics to. The standard teaching vehicle is IMP (short for imperative), also called WHILE in some texts. Its grammar is deliberately tiny so that semantic complexity cannot hide behind syntactic noise.

Syntax:

a ::= n | x | a + a | a - a | a * a          -- arithmetic expressions
b ::= true | false | a = a | a ≤ a | ¬b | b ∧ b   -- boolean expressions
c ::= skip | x := a | c ; c                 -- commands
    | if b then c else c
    | while b do c

Here n is an integer literal, x is a variable name, and c is a command (statement).

A state σ : Var → ℤ is a total function mapping variable names to integers. All semantic definitions will be parameterized by a state. This captures the idea that a command changes the store — it transforms one state into another.

The syntax is abstract: we work with the parse tree (abstract syntax tree, AST), not the raw string. Every semantic rule operates on AST nodes.

# Python encoding of IMP ASTs
from dataclasses import dataclass
from typing import Union

@dataclass
class Num:   n: int
@dataclass
class Var:   x: str
@dataclass
class Add:   left: 'AExp'; right: 'AExp'
@dataclass
class Sub:   left: 'AExp'; right: 'AExp'

@dataclass
class Skip: pass
@dataclass
class Assign: x: str; a: 'AExp'
@dataclass
class Seq:   c1: 'Cmd'; c2: 'Cmd'
@dataclass
class If:    b: 'BExp'; c1: 'Cmd'; c2: 'Cmd'
@dataclass
class While: b: 'BExp'; body: 'Cmd'

# A state is just a dict
sigma = {'x': 5, 'y': 3}

Big-step semantics, introduced by Gilles Kahn in 1987 (hence also called natural semantics), defines what a program evaluates to in one big step. You write judgments of the form:

• ⟨a, σ⟩ ⇓ₐ n — arithmetic expression a evaluates to integer n in state σ
• ⟨b, σ⟩ ⇓_b t — boolean expression b evaluates to truth value t in state σ
• ⟨c, σ⟩ ⇓ σ' — command c, started in state σ, terminates and leaves state σ'

These judgments are defined by a set of inference rules in the Gentzen style:

         (premises)
    ─────────────────  (rule name)
        (conclusion)

A rule with no premises is an axiom.

Selected rules for arithmetic:

────────────────  (Num)       ───────────────────────  (Var)
⟨n, σ⟩ ⇓ₐ n                  ⟨x, σ⟩ ⇓ₐ σ(x)

⟨a₁, σ⟩ ⇓ₐ n₁    ⟨a₂, σ⟩ ⇓ₐ n₂
─────────────────────────────────────  (Add)
      ⟨a₁ + a₂, σ⟩ ⇓ₐ n₁+n₂

Selected rules for commands:

─────────────────────  (Skip)
⟨skip, σ⟩ ⇓ σ

        ⟨a, σ⟩ ⇓ₐ n
──────────────────────────────  (Assign)
⟨x := a, σ⟩ ⇓ σ[x ↦ n]

⟨c₁, σ⟩ ⇓ σ'    ⟨c₂, σ'⟩ ⇓ σ''
───────────────────────────────────  (Seq)
        ⟨c₁;c₂, σ⟩ ⇓ σ''

⟨b, σ⟩ ⇓_b true    ⟨c₁, σ⟩ ⇓ σ'
────────────────────────────────────  (If-True)
⟨if b then c₁ else c₂, σ⟩ ⇓ σ'

⟨b, σ⟩ ⇓_b false    ⟨c₂, σ⟩ ⇓ σ'
────────────────────────────────────  (If-False)
⟨if b then c₁ else c₂, σ⟩ ⇓ σ'

        ⟨b, σ⟩ ⇓_b false
───────────────────────────────────────  (While-False)
⟨while b do c, σ⟩ ⇓ σ

⟨b,σ⟩⇓_b true  ⟨c,σ⟩⇓σ'  ⟨while b do c, σ'⟩⇓σ''
─────────────────────────────────────────────────  (While-True)
           ⟨while b do c, σ⟩ ⇓ σ''

A derivation tree is a finite tree of rule applications whose root is the desired judgment and whose leaves are axioms. The existence of such a tree is the proof that the program produces that output.

Key insight: big-step semantics naturally models termination — a judgment ⟨c, σ⟩ ⇓ σ' exists only if c terminates. A non-terminating program (like while true do skip) has no derivation, so there is no σ' such that ⟨while true do skip, σ⟩ ⇓ σ'. This is elegant but also a limitation: big-step semantics cannot easily talk about intermediate states or infinite computations.

# Big-step evaluator in Python — directly mirrors the inference rules
def eval_aexp(a, sigma):
    match a:
        case Num(n):        return n
        case Var(x):        return sigma[x]
        case Add(l, r):     return eval_aexp(l, sigma) + eval_aexp(r, sigma)
        case Sub(l, r):     return eval_aexp(l, sigma) - eval_aexp(r, sigma)

def eval_cmd(c, sigma):
    match c:
        case Skip():        return sigma
        case Assign(x, a):  return {**sigma, x: eval_aexp(a, sigma)}
        case Seq(c1, c2):   return eval_cmd(c2, eval_cmd(c1, sigma))
        case If(b, c1, c2): return eval_cmd(c1 if eval_bexp(b,sigma) else c2, sigma)
        case While(b, body):
            if not eval_bexp(b, sigma):
                return sigma  # While-False
            sigma2 = eval_cmd(body, sigma)  # While-True, first iteration
            return eval_cmd(While(b, body), sigma2)  # recursive big step

Small-step semantics (SOS), introduced by Gordon Plotkin in his landmark 1981 Aarhus notes, defines computation as a sequence of small reduction steps. Instead of one big judgment that goes from program to final value, we have a binary reduction relation on configurations.

A configuration is a pair ⟨c, σ⟩ (a command plus a state), or just σ (a terminal state, meaning the program is done). The reduction relation → is a relation on configurations:

⟨c, σ⟩ → ⟨c', σ'⟩    -- one step: c makes one computational move
⟨c, σ⟩ → σ'           -- one step that also terminates

Selected small-step rules:

          ⟨a, σ⟩ →ₐ n
    ──────────────────────────────  (Assign)
    ⟨x := a, σ⟩ → σ[x ↦ n]

    ──────────────────────  (Skip-Seq)
    ⟨skip;c₂, σ⟩ → ⟨c₂, σ⟩

           ⟨c₁, σ⟩ → ⟨c₁', σ'⟩
    ────────────────────────────────────  (Seq-Step)
    ⟨c₁;c₂, σ⟩ → ⟨c₁';c₂, σ'⟩

    ──────────────────────────────────────────────────  (While-Unfold)
    ⟨while b do c, σ⟩ → ⟨if b then (c; while b do c) else skip, σ⟩

The reflexive-transitive closure →* relates a configuration to any configuration reachable in zero or more steps. A program terminates iff ⟨c, σ⟩ →* σ' for some final state σ'.

Why small-step is more expressive than big-step:

1. Intermediate states are first-class — you can define invariants that must hold at every step, which is needed for reasoning about concurrent programs.
2. Non-termination is observable — you can say a program diverges by showing ⟨c, σ⟩ has an infinite reduction sequence.
3. Interleaving concurrency — add a rule that picks one of two concurrent threads to step; big-step cannot express this.
4. Exception handling and continuations are easier to express.

Confluence and determinism: For IMP, the reduction relation is deterministic — there is at most one rule applicable at each step. Proving determinism is a good exercise; it requires showing the rules are mutually exclusive.

# Small-step reducer for a subset of IMP
# Returns (new_cmd_or_None, new_sigma) — None means terminal
def step(c, sigma):
    match c:
        case Assign(x, a):
            n = eval_aexp(a, sigma)
            return (None, {**sigma, x: n})  # terminal step

        case Seq(Skip(), c2):
            return (c2, sigma)              # Skip-Seq: discard skip

        case Seq(c1, c2):
            result = step(c1, sigma)
            if result is None:
                return (c2, sigma)          # c1 terminated
            c1p, sigmap = result
            return (Seq(c1p, c2), sigmap)   # Seq-Step

        case While(b, body):
            # Unfold: while b do c  ≡  if b then (c; while b do c) else skip
            return (If(b, Seq(body, c), Skip()), sigma)

def run(c, sigma):
    """Drive small-step until termination."""
    while True:
        result = step(c, sigma)
        if result is None:
            return sigma
        c, sigma = result

Big-step and small-step semantics are two descriptions of the same thing — for a terminating program, they agree. This is a theorem, not an assumption:

Theorem (Equivalence): For any command c and states σ, σ':

⟨c, σ⟩ ⇓ σ'   ⟺   ⟨c, σ⟩ →* σ'

The proof goes by mutual induction on the structure of derivations in each direction. This is one of the first non-trivial theorems you prove about a formal semantics, and the technique — structural induction on derivation trees — recurs everywhere.

Trade-off table:

Which to use? In practice:

• Use big-step when you only care about the input/output relationship (type soundness proofs, definitional interpreters).
• Use small-step when you need to reason about intermediate computation (concurrent programs, transactional memory, debuggers, cost models).

Many research papers give both, prove them equivalent, then use whichever is convenient for each lemma.

Denotational semantics, developed by Dana Scott and Christopher Strachey (Oxford, late 1960s), takes a radically different approach: instead of describing how a program runs, it maps every program to a pure mathematical object — its denotation.

For IMP:

• An arithmetic expression a denotes a function ⟦a⟧ : State → ℤ
• A boolean expression b denotes a function ⟦b⟧ : State → 𝔹
• A command c denotes a partial function ⟦c⟧ : State ⇀ State (partial because the command might not terminate)

The denotation is defined compositionally — the meaning of a compound program is built from the meanings of its parts. This is the compositionality principle, and it is what makes denotational semantics special: you can reason about a program fragment in isolation.

Denotation of expressions:

⟦n⟧(σ)         = n
⟦x⟧(σ)         = σ(x)
⟦a₁ + a₂⟧(σ)  = ⟦a₁⟧(σ) + ⟦a₂⟧(σ)

Denotation of commands:

⟦skip⟧         = id   (the identity function)
⟦x := a⟧(σ)   = σ[x ↦ ⟦a⟧(σ)]
⟦c₁;c₂⟧       = ⟦c₂⟧ ∘ ⟦c₁⟧   (function composition)
⟦if b then c₁ else c₂⟧(σ) =
    ⟦c₁⟧(σ)  if ⟦b⟧(σ) = true
    ⟦c₂⟧(σ)  if ⟦b⟧(σ) = false

The challenge: while loops. What is ⟦while b do c⟧? A while loop is the iteration of a body — c applied 0, 1, 2, ... times, stopping when b becomes false. But if the loop never terminates, the function is undefined on that input. We need a mathematical device to handle this: the least fixed point.

Define the functional F : (State ⇀ State) → (State ⇀ State) by:

F(f)(σ) = σ           if ⟦b⟧(σ) = false
F(f)(σ) = f(⟦c⟧(σ))  if ⟦b⟧(σ) = true
F(f)(σ) = ⊥            if ⟦b⟧(σ) = true and ⟦c⟧(σ) is undefined

Then ⟦while b do c⟧ = lfp(F) — the least fixed point of F.

This is mathematically precise and handles non-termination by making the denotation a partial function (undefined on non-terminating inputs). The key tool that makes this work is Scott's domain theory.

# Denotational semantics in Python (partial functions as dicts or None-returning callables)
from functools import reduce

def denote_aexp(a):
    """Returns a function State -> int"""
    match a:
        case Num(n):        return lambda sigma: n
        case Var(x):        return lambda sigma: sigma[x]
        case Add(l, r):     la, ra = denote_aexp(l), denote_aexp(r)
                            return lambda sigma: la(sigma) + ra(sigma)

def denote_cmd(c):
    """Returns a partial function State -> State | None (None = diverge)"""
    match c:
        case Skip():        return lambda sigma: sigma
        case Assign(x, a):  da = denote_aexp(a)
                            return lambda sigma: {**sigma, x: da(sigma)}
        case Seq(c1, c2):   d1, d2 = denote_cmd(c1), denote_cmd(c2)
                            def seq(sigma):
                                s = d1(sigma)
                                return d2(s) if s is not None else None
                            return seq
        case While(b, body):
            db = denote_bexp(b)
            dc = denote_cmd(body)
            # Compute lfp by iterating F from the bottom (empty function)
            # This terminates only for the finite approximation; real lfp is a limit
            def F(f):
                def step(sigma):
                    if not db(sigma): return sigma
                    s = dc(sigma)
                    return f(s) if s is not None else None
                return step
            # Approximate lfp with a fixed iteration bound (for illustration)
            f = lambda sigma: None  # bottom: diverges everywhere
            for _ in range(1000):   # 1000-step approximation
                f = F(f)
            return f

The while loop's denotation requires the least fixed point of a functional. Why does such a point exist, and what does 'least' mean? This is the contribution of domain theory, developed by Dana Scott (1969) to give denotational semantics a sound mathematical foundation.

The key ideas:

1. Partial order on partial functions. Define f ⊑ g (f is 'less informative than' g) iff for all x, if f(x) = v then g(x) = v. Intuitively, g computes everything f computes and possibly more. The bottom element ⊥ is the everywhere-undefined function.

2. Chains and completeness. A chain is a sequence f₀ ⊑ f₁ ⊑ f₂ ⊑ ... The least upper bound (lub) of a chain f_n is the function that takes each input to the value it eventually stabilizes on. A domain (complete partial order, cpo) has lubs for all chains.

3. Scott continuity. A functional F is Scott-continuous if it preserves lubs of chains: F(⊔ᵢ fᵢ) = ⊔ᵢ F(fᵢ). Intuitively, if you know the loop's behavior for all finite numbers of iterations, you know its full behavior.

4. Kleene fixed-point theorem. If D is a cpo with bottom ⊥ and F : D → D is Scott-continuous, then F has a least fixed point:

lfp(F) = ⊔ᵢ Fⁱ(⊥)

where F⁰(⊥) = ⊥, F¹(⊥) = F(⊥), F²(⊥) = F(F(⊥)), etc.

For the while loop, Fⁿ(⊥) is the function that correctly computes the loop for at most n iterations, returning ⊥ (diverging) if more are needed. The least fixed point is the limit — it correctly handles any number of iterations, diverging exactly when the loop diverges.

Why 'least'? There could be many fixed points of F. The least one is the one that is undefined on exactly those inputs where the loop truly diverges — no more, no less. This matches our intuition for what a while loop should compute.

An analogy: Think of building a function by induction. F⁰(⊥) is a blank check — it diverges everywhere. F¹(⊥) handles inputs where the loop terminates in 0 iterations (guard is immediately false). F²(⊥) handles 0 or 1 iterations. The lfp is the union of all these finite approximations.

# Kleene iteration: compute lfp(F) for a while loop by finite approximation
# Each iteration adds one more 'layer' of the loop

def kleene_while(b_fn, body_fn, steps=50):
    """Return a function approximating while b do body
       b_fn : sigma -> bool
       body_fn : sigma -> sigma | None
    """
    # F maps a partial function f to one-more-unrolling of the loop
    def F(f):
        def step(sigma):
            if not b_fn(sigma):
                return sigma       # guard false: done
            s2 = body_fn(sigma)
            if s2 is None:
                return None        # body diverges: diverge
            return f(s2)           # recurse into inner f
        return step

    f = lambda sigma: None  # bot: diverges everywhere
    for _ in range(steps):
        f_new = F(f)
        f = f_new
    return f

# Example: compute x = 0 by counting down from n
# while x > 0 do x := x - 1
b = lambda s: s['x'] > 0
body = lambda s: {**s, 'x': s['x'] - 1}
loop = kleene_while(b, body, steps=200)
print(loop({'x': 5}))   # => {'x': 0}  (terminates in 5 steps)
print(loop({'x': 300})) # => None       (steps exceeded: approximation diverges)

A crucial notational and conceptual skill is reading and writing inference rules and building derivation trees (also called proof trees or derivations).

An inference rule has the form:

  J₁   J₂   ...   Jₙ
 ─────────────────────  (Name)
         J

J₁...Jₙ are the premises, J is the conclusion. If n=0 the rule is an axiom (no premises needed — it is unconditionally true).

A derivation of judgment J is a tree where:

• The root node is labeled J
• Each internal node is a rule application whose conclusion matches the node's label and whose children are derivations of the premises
• All leaves are axiom instances

Example: Derive ⟨x := 3 + 2, σ⟩ ⇓ σ[x ↦ 5]:

                ──────────  (Num)   ──────────  (Num)
                ⟨3,σ⟩⇓₃            ⟨2,σ⟩⇓₂
               ─────────────────────────────  (Add)
                     ⟨3+2, σ⟩⇓₅
               ──────────────────────────────────  (Assign)
               ⟨x := 3+2, σ⟩ ⇓ σ[x ↦ 5]

Induction on derivations is the fundamental proof technique. To prove a property P holds for all valid judgments, you show:

1. P holds for all axiom instances (base case)
2. For each non-axiom rule, if P holds for all premises' derivations, then P holds for the conclusion's derivation (inductive step)

This is just structural induction on the derivation tree. It is used to prove type soundness, equivalence of semantics, compiler correctness, and virtually every other meta-theorem in PL theory.

# Representing and checking derivation trees
from dataclasses import dataclass, field
from typing import List, Any

@dataclass
class Derivation:
    rule: str           # name of the inference rule applied
    conclusion: str     # the judgment concluded
    premises: List['Derivation'] = field(default_factory=list)
    # A leaf (axiom application) has premises=[]

# Example: manual derivation of ⟨x := 3 + 2, {}⟩ ⇓ {x: 5}
deriv = Derivation(
    rule='Assign',
    conclusion='⟨x := 3+2, {}⟩ ⇓ {x:5}',
    premises=[
        Derivation(
            rule='Add',
            conclusion='⟨3+2, {}⟩ ⇓ 5',
            premises=[
                Derivation('Num', '⟨3, {}⟩ ⇓ 3'),
                Derivation('Num', '⟨2, {}⟩ ⇓ 2'),
            ]
        )
    ]
)

def print_deriv(d, indent=0):
    print(' ' * indent + f'[{d.rule}] {d.conclusion}')
    for p in d.premises:
        print_deriv(p, indent + 2)

print_deriv(deriv)

We have three semantic styles. A natural question is: do they agree? This is not obvious — they were defined independently using different mathematical machinery.

Theorem (Operational Equivalence): For any command c and states σ, σ':

⟨c, σ⟩ ⇓ σ'   ⟺   ⟨c, σ⟩ →* σ'

(Big-step derivation exists iff small-step reduction sequence to σ' exists.)

Theorem (Computational Adequacy): For any command c and states σ, σ':

⟦c⟧(σ) = σ'   ⟺   ⟨c, σ⟩ ⇓ σ'

(Denotational value equals the operationally computed output.)

Proof sketch for adequacy (⇐ direction): By induction on the big-step derivation. Each case shows that the denotational equation mirrors the big-step rule. The hard case is While-True, which requires using properties of the least fixed point. Specifically, you need:

• ⟦while b do c⟧ = lfp(F) by definition
• F(lfp(F)) = lfp(F) (fixed point property)
• Induction hypothesis gives ⟦c⟧(σ) = σ' and ⟦while b do c⟧(σ') = σ''
• Then F(lfp(F))(σ) = lfp(F)(⟦c⟧(σ)) = lfp(F)(σ') = σ'' ✓

Why does this matter? Adequacy means the three styles are interchangeable for expressing properties of terminating programs. You can:

• Define the language operationally (easier to implement interpreters and type systems)
• Prove properties denotationally (function-level equational reasoning)
• Switch between styles in the same proof

Observational equivalence. Two programs c₁ and c₂ are observationally equivalent (written c₁ ≅ c₂) if for all states σ, ⟦c₁⟧(σ) = ⟦c₂⟧(σ). This is the correct notion of 'same program' — it says no context can distinguish them. Compiler optimizations must preserve observational equivalence.

Formal semantics is not just abstract mathematics — it is the foundation of practical tools.

Type soundness (progress + preservation). A type system Γ ⊢ c : T is sound if well-typed programs do not get stuck. The proof technique (due to Wright and Felleisen, 1994) uses the small-step semantics:

• Progress: If ⊢ e : T then either e is a value or ∃e'. e → e'.
• Preservation: If ⊢ e : T and e → e' then ⊢ e' : T. Together, these imply a well-typed program never reduces to a stuck configuration (e.g., 1 + true).

Compiler correctness. A compiler C is correct if for all source programs s and inputs i, ⟦C(s)⟧_target(i) = ⟦s⟧_source(i). This is a precise statement about two denotational semantics (source and target language). CompCert proved exactly this for a significant subset of C to PowerPC/ARM assembly, using Coq and operational semantics.

Program equivalence via denotational reasoning:

x := 0; x := 1  ≅  x := 1

Proof: ⟦x:=0; x:=1⟧(σ) = σ[x↦0][x↦1] = σ[x↦1] = ⟦x:=1⟧(σ). QED.

This kind of equational reasoning justifies compiler optimizations like dead-store elimination and constant folding.

Hoare logic connection. Hoare triples {P} c {Q} can be derived from operational semantics by defining:

{P} c {Q}  ≜  ∀σ. P(σ) → ∀σ'. ⟨c,σ⟩ ⇓ σ' → Q(σ')

This makes axiomatic semantics a derived notion built on operational semantics, rather than a separate foundation.

# Program equivalence by denotational reasoning
# Proving: (x := 0); (x := 1)  is equivalent to  (x := 1)

def prog1(sigma):
    # x := 0; x := 1
    s1 = {**sigma, 'x': 0}   # after x := 0
    s2 = {**s1,   'x': 1}   # after x := 1
    return s2

def prog2(sigma):
    # x := 1
    return {**sigma, 'x': 1}

# Verify equivalence on several states
test_states = [{'x': 0}, {'x': 5}, {'x': -3, 'y': 10}]
for s in test_states:
    assert prog1(s) == prog2(s), f"Mismatch on {s}"  # holds for all states

# This is the computational check; the *proof* uses the denotational equations:
# [[x:=0; x:=1]](σ) = [[x:=1]]([[x:=0]](σ)) = [[x:=1]](σ[x↦0]) = σ[x↦0][x↦1] = σ[x↦1]
# [[x:=1]](σ)       = σ[x↦1]
# So they are equal for every σ. QED.

IMP is intentionally minimal. Real languages have functions, recursion, closures, and mutable references. Extending the semantics is instructive.

Procedures and environments. Add to IMP:

c ::= ... | call f(a)      -- procedure call
d ::= proc f(x) = c ; d   -- declaration

Now a state must also carry an environment ρ : ProcName → (Var × Cmd) mapping procedure names to their parameter/body pairs. The big-step rule for call:

ρ(f) = (x, body)    ⟨a, σ⟩ ⇓ₐ n    ⟨body, σ[x↦n]⟩ ⇓ σ'
────────────────────────────────────────────────────────  (Call)
              ⟨call f(a), ρ, σ⟩ ⇓ σ'

(We use pass-by-value here; pass-by-reference would update σ differently.)

Closures (higher-order functions). When functions are first-class values, you need closures — a pair of a function body and the environment at the time of definition. The denotation of a lambda becomes a higher-order function on domains, requiring that the domain be reflexive (can contain its own function space). Scott's breakthrough in 1969 was constructing such domains, which he called D∞ domains.

Recursive types and domains. A denotational semantics for a language with recursive types (like type t = Int | (t -> t)) requires solving domain equations like D ≅ Int + [D → D]. Scott's domain theory provides the machinery to solve these (using limits of inverse systems of approximating domains).

In practice: Most modern formalized language semantics use small-step SOS (because of its flexibility with concurrency and non-termination), often mechanized in proof assistants like Coq, Lean, or Isabelle/HOL. Denotational semantics remains essential for reasoning about program equivalence and for the foundations of type theory.

-- Haskell: denotational semantics for a tiny lambda calculus
-- Values are integers or closures
data Val = VInt Int | VClos String Expr Env
type Env = [(String, Val)]

data Expr
  = Lit Int
  | Lam String Expr       -- λx. e
  | App Expr Expr          -- e1 e2
  | Var String
  | Fix Expr               -- fix-point combinator for recursion

eval :: Env -> Expr -> Val
eval env (Lit n)     = VInt n
eval env (Var x)     = case lookup x env of Just v -> v
eval env (Lam x e)   = VClos x e env   -- capture environment!
eval env (App e1 e2) =
  let VClos x body cenv = eval env e1
      v2 = eval env e2
  in  eval ((x, v2) : cenv) body        -- extend closure's env
eval env (Fix e) =
  -- fix f = f (fix f)  -- unfold once
  let f = eval env e
  in  case f of
        VClos x body cenv ->
          eval ((x, eval env (Fix e)) : cenv) body