Learning path

Full curriculum

Full curriculum

Arrows go from each prerequisite to the units that depend on it. Hover or focus a unit to highlight its path.

Unit content

Denotational semantics

A denotational semantics assigns each program phrase a mathematical meaning. Instead of describing execution step by step, it maps syntax into semantic objects and composes the meanings of larger phrases from their parts.

Write $\llbracket e\rrbracket$ for the denotation of expression $e$. For pure arithmetic,

$$\llbracket e_1+e_2\rrbracket_\rho =\llbracket e_1\rrbracket_\rho+\llbracket e_2\rrbracket_\rho,$$

where the environment $\rho$ supplies meanings for free variables.

For a conditional,

$$\llbracket \text{if }b\text{ then }e_1\text{ else }e_2\rrbracket_\rho$$

selects the denotation of $e_1$ or $e_2$ according to the denotation of $b$.

The defining principle is compositionality: the meaning of a compound phrase is determined by the meanings of its immediate parts. This makes semantic equations suitable for equational reasoning and language design.

Recursion introduces a deeper issue because a recursive definition refers to its own meaning. A denotational model can interpret the recursive program as a suitable fixed point of the semantic function describing one unfolding of its body.

Denotational semantics complements operational semantics. Operational rules say how programs compute; denotations say what mathematical objects those computations mean. Proving the two descriptions agree connects implementation-oriented execution with abstract reasoning.