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

В информатике денотационная семантика (первоначально известная как математическая семантика или семантика Скотта–Стрейчи ) — это подход к формализации значений языков программирования путем построения математических объектов (называемых денотациями ), которые описывают значения выражений из языков. Другие подходы, обеспечивающие формальную семантику языков программирования, включают аксиоматическую семантику и операционную семантику .

В широком смысле денотационная семантика занимается поиском математических объектов, называемых доменами , которые представляют то, что делают программы. Например, программы (или программные фразы) могут быть представлены частичными функциями ^{[1] [2]} или играми ^[3] между средой и системой.

Важным принципом денотационной семантики является то, что семантика должна быть композиционной : денотат программной фразы должен быть построен из денотатов ее подфраз .

Денотационная семантика возникла в работе Кристофера Стрейчи и Даны Скотт , опубликованной в начале 1970-х годов. ^{[1] [2]} Первоначально разработанная Стрейчи и Скоттом, денотационная семантика предоставляла значение компьютерной программы как функции , которая отображала входные данные в выходные данные. ^[2] Чтобы придать значения рекурсивно определенным программам, Скотт предложил работать с непрерывными функциями между доменами , в частности, с полными частичными порядками . Как описано ниже, работа была продолжена в исследовании соответствующей денотационной семантики для таких аспектов языков программирования, как последовательность, параллелизм, недетерминизм и локальное состояние .

Денотационная семантика была разработана для современных языков программирования, которые используют такие возможности, как параллелизм и исключения , например, Concurrent ML , ^[4] CSP , ^[5] и Haskell . ^[6] Семантика этих языков является композиционной в том смысле, что значение фразы зависит от значений ее подфраз. Например, значение аппликативного выражения f(E1,E2) определяется в терминах семантики ее подфраз f, E1 и E2. В современном языке программирования E1 и E2 могут быть оценены одновременно, и выполнение одного из них может повлиять на другой, взаимодействуя через общие объекты, заставляя их значения определяться в терминах друг друга. Кроме того, E1 или E2 могут выдать исключение, которое может завершить выполнение другого. В разделах ниже описываются особые случаи семантики этих современных языков программирования.

Денотационная семантика приписывается программной фразе как функции от среды (содержащей текущие значения ее свободных переменных) к ее денотации. Например, фраза n*mсоздает денотацию, когда предоставляется среда, которая имеет связывание для ее двух свободных переменных: nи m. Если в среде nимеет значение 3 и mимеет значение 5, то денотация равна 15. ^[2]

Функцию можно представить как набор упорядоченных пар аргумента и соответствующих значений результата. Например, набор {(0,1), (4,3)} обозначает функцию с результатом 1 для аргумента 0, результатом 3 для аргумента 4 и неопределенным в противном случае.

Рассмотрим, например, функцию факториала , которую можно рекурсивно определить следующим образом:

int factorial ( int n ) { если ( n == 0 ) то вернуть 1 ; иначе вернуть n * factorial ( n -1 ); }                

