Domain Theory

Origin. Dana Scott introduced domains (1969-70) to give semantics to the lambda calculus. Solves: D ≅ D → D (types isomorphic to their function space). Continuous lattices and dcpos provide mathematical foundation. Scott and Strachey developed denotational semantics. Foundational for programming language semantics.

Models. Partial information and approximation. Programs may not terminate or may compute partially. Domains: ordered sets where elements are approximations. ⊥ is no information; x ⊑ y means y has more information. Continuous functions preserve approximation structure. Fixed points give meaning to recursion.

Formalism.

Directed-complete partial order (dcpo): (D, ⊑) where every directed set has a supremum. Directed: non-empty, every pair has upper bound.

Scott topology: Open sets: upward closed + inaccessible by directed limits. Continuous functions: Scott-continuous (preserve directed sups).

Pointed dcpo (domain): Has bottom ⊥ (least element). Every Scott-continuous f: D → D has least fixed point: fix(f) = ⊔ₙ fⁿ(⊥).

Important domain constructions:

D₁ × D₂: product (pairwise order)
D₁ → D₂: continuous functions (pointwise order)
D₁ + D₂: separated sum
D⊥: lift (add new bottom)
[D → D]: reflexive domain (D ≅ [D → D])

Scott's D∞ construction: Build D∞ as limit of D₀ →ₑ D₁ →ₑ D₂ →ₑ ... where Dₙ₊₁ = [Dₙ → Dₙ]. Achieves D∞ ≅ [D∞ → D∞].

Algebraic domains: Element x is compact if x ⊑ ⊔D implies x ⊑ d for some d ∈ D. Algebraic: every element is sup of compacts below it.

Symbols.

Symbol	Unicode	Name	Meaning
⊑	U+2291	Approximation	Information order
⊥	U+22A5	Bottom	No information
⊔	U+2294	Supremum	Least upper bound
→	U+2192	Function space	Continuous functions
fix	—	Fixed point	Least fixed point
D	—	Domain	Dcpo
K(D)	—	Compacts	Compact elements

Metatheory. Dcpos form Cartesian closed category. Fixed-point theorem: continuous f has least fixed point. Solutions to recursive domain equations exist. Scott model: untyped λ-calculus has model in D∞. Algebraic domains = ideal completion of bases. Continuous lattices = injective T₀ spaces.

Applies to. Denotational semantics (λ-calculus, PCF). Programming language semantics. Higher-order recursion. Probabilistic programming semantics. Concurrency semantics. Game semantics foundations. Type theory (recursive types).

Limitations. Abstract: far from operational intuition. Full abstraction problem (PCF). Classical domains inadequate for some concurrency. Synthetic domain theory offers alternatives. Computation may require effectful extensions. Probabilistic and quantum require further development.