Из Википедии, бесплатной энциклопедии
  (Перенаправлено из полностью абстрактного )
Перейти к навигации Перейти к поиску
Семантика
ЛингвистическийЛогический
Вычисление
Типы
Теория
Анализ
Приложения

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

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

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

Историческое развитие [ править ]

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

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

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

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

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

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

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

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

Поучительно представить эту цепочку итераций для «частичной факториальной функции» F как F 0 , F 1 , F 2 , ..., где F n означает, что F применяется n раз .

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

Этот итерационный процесс строит последовательность частичных функций от ℕ до. Частичные функции образуют полный по цепочке частичный порядок с использованием в качестве порядка. Кроме того, этот итерационный процесс лучших приближений факториальной функции формирует расширяющее (также называемое прогрессивным) отображение, потому что каждое из них использует ⊆ в качестве упорядочения. Таким образом, по теореме о неподвижной точке (в частности, по теореме Бурбаки – Витта ) существует неподвижная точка для этого итерационного процесса.

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

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

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

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

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

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

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

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

Денотационная семантика состояния [ править ]

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

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

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

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

Тип данных  список  =  Cons  из  физ  *  список  |  Пустой

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

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

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

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

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

Тип данных  α  список  =  Cons  из  альфа  *  α  список  |  Пустой

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

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

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

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

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

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

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

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

Денотационная семантика как перевод из источника в источник [ править ]

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

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

Абстракция [ править ]

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

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

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

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

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

Композиционность [ править ]

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

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

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

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

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

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

Согласно Дане Скотт (1980): [20]

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

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

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

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

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

Ссылки [ править ]

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

Дальнейшее чтение [ править ]

Учебники
  • Милн, RE; Стрейчи, К. (1976). Теория семантики языков программирования . ISBN 978-1-5041-2833-9.
  • Гордон, MJC (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). «Денотационная семантика». По Абрамскому, С .; Габбай, Дов М .; Майбаум, TSE (ред.). Семантические структуры . Справочник по логике в информатике. 3 . Издательство Оксфордского университета. С. 169–322. ISBN 978-0-19-853762-5.
  • Абрамский, С .; Юнг, А. (1994). «Теория предметной области» (PDF) . Абрамский, Габбай и Майбаум 1994 .
  • Stoltenberg-Hansen, V .; Lindström, I .; Гриффор, ER (1994). Математическая теория областей . Издательство Кембриджского университета. ISBN 978-0-521-38344-8.
Конспект лекций
  • Винскель, Глинн. «Денотационная семантика» (PDF) . Кембриджский университет.
Прочие ссылки
  • Грейф, Ирэн (август 1975 г.). Семантика взаимодействующих параллельных процессов (PDF) (PhD). Проект MAC. Массачусетский Институт Технологий. ADA016302.
  • Плоткин Г.Д. (1976). «Энергетическая конструкция». SIAM J. Comput . 5 (3): 452–487. CiteSeerX  10.1.1.158.4318 . DOI : 10.1137 / 0205035 .
  • Эдсгер Дейкстра . Дисциплина программирования Prentice Hall. 1976 г.
  • Krzysztof R. Apt, JW de Bakker. Упражнения по денотационной семантике MFCS 1976: 1-11
  • де Баккер, JW (1976). «Повторное посещение наименьших фиксированных точек». Теор. Comput. Sci . 2 (2): 155–181. DOI : 10.1016 / 0304-3975 (76) 90031-1 .
  • Смит, Майкл Б. (1978). «Силовые домены». J. Comput. Syst. Sci . 16 : 23–36. DOI : 10.1016 / 0022-0000 (78) 90048-X .
  • Франсез, Ниссим; Хоар, ЦАР; Леманн, Даниэль; де Ровер, Виллем-Поль (декабрь 1979 г.). Семантика недетерминизма, параллелизма и коммуникации . Журнал компьютерных и системных наук . Конспект лекций по информатике. 64 . С. 191–200. DOI : 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.
  • Schwartz, Jerald (1979). "Denotational semantics of parallelism". Kahn 1979.
  • Wadge, William (1979). "An extensional treatment of dataflow deadlock". Kahn 1979.
  • Ralph-Johan Back. "Semantics of Unbounded Nondeterminism" ICALP 1980.
  • David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.
  • Clinger, W.D. (1981). "Foundations of Actor Semantics" (PhD). Massachusetts Institute of Technology. hdl:1721.1/6935. AITR-633. Cite journal requires |journal= (help)
  • Allison, L. (1986). A Practical Introduction to Denotational Semantics. Cambridge University Press. ISBN 978-0-521-31423-7.
  • America, P.; de Bakker, J.; Kok, J.N.; Rutten, J. (1989). "Denotational semantics of a parallel object-oriented language". Information and Computation. 83 (2): 152–205. doi:10.1016/0890-5401(89)90057-6.
  • Schmidt, David A. (1994). The Structure of Typed Programming Languages. MIT Press. ISBN 978-0-262-69171-0.

External links[edit]

  • Denotational Semantics. Overview of book by Lloyd Allison
  • Schreiner, Wolfgang (1995). "Structure of Programming Languages I: Denotational Semantics". Course notes.