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

Понятие денотационная семантика приводят Кристофер Стрейчи и Дана Скотт в своих работах, опубликованных в начале 1970-х годов и отсюда этот метод получает название «математическая семантика» или «семантика Скотта-Стрейчи»^[2][3]. Она представляла значение компьютерной программы как функции, которая отображала входные данные в выходные. Чтобы придать значения рекурсивно определённым программам, Скотт предложил работать с непрерывными функциями между доменами, в частности, с полными частичными порядками^[4]. Работа была продолжена в исследовании соответствующей денотационной семантики для таких аспектов языков программирования, как последовательность, параллелизм, недетерминизм и локальное состояние .

Название метода «денотационная семантика» происходит от английского слова denote (обозначать), поскольку математический объект обозначает смысл соответствующей синтаксической сущности. Денотационная семантика — это метод придания точного значения языку программирования. Хотя синтаксис языка всегда формально указан в варианте BNF, более важная часть определения его семантики в основном оставлена ​​естественному языку, который неоднозначен и оставляет много вопросов открытыми. Особенно для построения компилятора для этого языка необходимо более глубокое понимание, чем может быть обеспечено неформальными описаниями.

Денотационная семантика занимается поиском более подходящих моделей — доменов, в том числе, для моделирования таких понятий языков программирования как функциональный тип. Считается, что целесообразно не ограничиваться лишь вычислимыми функциями, а использовать любые непрерывные по Скотту функции на частично упорядоченных множествах, которыми возможно смоделировать также и незавершимые вычисления (а таковые возникают во всяком полном по Тьюрингу языке). Средства теории областей, используемые в денотационной семантике, достаточно выразительны, например, непрерывной по Скотту функцией моделируется «parallel or», определимый далеко не во всех языках программирования.

Важным аспектом денотационной семантики языков программирования является композиционность, посредством которой денотация программы строится из денотаций её частей. Базовая денотационная семантика в теории доменов является композиционной, поскольку она задается следующим образом. Начинают с рассмотрения фрагментов программ, то есть программ со свободными переменными. Контекст типизации назначает тип каждой свободной переменной. Например, в выражении (x + y) можно рассматривать в контексте типизации (x:nat,y:nat). Задаётся денотация фрагментам программ, используя следующую схему:

1. Начинают с описания значений типов языка: значение каждого типа должно быть доменом. Пишут〚τ〛 для домена, обозначающего тип τ. Например, значение типа nat должно быть доменом натуральных чисел: 〚nat〛= ${\displaystyle \mathbb {N} }$_⊥.
2. Из значения типов выводят значение для типизирования контекстов. Устанавливают 〚 x₁:τ₁,…, x_n:τ_n〛 = 〚 τ₁〛× … ×〚τ_n〛. Например, 〚x:nat,y:nat〛= ${\displaystyle \mathbb {N} }$_⊥×${\displaystyle \mathbb {N} }$_⊥. В качестве особого случая значение пустого контекста типизации без переменных представляет собой домен с одним элементом, обозначаемым 1.
3. В конце, присваивают значение каждому фрагменту программы в контексте набора текста. Полагая, что P — фрагмент программы типа σ, в контексте набора текста Γ, записывают Γ⊢P:σ. Тогда значение этой программы в контексте набора текста должно быть непрерывной функцией 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛. Например, 〚⊢7:nat〛:1→${\displaystyle \mathbb {N} }$_⊥ — постоянная функция «7», в то время как〚x:nat,y:nat⊢x+y:nat〛:${\displaystyle \mathbb {N} }$_⊥×${\displaystyle \mathbb {N} }$_⊥→${\displaystyle \mathbb {N} }$_⊥ — функция, которая складывает два числа. Тогда значение суммы (7+4) определяется путем составления трех функций 〚⊢7: nat〛:1→_⊥ , 〚⊢4: nat〛:1→_⊥ , и 〚x : nat, y : nat⊢ x + y : nat〛:_⊥ ×_⊥ →_⊥ .

Это общая схема для композиционной денотационной семантики. В ней нет конкретики относительно доменов и непрерывных функций. Вместо этого можно работать с другой категорией. В игровой семантике категория игр имеет игры как объекты и стратегии как морфизмы: можно интерпретировать типы как игры, а программы как стратегии. Для простого языка без общей рекурсии можно обойтись категорией множеств и функций.

Концепция доменов мощности была разработана для того, чтобы определить денотационную семантику недетерминированных последовательных программ. Записывая P для конструктора домена мощности, домен P (D) является доменом недетерминированных вычислений типа, обозначенного D . В информатике неограниченный недетерминизм или неограниченная неопределенность — это свойство параллелизма, при котором задержка в обслуживании запроса может стать неограниченной в результате конкуренции за общие ресурсы. При этом сохраняется гарантия, что запрос будет обслужен. Неограниченный недетерминизм стал важным вопросом в развитии денотационной семантики параллелизма и позднее стал частью исследований теоретической концепции гипервычислений^[5].

Состояние и простые императивные функции можно напрямую смоделировать в денотационной семантике. Команда рассматривается как частичная функция в некоторой области состояний. Выражение «x:=3» является функцией, которая назначает переменной x состояние 3. Оператор последовательности « ;» понимается как композиция функций. Конструкции с фиксированной точкой используются для придания семантики циклическим конструкциям, таким как « while». При моделировании программ с локальными переменными методы усложняются. Один из подходов заключается в том, чтобы работать не с доменами, а с интерпретациями функторов.

