Денотационная семантика - Denotational semantics - Wikipedia

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

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

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

Историческое развитие

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

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

Значения рекурсивных программ

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

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

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

int факториал(int п) { если (п == 0) тогда возвращаться 1; еще возвращаться п * факториал(п-1); }

Решение состоит в том, чтобы придать значения приближенным значениям. Факториальная функция - это общая функция от ℕ до ℕ (определяется всюду в своей области определения), но мы моделируем его как частичная функция. Вначале мы начинаем с пустая функция (пустой набор). Затем мы добавляем упорядоченную пару (0,1) к функции, чтобы получить другую частичную функцию, которая лучше аппроксимирует факториальную функцию. После этого мы добавляем еще одну упорядоченную пару (1,1), чтобы создать еще лучшее приближение.

Поучительно подумать об этой цепочке итераций для «частичной факториальной функции». F в качестве F⁰, F¹, F², ... куда F^п указывает F применяемый п раз.

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

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

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

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

Здесь символ «⊔» означает направленное присоединение (из направленные наборы ), что означает «наименьшая верхняя граница». Направленное соединение - это, по сути, присоединиться направленных наборов.

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

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

Есть трудности с честностью и безграничность в теоретико-предметных моделях недетерминизма.^[6]

Денотационная семантика параллелизма

Многие исследователи утверждают, что приведенные выше теоретико-предметные модели недостаточны для более общего случая параллельное вычисление. По этой причине различные новые модели были введены. В начале 1980-х люди начали использовать стиль денотационной семантики, чтобы дать семантику для параллельных языков. Примеры включают Работа Уилла Клингера с актером-моделью; Работа Глинна Винскеля с ивент-структурами и сети петри;^[7] и работа Francez, Hoare, Lehmann и de Roever (1979) по семантике трассировки для CSP.^[8] Все эти направления исследований остаются в стадии расследования (см., Например, различные денотационные модели для CSP^[4]).

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

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

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

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

Обозначения типов данных

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

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

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

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

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

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

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

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

Таким образом, списки натуральных чисел имеют тип список нац, а списки строк имеют список строк.

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

Недавняя область исследований включала денотационную семантику для языков программирования на основе объектов и классов.^[13]

Денотационная семантика для программ ограниченной сложности

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

Денотационная семантика последовательности

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

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

Денотационная семантика как перевод от источника к источнику

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

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

Абстракция

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

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

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

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

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

Композиционность

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

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

