Denotational Semantics

Origin. Scott and Strachey (1970s). Mathematical meaning of programs. Domains as semantic spaces. Compositionality: meaning from parts. Foundation for language semantics.

Models. Programs denote mathematical objects. ⟦·⟧: syntax → semantics. Compositionality: ⟦e₁ op e₂⟧ = f(⟦e₁⟧, ⟦e₂⟧). Fixed points for recursion.

Formalism.

Semantic function: ⟦·⟧: Syntax → Domain Maps syntactic constructs to meanings.

Domains: Partially ordered sets with limits. D = D⊥ (lift with ⊥ for non-termination). Function spaces: D → E continuous functions.

Basic constructs: ⟦n⟧ρ = n (numeral) ⟦x⟧ρ = ρ(x) (variable lookup) ⟦e₁ + e₂⟧ρ = ⟦e₁⟧ρ + ⟦e₂⟧ρ

Lambda abstraction: ⟦λx.e⟧ρ = λd.⟦e⟧ρ[x↦d]

Application: ⟦e₁ e₂⟧ρ = ⟦e₁⟧ρ(⟦e₂⟧ρ)

Recursion: ⟦fix f⟧ρ = fix(⟦f⟧ρ) = ⊔ₙ fⁿ(⊥) Least fixed point.

Continuity: Semantic functions are continuous. Preserves directed limits. Enables fixed-point existence.

Adequacy: e ⇓ v implies ⟦e⟧ = ⟦v⟧. Computational matches denotational.

Symbols.

Symbol	Unicode	Name	Meaning
⟦ ⟧	—	Brackets	Semantic function
ρ	U+03C1	Rho	Environment
⊥	U+22A5	Bottom	Divergence
⊔	U+2294	Join	Least upper bound
fix	—	Fix	Fixed point

Metatheory. Full abstraction: denotational = observational. Domain theory (Scott). Adequacy theorems. Compositionality.

Applies to. Language specification. Compiler correctness. Program analysis. Concurrency models.

Limitations. Full abstraction hard. Higher-order state complex. Game semantics alternative. Operational often simpler.