Denotational Semantics

What does 'the program is correct' mean? Operational semantics says how a program executes. Denotational semantics says what it means mathematically. The difference is like between a Turing machine algorithm and the mathematical function it computes.

• **Haskell** - a language whose semantics is directly based on domain theory. Lazy evaluation (thunks) corresponds to partial functions between domains. Monads are functors between categories of domains
• **Certified compilers**: CompCert (formally verified C compiler) uses denotational semantics to prove the correctness of optimizations. Deployed in aviation and defense systems
• **Static analysis**: Abstract Interpretation (Cousot & Cousot, 1977) - an application of domain theory to static program analysis. Foundation of Astrée (analyzer for Airbus A340/A380 fly-by-wire software)

Domains: Mathematical Objects as Program Values

1969. Dana Scott is trying to give a mathematical meaning to the lambda calculus. The problem: a function can take itself as an argument. Classical set theory collapses due to size paradoxes. Scott invents domain theory - and it becomes the foundation of all denotational semantics.

Denotational semantics assigns each syntactic element of a program a **denotation** - a mathematical object. The integer n denotes the number n. A function denotes a mathematical function. A non-terminating program denotes a special element - **bottom** (⊥). A domain is a set with a partial order that includes ⊥.

ML parallel: the `Maybe/Option` type in Haskell/Rust is a discrete domain. `None/Nothing` plays the role of ⊥. The function `map` on `Option` is a monotone function between domains. This is not accidental: domain theory directly influenced the design of type systems in functional languages.

Fixed Points: Recursion as Mathematics

The recursive function `factorial(n) = if n=0 then 1 else n * factorial(n-1)` defines factorial in terms of itself. This is a circular definition. How can it be given a mathematical meaning? Through the fixed point. Factorial is the least fixed point of the functional $F$, where $F(f) = \lambda n.$ if $n=0$ then $1$ else $n * f(n-1)$.

Kleene's least fixed point theorem: every monotone continuous functional $F: D \to D$ has a least fixed point $\text{fix}(F) = \bigsqcup_{n \geq 0} F^n(\bot)$. This is iteration: $\bot, F(\bot), F(F(\bot)), ...$ converges to fix(F). This is exactly how the semantic meaning of any recursion is constructed.

Continuity: The Guarantee for Fixed Points

Kleene's theorem works only for **continuous** functions. Continuity in domain theory: a function $f$ is continuous if $f(\bigsqcup D) = \bigsqcup f(D)$ for any directed chain D. In other words: the value at the limit equals the limit of the values. This is a stronger requirement than monotonicity.

Why does this matter? Continuity guarantees that the approximations F^n(⊥) actually converge to the fixed point and do not 'jump over' it. All reasonable programming constructs - sequence, conditional, lambda - define continuous denotational functions. This is not accidental: Dana Scott verified this carefully when developing domain theory.

Calculus analogy: Banach's fixed point theorem - a contraction mapping has a unique fixed point reachable by iteration. Domain theory is the analogue for partially ordered structures instead of metric spaces. ML applications: convergence guarantees for iterative algorithms (EM algorithm, belief propagation) are based on similar ideas.

Compositionality: Meaning from Parts

The defining property of denotational semantics: **compositionality**. The meaning of expression `e1 + e2` is determined solely by the meaning of `e1` and the meaning of `e2`, not their syntactic structure. Formally: the denotation function [[ ]] is homomorphic: [[e1 + e2]] = [[e1]] + [[e2]].

This enables: (1) proving program equivalence - if [[P1]] = [[P2]], the programs are semantically identical. (2) compiler optimization - replacing a subexpression with a denotationally equivalent one is correct. (3) defining types via domains - a type is a domain, a well-typed function is a continuous function between domains.

Related Topics

Denotational semantics bridges mathematics and programming languages:

• Operational Semantics — Alternative approach: how a program executes (steps) vs. what it means (math objects)
• Lambda Calculus — Denotational semantics of lambda expressions is the canonical example
• Axiomatic Semantics — Hoare logic is built on top of denotational semantics for program verification

Key Ideas

• **Domains**: partially ordered sets with ⊥ as 'no value'. Program type = domain. Bottom ⊥ - non-termination and undefined.
• **Fixed points**: recursion = fix(F) = sup{F^n(⊥)}. Every recursive definition has a mathematical meaning as the least fixed point of a functional.
• **Continuity**: condition for Kleene's theorem. f(sup D) = sup f(D). All standard programming constructs are continuous.
• **Compositionality**: [[e1 op e2]] is determined solely by [[e1]] and [[e2]]. Foundation for proving correctness of optimizations and program equivalence.

Вопросы для размышления

• Lazy evaluation in Haskell corresponds to partial functions in domain theory. How does this relate to ⊥ and fixed points?
• Denotational semantics is hard for languages with mutable state and I/O. Monads solve this in Haskell. How?
• CompCert proves C compiler correctness through denotational semantics. What exactly is proved and how applicable is this to modern optimizing compilers?

Связанные уроки

• plt-14-operational-semantics — Operational semantics is an alternative approach for comparison
• plt-16-axiomatic-semantics — Denotational semantics is the foundation for the axiomatic approach
• plt-06-lambda-calculus — Lambda calculus is the language of denotational semantics
• alg-21-dp — Fixed points in denotational semantics resemble DP: iterative construction of a solution
• comp-20-semantic-passes