1. Начнем с описания значений типов нашего языка: значение каждого типа должно быть областью. Обозначим через 〚τ〛 область, обозначающую тип τ. Например, значение типа нац должна быть областью натуральных чисел: 〚нац〛 = ℕ_⊥.
2. Из значения типов мы получаем значение контекстов ввода. Мы установили [ Икс₁: τ₁,..., Икс_п: τ_п〛 = 〚Τ₁〛 × ... × 〚τ_п〛. Например, [Икс:нац,у:нац>〛 = ℕ_⊥× ℕ_⊥. В качестве особого случая значение пустого контекста ввода без переменных - это область с одним элементом, обозначенным 1.
3. Наконец, мы должны придать смысл каждому фрагменту программы в контексте ввода. Предположим, что п является фрагментом программы типа σ, в контексте ввода Γ, часто пишется как Γ⊢п: σ. Тогда смысл этой программы-в-контексте-типизации должен быть непрерывной функцией Γ⊢п: σ〛: 〚Γ〛 → 〚σ〛. Например, №7:нац〛: 1 → ℕ_⊥ - функция с постоянной цифрой 7, а whileИкс:нац,у:нац⊢Икс+у:нац〛: ℕ_⊥× ℕ_⊥→ ℕ_⊥ это функция, которая складывает два числа.

Теперь смысл составного выражения (7 + 4) определяется составлением трех функций 〚⊢7:нац〛: 1 → ℕ_⊥, 〚⊢4:нац〛: 1 → ℕ_⊥, и [Икс:нац,у:нац⊢Икс+у:нац〛: ℕ_⊥× ℕ_⊥→ ℕ_⊥.

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

Семантика против реализации

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

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

По словам Клингера (1981):^[21]:79

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

Связь с другими областями информатики

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

Рекомендации

1. Дана С. Скотт. Очерк математической теории вычислений. Техническая монография PRG-2, вычислительная лаборатория Оксфордского университета, Оксфорд, Англия, ноябрь 1970 г.
2. Дана Скотт и Кристофер Стрейчи. К математической семантике компьютерных языков Техническая монография Oxford Programming Research Group. ПРГ-6. 1971 г.
3. Джон Реппи «Параллельное машинное обучение: дизайн, применение и семантика» в Springer-Verlag, Конспект лекций по информатике, Vol. 693. 1993
4. А. В. Роско. "Теория и практика параллелизма" Prentice-Hall. Пересмотрено в 2005 г.
5. Саймон Пейтон Джонс, Аластер Рид, Фергус Хендерсон, Тони Хоар, и Саймон Марлоу. "Семантика неточных исключений "Конференция по разработке и реализации языков программирования. 1999.
6. Леви, Пол Блейн (2007). "Амбициозный удар нарушает точность стрельбы, наземный - нет". Электр. Примечания Теор. Comput. Наука. 173: 221–239. Дои:10.1016 / j.entcs.2007.02.036.
7. Семантика структуры событий для CCS и родственных языков. Отчет об исследовании DAIMI, Орхусский университет, 67 стр., Апрель 1983 г.
8. Ниссим Франсез, К. А. Р. Хоар, Даниэль Леманн и Виллем-Поль де Ровер. "Семантика недетерминизма, параллелизма и коммуникации ", Журнал компьютерных и системных наук. Декабрь 1979 г.
9. Каттани, Джан Лука; Винскель, Глинн (2005). «Профункторы, открытые карты и бисимуляция». Математические структуры в информатике. 15 (3): 553–614. CiteSeerX  10.1.1.111.6243. Дои:10.1017 / S0960129505004718.
10. Найгаард, Миккель; Винскель, Глинн (2004). «Теория предметной области для параллелизма». Теор. Comput. Наука. 316 (1–3): 153–190. Дои:10.1016 / j.tcs.2004.01.029.
11. Питер В. О'Хирн, Джон Пауэр, Роберт Д. Теннент, Макото Такеяма. Возвращение к синтаксическому контролю помех. Электр. Примечания Теор. Comput. Sci. 1. 1995.
12. Фрэнк Дж. Олес. Теоретико-категориальный подход к семантике программирования. Кандидатская диссертация, Сиракузский университет, Нью-Йорк, США. 1982 г.
13. Реус, Бернхард; Штрейхер, Томас (2004). «Семантика и логика объектных исчислений». Теор. Comput. Наука. 316 (1): 191–213. Дои:10.1016 / j.tcs.2004.01.030.
14. Байо, П. (2004). «Стратифицированные пространства когерентности: денотационная семантика для легкой линейной логики». Теор. Comput. Наука. 318 (1–2): 29–55. Дои:10.1016 / j.tcs.2003.10.015.
15. O'Hearn, P.W .; Riecke, J.G. (Июль 1995 г.). «Логические отношения Крипке и ПКФ». Информация и вычисления. 120 (1): 107–116. Дои:10.1006 / inco.1995.1103.
16. Мартин Абади. «Защита при переводе на языки программирования». Proc. ICALP'98. LNCS 1443.1998.
17. Кеннеди, Эндрю (2006). «Защита модели программирования .NET». Теор. Comput. Наука. 364 (3): 311–7. Дои:10.1016 / j.tcs.2006.08.014.
18. Куриен, Пьер-Луи (2007). «Определимость и полная абстракция». Электронные заметки по теоретической информатике. 172: 301–310. Дои:10.1016 / j.entcs.2007.02.011.
19. Милнер, Робин (2009). Пространство и движение сообщающихся агентов. Издательство Кембриджского университета. ISBN  978-0-521-73833-0. Проект 2009 г. В архиве 2012-04-02 в Wayback Machine.
20. «Что такое денотационная семантика?», Серия выдающихся лекций Лаборатории информатики Массачусетского технологического института, 17 апреля 1980 г., цитируется по Clinger (1981).
21. Клингер, Уильям Д. (1981). «Основы актерской семантики» (PhD). Массачусетский Институт Технологий. HDL:1721.1/6935. АИТР-633.

дальнейшее чтение

Учебники

• Milne, R.E .; Стрейчи, К. (1976). Теория семантики языка программирования. ISBN  978-1-5041-2833-9.
• Гордон, M.J.C. (2012) [1979]. Денотационное описание языков программирования: введение. Springer. ISBN  978-1-4612-6228-2.
• Стой, Джозеф Э. (1977). Денотационная семантика: подход Скотта-Стрейчи к семантике языков программирования. MIT Press. ISBN  978-0262191470. (Классический устаревший учебник.)
• Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка. Аллин и Бэкон. ISBN  978-0-205-10450-5. (сейчас не издается; доступна бесплатная электронная версия )
• Гюнтер, Карл (1992). Семантика языков программирования: структуры и методы. MIT Press. ISBN  978-0262071437.
• Винскель, Глинн (1993). Формальная семантика языков программирования. MIT Press. ISBN  978-0262731034.
• Теннент, Р.Д. (1994). «Денотационная семантика». У Абрамского, С .; Габбай, Дов М .; Майбаум, Т.С.Э. (ред.). Семантические структуры. Справочник по логике в информатике. 3. Издательство Оксфордского университета. С. 169–322. ISBN  978-0-19-853762-5.
• Абрамский, С.; Юнг, А. (1994). «Теория предметной области» (PDF). Абрамский, Габбай и Майбаум 1994.
• Stoltenberg-Hansen, V .; Lindström, I .; Гриффор, Э. Р. (1994). Математическая теория областей. Издательство Кембриджского университета. ISBN  978-0-521-38344-8.

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

• Винскель, Глинн. «Денотационная семантика» (PDF). Кембриджский университет.

Прочие ссылки

• Грейф, Ирэн (август 1975). Семантика взаимодействующих параллельных процессов (PDF) (Кандидат наук). Проект MAC. Массачусетский Институт Технологий. ADA016302.
• Плоткин, Г. (1976). «Энергетическая конструкция». SIAM J. Comput. 5 (3): 452–487. CiteSeerX  10.1.1.158.4318. Дои:10.1137/0205035.
• Эдсгер Дейкстра. Дисциплина программирования Прентис Холл. 1976 г.
• Кшиштоф Р. Апт, Дж. В. де Баккер. Упражнения по денотационной семантике MFCS 1976: 1-11
• де Баккер, Дж. (1976). «Повторное посещение наименьших фиксированных точек». Теор. Comput. Наука. 2 (2): 155–181. Дои:10.1016/0304-3975(76)90031-1.
• Смит, Майкл Б. (1978). «Силовые домены». J. Comput. Syst. Наука. 16: 23–36. Дои:10.1016 / 0022-0000 (78) 90048-Х.
• Франсез, Ниссим; Hoare, C.A.R .; Леманн, Даниэль; де Ровер, Виллем-Поль (декабрь 1979 г.). Семантика недетерминизма, параллелизма и коммуникации. Журнал компьютерных и системных наук. Конспект лекций по информатике. 64. С. 191–200. Дои:10.1007/3-540-08921-7_67. HDL:1874/15886. ISBN  978-3-540-08921-6.
• Линч, Нэнси; Фишер, Майкл Дж. (1979). «Об описании поведения распределенных систем». В Кан, Г. (ред.). Семантика параллельных вычислений: материалы международного симпозиума, Эвиан, Франция, 2-4 июля 1979 г.. Springer. ISBN  978-3-540-09511-8.
• Шварц, Джеральд (1979). «Денотационная семантика параллелизма». Кан 1979.
• Уэдж, Уильям (1979). «Расширенная обработка тупика потока данных». Кан 1979.
• Ральф-Йохан Бэк. «Семантика неограниченного недетерминизма» ИКАЛП 1980.
• Дэвид Парк. О семантике справедливого параллелизма Материалы Зимней школы по формальной спецификации ПО. Springer-Verlag. 1980 г.
• Clinger, W.D. (1981). «Основы актерской семантики» (PhD). Массачусетский Институт Технологий. HDL:1721.1/6935. АИТР-633.
• Эллисон, Л. (1986). Практическое введение в денотационную семантику. Издательство Кембриджского университета. ISBN  978-0-521-31423-7.
• America, P .; de Bakker, J .; Kok, J.N .; Руттен, Дж. (1989). «Денотационная семантика параллельного объектно-ориентированного языка». Информация и вычисления. 83 (2): 152–205. Дои:10.1016/0890-5401(89)90057-6.
• Шмидт, Дэвид А. (1994). Структура типизированных языков программирования. MIT Press. ISBN  978-0-262-69171-0.

внешняя ссылка

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