Многие языки программирования позволяют задавать рекурсивные типы данных . Например, тип списков чисел может быть определён следующим образом:

datatype list = Cons of nat * list | Empty

Здесь рассматриваются только функциональные структуры, которые не изменяются. Обычные императивные языки программирования позволяют изменять элементы такого рекурсивного списка.

Другой пример: семантика бестипового лямбда-исчисления:

datatype D = D of (D → D)

Проблема решения уравнений домена связана с поиском доменов, которые моделируют эти типы данных. Чтобы придать λ-исчислению какой-либо смысл, необходимо получить множество, в которое вкладывалось бы его пространство функций. Один из подходов заключается в том, чтобы рассматривать совокупность всех доменов как сам домен, а затем решать рекурсивное определение там.

Часто бывает полезно перевести один язык программирования на другой. Например, параллельный язык программирования может быть переведён в исчисление процессов; высокоуровневый язык программирования может быть переведён в байт-код. И тогда денотационную семантику можно рассматривать как интерпретацию языков программирования на внутренний язык категории доменов.

В дальнейшем, Д.Скотт развил теорию и модели вычислений, разработал принципы денотационной семантики языков программирования, углубил понятие о вычислимости.

Разработанная Стрейчи и Скоттом денотационная семантика предполагала управление компьютерной программой как функцией, которая переводила входные данные в выходные. Чтобы придать значения рекурсивно определённым программам, Скотт предложил работать с непрерывными функциями между доменами.

В начале 1980-х годов начинают использовать методы денотационной семантики для задания семантики параллельных языков. Примерами являются работа Уилла Клингера с моделью актора; работа Глинна Винскеля со структурами событий и сетями Петри; работа Франсеза, Хоара, Лемана и де Роевера (1979) по семантике трассировки для CSP. Все эти направления исследований остаются в стадии изучения.

После разработки языков программирования, основанных на линейной логике, языкам была дана денотационная семантика для линейного использования (например, сети доказательств, пространства когерентности), а также полиномиальная временная сложность.

Проблема полной абстракции для типизированного функционального языка программирования PCF долгое время не была решена. Трудность с PCF заключается в том, что это очень последовательный язык. Например, в PCF нет способа определить функцию parallel-or . По этой причине подход с использованием доменов даёт денотационную семантику, которая не является полностью абстрактной.

• Типы интерпретируются как определённые домены.
  • ${\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }}$ (натуральные числа с нижним индексом, с прямым перечислением)
  • ${\displaystyle [\![\sigma \to \tau \,]\!]}$ интерпретируется как область непрерывных по Скотту функций от ${\displaystyle [\![\sigma ]\!]\,}$ до ${\displaystyle [\![\tau ]\!]\,}$, в точечном порядке.
• Выражение ${\displaystyle x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}}$ интерпретируется как: ${\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]}$
• Термины в выражении ${\displaystyle \Gamma \;\vdash \;x\;:\;\sigma }$ интерпретируются как непрерывные функции ${\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}$
  • Переменные термины интерпретируются как проекции
  • Лямбда-абстракция и применение интерпретируются с использованием декартовой замкнутой структуры категории доменов и непрерывных функций
  • Y интерпретируется путем взятия наименее фиксированной точки аргумента.

Эта модель не является полностью абстрактной для PCF; но она полностью абстрактна для языка, полученного путем добавления параллельного оператора или к PCF. Этот открытый вопрос был в основном решён в 1990-х годах с развитием игровой семантики, а также методов, включающих логические отношения.

Семантика, предложенная Д. Скоттом и развитая Ю. Л. Ершовым с помощью теории нумераций, является универсальной и важнейшей среди семантик языков программирования.

Денотационная семантика была разработана для современных языков программирования, которые используют такие возможности, как параллелизм и исключения, например, Concurrent ML, CSP, и Haskell. Семантика этих языков является композиционной в том смысле, что значение фразы зависит от значений её подфраз.

Близкой по свойствам к топологии Скотта конструкцией является категория пространств, разработанная Юрием Леонидовичем Ершовым в 1975 году. С её помощью также может быть построена непротиворечивая модель λ-исчисления. В качестве её преимущества отмечается, что категория пространств является декартово замкнутой, каждый объект в ней является топологическим пространством, топология на произведении является произведением топологий сомножителей, а топология в пространстве функций оказывается топологией поточечной сходимости. Такими удобными свойствами топология Скотта не обладает, в частности, произведение топологий Скотта на полных частично упорядоченных множеств в общем случае топологией Скотта на произведении множеств не является.

Всякий домен Ершова-Скотта можно представить как множество состояний некоторой информационной системы Скотта, а множество состояний всякой информационной системы Скотта всегда является доменом Ершова-Скотта. Пространства Ершова-Скотта имеют многочисленные приложения в теоретическом программировании и теории вычислимости. В частности, они послужили основой для построения моделей бестипового лямбда-исчисления. При этом построении ключевую роль сыграли пространства непрерывных функций, наделённые топологией поточечной сходимости. Пространства Ершова можно рассматривать как топологический подход к теории областей Ершова-Скотта, см. [13], которая является одним из важных разделов современной математики.

Курс"Денотационная семантика языков программирования" введён в программу высшего образования на базе государственных университетов по направлению подготовки «Математика и компьютерные науки». Так, в Новосибирском государственном университете дисциплина реализуется на Механико-математическом факультете кафедрой дискретной математики и информатики. Основная цель дисциплины — изучение базовых результатов, относящихся к ламбда-исчислению и его семантикам.