Чтобы придать смысл этому рекурсивному определению, обозначение строится как предел приближений, где каждое приближение ограничивает количество вызовов factorial. В начале мы начинаем без вызовов — следовательно, ничего не определено. В следующем приближении мы можем добавить упорядоченную пару (0,1), поскольку это не требует повторного вызова factorial. Аналогично мы можем добавить (1,1), (2,2) и т. д., добавляя по одной паре в каждом последующем приближении, поскольку вычисление factorial(n) требует n+1 вызовов. В пределе мы получаем общую функцию от до , определенную всюду в своей области определения.${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

Формально мы моделируем каждое приближение как частичную функцию . Затем наше приближение многократно применяет функцию, реализующую «создание более определенной частичной факториальной функции», т. е . начиная с пустой функции (пустого множества). F можно определить в коде следующим образом (используя for ):${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$${\displaystyle F:(\mathbb {N} \rightharpoonup \mathbb {N} )\to (\mathbb {N} \rightharpoonup \mathbb {N} )}$Map<int,int>${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$

int factorial_nonrecursive ( Map < int , int > factorial_less_defined , int n ) { если ( n == 0 ) то вернуть 1 ; иначе если ( fprev = lookup ( factorial_less_defined , n -1 )) то вернуть n * fprev ; иначе вернуть NOT_DEFINED ; }                         Карта < int , int > F ( Карта < int , int > factorial_less_defined ) { Карта < int , int > new_factorial = Карта . empty (); for ( int n in all < int > ()) { if ( f = factorial_nonrecursive ( factorial_less_defined , n ) != NOT_DEFINED ) new_factorial . put ( n , f ); } return new_factorial ; }                         

Тогда мы можем ввести обозначение F ⁿ для обозначения F, примененного n раз .

• F ⁰ ({}) — полностью неопределенная частичная функция, представленная в виде множества {};
• F ¹ ({}) — частичная функция, представленная в виде набора {(0,1)}: она определена в 0 как 1 и не определена в других местах;
• F ⁵ ({}) — частичная функция, представленная в виде набора {(0,1), (1,1), (2,2), (3,6), (4,24)}: она определена для аргументов 0,1,2,3,4.

Этот итеративный процесс строит последовательность частичных функций от до . Частичные функции образуют цепочку-полный частичный порядок, используя ⊆ в качестве упорядочения. Более того, этот итеративный процесс лучших приближений факториальной функции образует экспансивное (также называемое прогрессивным) отображение, поскольку каждое использует ⊆ в качестве упорядочения. Таким образом, по теореме о неподвижной точке (в частности , теореме Бурбаки–Витта ) существует неподвижная точка для этого итерационного процесса.${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$${\displaystyle F^{i}\leq F^{i+1}}$

В этом случае неподвижная точка является наименьшей верхней границей этой цепи, которая является полной factorialфункцией, которая может быть выражена как объединение

${\displaystyle \bigcup _{i\in \mathbb {N} }F^{i}(\{\}).}$

Найденная нами неподвижная точка является наименьшей неподвижной точкой F , поскольку наша итерация началась с наименьшего элемента в области (пустого множества). Чтобы доказать это, нам нужна более сложная теорема о неподвижной точке, такая как теорема Кнастера–Тарского .

Концепция доменов мощности была разработана для того, чтобы дать денотационную семантику недетерминированным последовательным программам. Записывая P для конструктора домена мощности, домен P ( D ) является доменом недетерминированных вычислений типа, обозначенного D .

В предметно-теоретических моделях недетерминизма существуют трудности со справедливостью и неограниченностью . ^[7]

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

Недавно Винскель и другие предложили категорию профункторов в качестве теории доменов для параллелизма. ^{[10] [11]}

Состояние (например, куча) и простые императивные функции можно напрямую смоделировать в денотационном семантике, описанной выше. Основная идея заключается в том, чтобы рассматривать команду как частичную функцию в некоторой области состояний. Значение " x:=3" тогда является функцией, которая переводит состояние в состояние с 3назначенным x. Оператор последовательности " ;" обозначается композицией функций. Конструкции с фиксированной точкой затем используются для придания семантики циклическим конструкциям, таким как " while".

Все становится сложнее при моделировании программ с локальными переменными. Один из подходов заключается в том, чтобы больше не работать с доменами, а вместо этого интерпретировать типы как функторы из некоторой категории миров в категорию доменов. Затем программы обозначаются естественными непрерывными функциями между этими функторами. ^{[12] [13]}

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

 список  типов данных =  Минусы  nat  *  list |  Пусто  

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

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

тип данных  D  =  D  из  ( D  →  D )

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

Полиморфные типы данных — это типы данных, которые определяются параметром. Например, тип α lists определяется как

 тип данных α  список  =  Минусы  α  *  α список | Пустой    

Списки натуральных чисел, таким образом, имеют тип nat list, а списки строк — тип string list.

Некоторые исследователи разработали доменные модели полиморфизма. Другие исследователи также моделировали параметрический полиморфизм в рамках конструктивных теорий множеств.

Недавнее направление исследований было посвящено денотационной семантике для языков программирования, основанных на объектах и ​​классах. ^[14]

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

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

Этот открытый вопрос был в основном решен в 1990-х годах с развитием игровой семантики , а также методов, включающих логические отношения . ^[16] Более подробную информацию см. на странице PCF.

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

В этом контексте понятия из денотационной семантики, такие как полная абстракция, помогают удовлетворить проблемы безопасности. ^{[17] [18]}

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

1. Независимость от синтаксиса : обозначения программ не должны включать синтаксис исходного языка.
2. Адекватность (или обоснованность) : все наблюдаемо различные программы имеют различные обозначения;
3. Полная абстракция : все эквивалентные с точки зрения наблюдения программы имеют одинаковые обозначения.

Для семантики в традиционном стиле адекватность и полная абстракция могут быть примерно поняты как требование, чтобы «операционная эквивалентность совпадала с денотационным равенством». Для денотационной семантики в более интенсиональных моделях, таких как модель актора и исчисления процессов , существуют различные понятия эквивалентности в каждой модели, и поэтому концепции адекватности и полной абстракции являются предметом споров и их сложнее определить. Кроме того, математическая структура операционной семантики и денотационной семантики может стать очень близкой.

Дополнительные желательные свойства, которые мы могли бы захотеть сохранить между операционной и денотативной семантикой:

1. Конструктивизм : Конструктивизм занимается вопросом, можно ли с помощью конструктивных методов показать существование элементов предметной области.
2. Независимость денотационной и операционной семантики : Денотационная семантика должна быть формализована с использованием математических структур, которые независимы от операционной семантики языка программирования; Однако базовые концепции могут быть тесно связаны. См. раздел о композиционности ниже.
3. Полная полнота или определимость : каждый морфизм семантической модели должен быть обозначением программы. ^[19]

Важным аспектом денотационной семантики языков программирования является композиционность, посредством которой денотация программы строится из денотаций ее частей. Например, рассмотрим выражение "7 + 4". В этом случае композиционность заключается в том, чтобы предоставить значение для "7 + 4" в терминах значений "7", "4" и "+".

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

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

Теперь значение составного выражения (7+4) определяется путем составления трех функций 〚⊢7: nat〛:1→ _⊥ , 〚⊢4: 〛:1→ _⊥ , и 〚x : , y : ⊢ x + y : 〛: _⊥ × _⊥ → _⊥ .${\displaystyle \mathbb {N} }$nat${\displaystyle \mathbb {N} }$natnatnat${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

На самом деле, это общая схема для композиционной денотационной семантики. Здесь нет ничего конкретного о доменах и непрерывных функциях. Вместо этого можно работать с другой категорией . Например, в игровой семантике категория игр имеет игры как объекты и стратегии как морфизмы: мы можем интерпретировать типы как игры, а программы как стратегии. Для простого языка без общей рекурсии мы можем обойтись категорией множеств и функций . Для языка с побочными эффектами мы можем работать в категории Клейсли для монады. Для языка с состоянием мы можем работать в категории функторов . Милнер выступал за моделирование местоположения и взаимодействия, работая в категории с интерфейсами как объектами и биграфами как морфизмами. ^[20]

По словам Даны Скотт (1980): ^[21]

Семантика не обязательно должна определять реализацию, но она должна предоставлять критерии, показывающие, что реализация является правильной.

По данным Клингера (1981): ^{[22] : 79}

Однако обычно формальная семантика обычного последовательного языка программирования сама по себе может быть интерпретирована как (неэффективная) реализация языка. Однако формальная семантика не всегда должна обеспечивать такую ​​реализацию, и вера в то, что семантика должна обеспечивать реализацию, приводит к путанице относительно формальной семантики параллельных языков. Такая путаница становится болезненно очевидной, когда говорят, что наличие неограниченного недетерминизма в семантике языка программирования подразумевает, что язык программирования не может быть реализован.

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

Учебники

Конспект лекций

Другие ссылки

В Wikibook Haskell есть страница по теме: Денотационная семантика

• Денотационная семантика. Обзор книги Ллойда Эллисона
• Шрайнер, Вольфганг (1995). «Структура языков программирования I: Денотационная семантика». Заметки к курсу .