11. Denotational Semantics and Domain Theory

Working System

This chapter models lambda terms denotationally using partial values and fixed points. We use Python None as ⊥ (bottom) and compute least fixed-point approximants by iteration.

11. Denotational Semantics and Domain Theory#

Goal. Understand how lambda terms denote computations in a semantic domain, and why recursion corresponds to a least fixed point.

You will learn

  • What bottom (\(\bot\)) means and how partiality appears in semantic models

  • What a flat domain is and how it approximates undefined values

  • How least fixed points arise from Kleene chains of a continuous functional

  • How to compute fixed-point approximants by iteration in Python

  • How a fuelled interpreter models divergence as \(\bot\)

Roadmap#

  1. Build a flat domain \(D = \{\bot\} \cup \mathbb{N}\) and its order.

  2. Define a functional \(F\) over partial functions and compute its Kleene chain.

  3. Interpret recursion as the least fixed point \(\mathrm{lfp}(F)\).

  4. Implement a denotationally motivated interpreter with fuel (divergence yields \(\bot\)).

  5. Connect this semantic view to operational reduction and to NbE (next chapter).

Flat Domain Prototype#

We model a flat domain D = {⊥} ∪ ℕ where ⊥ means “undefined so far”. Order: ⊥ ≤ n for all n; distinct naturals are incomparable.

BOTTOM = None

def leq(x, y):
    # Flat order: bottom is below everything; concrete values only <= themselves.
    if x is BOTTOM:
        return True
    return x == y


def chain_lub(chain):
    # LUB of an increasing chain in a flat domain: last defined value if any.
    for v in reversed(chain):
        if v is not BOTTOM:
            return v
    return BOTTOM

print(leq(BOTTOM, 3), leq(3, 3), leq(2, 3))
print(chain_lub([BOTTOM, BOTTOM, 4, 4]))

True True False
4

Recursion as Least Fixed Point#

Given a continuous functional F, the denotation of fix F is the least fixed point:

\[ \mathrm{lfp}(F) = \sup_{n \ge 0} F^n(\bot). \]

Here \(F^n(\bot)\) is the \(n\)-fold iterate starting from the everywhere-bottom approximation. We approximate this chain computationally.

def kleene_chain(F, steps=8):
    f = lambda n: BOTTOM
    out = [f]
    for _ in range(steps):
        f = F(f)
        out.append(f)
    return out


def FactF(f):
    # Functional for factorial over partial functions N -> N⊥.
    def g(n):
        if n < 0:
            return BOTTOM
        if n == 0:
            return 1
        prev = f(n - 1)
        if prev is BOTTOM:
            return BOTTOM
        return n * prev
    return g

chain = kleene_chain(FactF, steps=7)

for k, fk in enumerate(chain):
    vals = [fk(n) for n in range(7)]
    print(f"F^{k}(⊥):", vals)

F^0(⊥): [None, None, None, None, None, None, None]
F^1(⊥): [1, None, None, None, None, None, None]
F^2(⊥): [1, 1, None, None, None, None, None]
F^3(⊥): [1, 1, 2, None, None, None, None]
F^4(⊥): [1, 1, 2, 6, None, None, None]
F^5(⊥): [1, 1, 2, 6, 24, None, None]
F^6(⊥): [1, 1, 2, 6, 24, 120, None]
F^7(⊥): [1, 1, 2, 6, 24, 120, 720]

At stage k, values up to roughly k-1 are known. The least upper bound of all stages gives total factorial on naturals.

Denotation of Lambda Terms (Fuelled Prototype)#

The next interpreter is denotationally motivated: divergence yields ⊥, while terminating terms yield values.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "lc_core.py").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from lc_core import Var, Lam, App, show

class Closure:
    def __init__(self, param, body, env):
        self.param = param
        self.body = body
        self.env = env

    def __repr__(self):
        return f"<closure λ{self.param}. ...>"


def eval_den(term, env, fuel=80):
    if fuel <= 0:
        return BOTTOM
    if isinstance(term, Var):
        return env.get(term.name, BOTTOM)
    if isinstance(term, Lam):
        return Closure(term.param, term.body, dict(env))
    if isinstance(term, App):
        fn_val = eval_den(term.fn, env, fuel - 1)
        arg_val = eval_den(term.arg, env, fuel - 1)
        if not isinstance(fn_val, Closure):
            return BOTTOM
        new_env = dict(fn_val.env)
        new_env[fn_val.param] = arg_val
        return eval_den(fn_val.body, new_env, fuel - 1)
    raise TypeError("unknown term")

id_term = Lam("x", Var("x"))
omega = App(Lam("x", App(Var("x"), Var("x"))), Lam("x", App(Var("x"), Var("x"))))

print("id denotation:", eval_den(id_term, {}))
print("omega denotation with finite fuel:", eval_den(omega, {}, fuel=60))

id denotation: <closure λx. ...>
omega denotation with finite fuel: None

Remark

In full domain theory, the semantic universe is a pointed CPO and interpretation is proven compositional and continuous. This notebook gives a runnable approximation that still exhibits the core idea: recursion = least fixed point.

Exercise

  1. Increase the number of Kleene steps in the factorial chain and observe how many inputs become defined at stage \(k\).

  2. Define a new functional (for example, triangular numbers) and compute its Kleene chain.

  3. Evaluate a terminating term and a diverging term with eval_den for different fuel values. Explain the results.

  4. Construct the term (\x. x) (\y. y) using Var/Lam/App and confirm its denotation is a closure (not bottom). See solutions: Exercise 11 (Denotational Semantics)

Summary#

  • Denotational semantics assigns meanings to terms in a domain that can represent partiality via \(\bot\).

  • Continuous functionals have least fixed points computed as limits of Kleene chains.

  • Iterating a functional in Python gives a runnable approximation of \(\mathrm{lfp}(F)\).

  • A fuelled interpreter is a practical way to model divergence as \(\bot\).

  • Next: Chapter 12 shows NbE, a semantics-driven way to compute normal forms in STLC.

Contents