Денотационная семантика

Что значит 'программа правильная'? Операциональная семантика говорит как программа выполняется. Денотационная - что она значит математически. Разница как между алгоритмом Тьюринга и математической функцией, которую он вычисляет.

• **Haskell** - язык, семантика которого прямо основана на domain theory. Ленивые вычисления (thunks) соответствуют частичным функциям между доменами. Монады - это функторы между категориями доменов
• **Certified compilers**: CompCert (формально верифицированный C компилятор) использует денотационную семантику для доказательства корректности оптимизаций. Deployed в авиационных и военных системах
• **Статический анализ**: Abstract Interpretation (Cousot & Cousot, 1977) - применение domain theory для статического анализа программ. Основа Astrée (анализатор Airbus A340/A380 fly-by-wire software)

Домены: математические объекты как значения программ

1969 год. Дана Скотт пытается дать математическое значение лямбда-исчислению. Проблема: функция может принимать сама себя как аргумент. Классическое множество теорий разрушается из-за парадоксов размерности. Скотт изобретает domain theory - и это становится фундаментом всей денотационной семантики.

Денотационная семантика задаёт каждому синтаксическому элементу программы **денотацию** - математический объект. Целое число n денотирует число n. Функция денотирует математическую функцию. Нетерминирующая программа денотирует специальный элемент - **bottom** (⊥). Домен - это множество с частичным порядком, включающее ⊥.

ML-параллель: тип `Maybe/Option` в Haskell/Rust - дискретный домен. `None/Nothing` играет роль ⊥. Функция `map` на `Option` - монотонная функция между доменами. Это не случайность: domain theory прямо повлияла на дизайн типовых систем функциональных языков.

Неподвижные точки: рекурсия как математика

Рекурсивная функция `factorial(n) = if n=0 then 1 else n * factorial(n-1)` определяет factorial через factorial. Это круговое определение. Как дать ему математический смысл? Через неподвижную точку. Factorial - это наименьшая неподвижная точка функционала $F$, где $F(f) = \lambda n. $ if $n=0$ then $1$ else $n * f(n-1)$.

Теорема Клини о наименьшей неподвижной точке: каждый монотонный непрерывный функционал $F: D \to D$ имеет наименьшую неподвижную точку $\text{fix}(F) = \bigsqcup_{n \geq 0} F^n(\bot)$. Это итерация: $\bot, F(\bot), F(F(\bot)), ..$ сходится к fix(F). Именно так устроен семантический смысл любой рекурсии.

Непрерывность функций: гарантия неподвижных точек

Теорема Клини работает только для **непрерывных** функций. Непрерывность в domain theory: функция $f$ непрерывна если $f(\bigsqcup D) = \bigsqcup f(D)$ для любой направленной цепи D. Другими словами: значение на пределе равно пределу значений. Это более строгое требование, чем монотонность.

Почему это важно? Непрерывность гарантирует что аппроксимации F^n(⊥) действительно сходятся к неподвижной точке, а не 'перепрыгивают' через неё. Все разумные программные конструкции - последовательность, условие, лямбда - задают непрерывные денотационные функции. Это не случайность: Dennis Scott тщательно проверил это при разработке domain theory.

Аналог в анализе: теорема Банаха о сжимающем отображении - функция-сжатие имеет единственную неподвижную точку, достигаемую итерацией. Domain theory - это аналог для частично упорядоченных структур вместо метрических пространств. Применения в ML: convergence гарантии для iterative algorithms (EM algorithm, belief propagation) основаны на похожих идеях.

Композициональность: смысл программы из смысла частей

Главное свойство денотационной семантики: **композициональность**. Смысл выражения `e1 + e2` определяется только смыслом `e1` и смыслом `e2`, не их синтаксической структурой. Формально: денотационная функция [[ ]] гомоморфна: [[e1 + e2]] = [[e1]] + [[e2]].

Это позволяет: (1) доказывать equivalence программ - если [[P1]] = [[P2]], программы семантически идентичны. (2) оптимизировать компилятор - замена подвыражения на денотационно эквивалентное корректна. (3) задавать типы через домены - тип это домен, функция правильного типа это непрерывная функция между доменами.

Связанные темы

Денотационная семантика соединяет математику и языки программирования:

• Операциональная семантика — Альтернативный подход: как программа выполняется (steps) vs. что она значит (math objects)
• Лямбда-исчисление — Денотационная семантика лямбда-выражений - канонический пример применения
• Аксиоматическая семантика — Hoare logic строится поверх денотационной семантики для верификации программ

Ключевые идеи

• **Домены**: частично упорядоченные множества с ⊥ как 'нет значения'. Программный тип = домен. Bottom ⊥ - нетерминация и undefined.
• **Неподвижные точки**: рекурсия = fix(F) = sup{F^n(⊥)}. Каждое рекурсивное определение имеет математический смысл как наименьшая неподвижная точка функционала.
• **Непрерывность**: условие для теоремы Клини. f(sup D) = sup f(D). Все стандартные программные конструкции непрерывны.
• **Композициональность**: [[e1 op e2]] определяется только через [[e1]] и [[e2]]. Фундамент для доказательства корректности оптимизаций и equivalence.

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

• Ленивые вычисления в Haskell соответствуют partial functions в domain theory. Как это связано с ⊥ и неподвижными точками?
• Dennotational semantics сложна для языков с mutable state и I/O. Монады решают это в Haskell. Как?
• CompCert доказывает корректность C компилятора через денотационную семантику. Что именно доказывается и насколько это применимо к современным оптимизирующим компиляторам?

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

• plt-14-operational-semantics — Операциональная семантика - альтернативный подход для сравнения
• plt-16-axiomatic-semantics — Денотационная семантика - фундамент для аксиоматического подхода
• plt-06-lambda-calculus — Лямбда-исчисление - язык денотационной семантики
• alg-21-dp — Неподвижные точки в денотационной семантике аналогичны DP: итеративное построение решения
• comp-20-semantic-passes