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 of a directed set
→	U+2192	Function space	Scott-continuous functions
×	U+00D7	Product	Pairwise ordered product of domains
≅	U+2245	Isomorphism	As in D ≅ [D → D]
∈	U+2208	Membership	Ranging over elements of a directed set
∞	U+221E	Infinity	Inverse limit stage in D∞
ₑ	U+2091	Latin subscript small letter e	Embedding in an embedding-projection pair
ⁿ	U+207F	Superscript n	Iterate fⁿ in the fixed point formula
ₙ	U+2099	Subscript n	Index of a stage or of the join ⊔ₙ
fix	—	Fixed point	Least fixed point, ⊔ₙ fⁿ(⊥)
D	—	Domain	Pointed dcpo
D⊥	—	Lift	Domain with a new bottom adjoined
[D → D]	—	Function domain	Scott-continuous self-maps, ordered pointwise
K(D)	—	Compacts	Finite, or compact, elements of D
+	—	Separated sum	Coproduct of domains

Metatheory. Dcpos with Scott-continuous maps form a cartesian closed category, and Scott-continuity coincides with topological continuity for the Scott topology, so the order theory and the topology are one subject. The Kleene fixed point theorem gives every continuous endomap of a pointed dcpo a least fixed point ⊔ₙ fⁿ(⊥), which is what makes recursion denotable. Scott's D∞ construction (1969) solves D ≅ [D → D] as an inverse limit along embedding-projection pairs, and Smyth and Plotkin, "The Category-Theoretic Solution of Recursive Domain Equations" (1982), generalized this: in an O-category with embedding-projection pairs the solution is a minimal invariant, simultaneously an initial algebra and a final coalgebra, and it is unique up to isomorphism. Cartesian closure is fragile under restriction. Smyth (1983) proved that the largest cartesian closed full subcategory of ω-algebraic cpos is the SFP, or bifinite, domains, and Jung (1988, 1990) classified the maximal cartesian closed full subcategories of algebraic and of continuous domains, finding exactly two families in each case: bifinite domains and L-domains in the algebraic case, FS-domains and continuous L-domains in the continuous case. Scott (1972) proved continuous lattices are precisely the injective T₀ spaces, and Abramsky's "Domain Theory in Logical Form" (1991) established a Stone duality between bifinite domains and a propositional logic of observable properties, sound and complete for it.

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. There is no canonical category of domains. Dcpos are cartesian closed, but the well-behaved subcategories are not: Jung's classification shows two incomparable maximal cartesian closed families of algebraic domains, so closure under function space forces a choice with no principled winner. Continuity commits the semantics to monotone functions, which is precisely why no domain-theoretic model can contain a halting test — a function distinguishing ⊥ from its approximants is not monotone — and why the Scott model of PCF is adequate but not fully abstract, containing parallel-or as an undefinable element. Nondeterminism forces a powerdomain, and the Plotkin, Smyth and Hoare constructions identify different programs with no neutral option. Probability is worse: whether any cartesian closed category of continuous domains is closed under the probabilistic powerdomain has been open since Jung and Tix raised it in 1998. Recursive domain equations are solvable only via embedding-projection pairs, so the solution depends on that structure and is characterized only up to the minimal invariant. Concurrency with fairness is not captured, since fair merge is not Scott-continuous.