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

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

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

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

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

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

Денотационная семантика была разработана для современных языков программирования, которые используют такие возможности, как параллелизм и исключения , например, Concurrent ML , ^[4] ЦСП , ^[5] и Хаскель . ^[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) { if (n == 0) then return 1; else return n * factorial(n-1); }

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

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

int factorial_nonrecursive(Map<int,int> factorial_less_defined, int n)
{
  if (n == 0) then return 1;
  else if (fprev = lookup(factorial_less_defined, n-1)) then
    return n * fprev;
  else
    return NOT_DEFINED;
}

Map<int,int> F(Map<int,int> factorial_less_defined)
{ 
  Map<int,int> new_factorial = Map.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 раз .

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

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

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

\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]

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

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

datatype list = Cons of nat * list | Empty

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

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

datatype D = D of (D → D)

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

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

datatype α list = Cons of α * α list | Empty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

^ Jump up to: Перейти обратно: ^а ^б Дана С. Скотт. Очерк математической теории вычислений . Техническая монография PRG-2, Вычислительная лаборатория Оксфордского университета, Оксфорд, Англия, ноябрь 1970 г.
^ Jump up to: Перейти обратно: ^а ^б ^с ^д Дана Скотт и Кристофер Стрейчи . К математической семантике компьютерных языков . Техническая монография Оксфордской исследовательской группы по программированию. ПРГ-6. 1971.
^ Ян Юрьенс. J. Игры в семантике языков программирования – элементарное введение. Synthese 133, 131–158 (2002). https://doi.org/10.1023/A:1020883810034
^ Джон Реппи «Параллельное машинное обучение: проектирование, применение и семантика» в Springer-Verlag, Конспекты лекций по информатике , Vol. 693. 1993 г.
^ Jump up to: Перейти обратно: ^а ^б А. В. Роско . «Теория и практика параллелизма» Прентис-Холл. Пересмотрено в 2005 году.
^ Саймон Пейтон Джонс , Аластер Рид, Фергюс Хендерсон, Тони Хоар и Саймон Марлоу. « Семантика неточных исключений » Конференция по проектированию и реализации языков программирования. 1999.
^ Леви, Пол Блейн (2007). «Амб нарушает благоразумие, а земной амб нет» . Электрон. Примечания Теор. Вычислить. Наука . 173 : 221–239. дои : 10.1016/j.entcs.2007.02.036 .
^ Семантика структуры событий для CCS и родственных языков . Отчет об исследовании DAIMI, Орхусский университет, 67 стр., апрель 1983 г.
^ Ниссим Франсез , КАР Хоар , Дэниел Леманн и Виллем-Поль де Ровер . « Семантика недетерминизма, параллелизма и коммуникации », Журнал компьютерных и системных наук . Декабрь 1979 года.
^ Каттани, Джан Лука; Винскель, Глинн (2005). «Профункторы, открытые карты и бисимуляция». Математические структуры в информатике . 15 (3): 553–614. CiteSeerX 10.1.1.111.6243 . дои : 10.1017/S0960129505004718 . S2CID 16356708 .
^ Найгаард, Миккель; Винскель, Глинн (2004). «Теория предметной области параллелизма» . Теор. Вычислить. Наука . 316 (1–3): 153–190. дои : 10.1016/j.tcs.2004.01.029 .
^ Питер В. О'Хирн , Джон Пауэр, Роберт Д. Теннент , Макото Такэяма. Еще раз о синтаксическом контроле интерференции. Электрон. Примечания Теор. Вычислить. наук. 1. 1995.
^ Фрэнк Дж. Олес. Теоретико-категорный подход к семантике программирования . Докторская диссертация, Сиракузский университет , Нью-Йорк, США. 1982.
^ Реус, Бернхард; Штрайхер, Томас (2004). «Семантика и логика объектных исчислений» . Теор. Вычислить. Наука . 316 (1): 191–213. дои : 10.1016/j.tcs.2004.01.030 .
^ Байо, П. (2004). «Стратифицированные когерентные пространства: денотатационная семантика легкой линейной логики» . Теор. Вычислить. Наука . 318 (1–2): 29–55. дои : 10.1016/j.tcs.2003.10.015 .
^ О'Хирн, PW; Рике, JG (июль 1995 г.). «Логические отношения Крипке и ПКФ» . Информация и вычисления . 120 (1): 107–116. дои : 10.1006/inco.1995.1103 . S2CID 6886529 .
^ Мартин Абади. «Защита при переводах с языков программирования». Учеб. ICALP'98 . ЛНКС 1443. 1998.
^ Кеннеди, Эндрю (2006). «Защита модели программирования .NET» . Теор. Вычислить. Наука . 364 (3): 311–7. дои : 10.1016/j.tcs.2006.08.014 .
^ Кюрьен, Пьер-Луи (2007). «Определимость и полная абстракция» . Электронные заметки по теоретической информатике . 172 : 301–310. дои : 10.1016/j.entcs.2007.02.011 .
^ Милнер, Робин (2009). Пространство и движение общающихся агентов . Издательство Кембриджского университета. ISBN 978-0-521-73833-0 . Черновик 2009 г. Архивировано 2 апреля 2012 г. в Wayback Machine .
^ «Что такое денотационная семантика?», Серия выдающихся лекций Лаборатории компьютерных наук Массачусетского технологического института, 17 апреля 1980 г., цитируется в Clinger (1981).
^ Клингер, Уильям Д. (май 1981 г.). Основы акторной семантики (кандидатская диссертация). Массачусетский технологический институт. hdl : 1721.1/6935 . АИТР-633.

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

Учебники

Милн, РЭ; Стрейчи, К. (1976). Теория семантики языков программирования . ISBN 978-1-5041-2833-9 .
Гордон, MJC (2012) [1979]. Денотационное описание языков программирования: Введение . Спрингер. ISBN 978-1-4612-6228-2 .
Стой, Джозеф Э. (1977). Денотационная семантика: подход Скотта-Стрейчи к семантике языка программирования . МТИ Пресс. ISBN 978-0-262-19147-0 . (Классический, хотя и устаревший учебник.)
Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка . Аллин и Бэкон. ISBN 978-0-205-10450-5 .
- сейчас распродан; доступна бесплатная электронная версия: Шмидт, Дэвид А. (1997) [1986]. Денотационная семантика: методология развития языка . Канзасский государственный университет.
Гюнтер, Карл (1992). Семантика языков программирования: структуры и методы . МТИ Пресс. ISBN 978-0-262-07143-7 .
Винскель, Глинн (1993). Формальная семантика языков программирования . МТИ Пресс. ISBN 978-0-262-73103-4 .
Теннент, Р.Д. (1994). «Денотативная семантика». В Абрамский С.; Габбай, Дов М.; Майбаум, TSE (ред.). Семантические структуры . Справочник по логике в информатике. Том. 3. Издательство Оксфордского университета. стр. 169–322. ISBN 978-0-19-853762-5 .
Абрамский, С. ; Юнг, А. (1994). «Теория предметной области» (PDF) . Абрамский, Габбай и Майбаум 1994 .
Столтенберг-Хансен, В.; Линдстрем, И.; Гриффор, ER (1994). Математическая теория областей . Издательство Кембриджского университета. ISBN 978-0-521-38344-8 .

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

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

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

Грейф, Ирен (август 1975 г.). Семантика взаимодействия параллельных процессов (PDF) (кандидатская диссертация). Проект МАК. Массачусетский технологический институт. АДА016302.
Плоткин, Г.Д. (1976). «Конструкция области власти». СИАМ Дж. Компьютер . 5 (3): 452–487. CiteSeerX 10.1.1.158.4318 . дои : 10.1137/0205035 .
Дейкстра, Эдсгер В. (1976). Дисциплина программирования . Ряд Прентиса-Холла в автоматических вычислениях. Энглвуд Клиффс, ISBN Нью-Джерси 0-13-215871-Х . OCLC 1958445 . {{cite book}}: CS1 maint: отсутствует местоположение издателя ( ссылка )
Апт, Кшиштоф Р .; де Баккер, JW (1976). Упражнения по денотационной семантике . Департамент компьютерных наук. Амстердам: Математический центр. OCLC 63400684 .
Де Баккер, JW (1976). «Пересмотр наименьших фиксированных точек» . Теоретическая информатика . 2 (2): 155–181. дои : 10.1016/0304-3975(76)90031-1 .
Смит, Майкл Б. (1978). «Домены власти» . Дж. Компьютер. Сист. Наука . 16 : 23–36. дои : 10.1016/0022-0000(78)90048-X .
Франсез, Ниссим; Хоар, ЦАР; Леманн, Дэниел; де Ровер, Виллем-Поль (декабрь 1979 г.). Семантика недетерминизма, параллелизма и коммуникации . Конспекты лекций по информатике. Том. 64. стр. 191–200. дои : 10.1007/3-540-08921-7_67 . hdl : 1874/15886 . ISBN 978-3-540-08921-6 . {{cite book}}: |work= игнорируется ( помогите )
Линч, Нэнси ; Фишер, Майкл Дж. (1979). «Об описании поведения распределенных систем» . Ин Кан, Г. (ред.). Семантика параллельных вычислений: материалы международного симпозиума, Эвиан, Франция, 2-4 июля 1979 г. Спрингер. ISBN 978-3-540-09511-8 .
Шварц, Джеральд (1979). «Денотационная семантика параллелизма». Кан 1979 .
Уодж, Уильям (1979). «Расширенное лечение тупиковой ситуации потока данных». Кан 1979 .
Назад, Ральф-Йохан (1980). «Семантика неограниченного недетерминизма» . Ин де Баккер, Жако; ван Леувен, Ян (ред.). Автоматы, языки и программирование . Конспекты лекций по информатике. Том. 85. Берлин, Гейдельберг: Шпрингер. стр. 51–63. дои : 10.1007/3-540-10003-2_59 . ISBN 978-3-540-39346-7 . OCLC 476017025 .
Парк, Дэвид (1980). «О семантике справедливого параллелизма» . В Бьёрнере, Дайнс (ред.). Абстрактные спецификации программного обеспечения (PDF) . Конспекты лекций по информатике. Том. 86. Берлин, Гейдельберг: Springer Berlin Heidelberg. стр. 504–526. дои : 10.1007/3-540-10007-5_47 . ISBN 978-3-540-10007-2 .
Эллисон, Л. (1986). Практическое введение в денотационную семантику . Издательство Кембриджского университета. ISBN 978-0-521-31423-7 .
Америка, П.; де Баккер, Дж.; Кок, Дж. Н.; Руттен, Дж. (1989). «Денотационная семантика параллельного объектно-ориентированного языка» . Информация и вычисления . 83 (2): 152–205. дои : 10.1016/0890-5401(89)90057-6 . S2CID 2405175 .
Шмидт, Дэвид А. (1994). Структура типизированных языков программирования . МТИ Пресс. ISBN 978-0-262-69171-0 .

Внешние ссылки [ править ]

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

[ropas.snu.ac.kr-1] Jump up to: Перейти обратно: ^а ^б Дана С. Скотт. Очерк математической теории вычислений . Техническая монография PRG-2, Вычислительная лаборатория Оксфордского университета, Оксфорд, Англия, ноябрь 1970 г.

[Research_Group_Technical_Monograph_1971-2] Jump up to: Перейти обратно: ^а ^б ^с ^д Дана Скотт и Кристофер Стрейчи . К математической семантике компьютерных языков . Техническая монография Оксфордской исследовательской группы по программированию. ПРГ-6. 1971.

[3] Ян Юрьенс. J. Игры в семантике языков программирования – элементарное введение. Synthese 133, 131–158 (2002). https://doi.org/10.1023/A:1020883810034

[4] Джон Реппи «Параллельное машинное обучение: проектирование, применение и семантика» в Springer-Verlag, Конспекты лекций по информатике , Vol. 693. 1993 г.

[Roscoe-5] Jump up to: Перейти обратно: ^а ^б А. В. Роско . «Теория и практика параллелизма» Прентис-Холл. Пересмотрено в 2005 году.

[6] Саймон Пейтон Джонс , Аластер Рид, Фергюс Хендерсон, Тони Хоар и Саймон Марлоу. « Семантика неточных исключений » Конференция по проектированию и реализации языков программирования. 1999.

[7] Леви, Пол Блейн (2007). «Амб нарушает благоразумие, а земной амб нет» . Электрон. Примечания Теор. Вычислить. Наука . 173 : 221–239. дои : 10.1016/j.entcs.2007.02.036 .

[8] Семантика структуры событий для CCS и родственных языков . Отчет об исследовании DAIMI, Орхусский университет, 67 стр., апрель 1983 г.

[9] Ниссим Франсез , КАР Хоар , Дэниел Леманн и Виллем-Поль де Ровер . « Семантика недетерминизма, параллелизма и коммуникации », Журнал компьютерных и системных наук . Декабрь 1979 года.

[10] Каттани, Джан Лука; Винскель, Глинн (2005). «Профункторы, открытые карты и бисимуляция». Математические структуры в информатике . 15 (3): 553–614. CiteSeerX 10.1.1.111.6243 . дои : 10.1017/S0960129505004718 . S2CID 16356708 .

[11] Найгаард, Миккель; Винскель, Глинн (2004). «Теория предметной области параллелизма» . Теор. Вычислить. Наука . 316 (1–3): 153–190. дои : 10.1016/j.tcs.2004.01.029 .

[12] Питер В. О'Хирн , Джон Пауэр, Роберт Д. Теннент , Макото Такэяма. Еще раз о синтаксическом контроле интерференции. Электрон. Примечания Теор. Вычислить. наук. 1. 1995.

[13] Фрэнк Дж. Олес. Теоретико-категорный подход к семантике программирования . Докторская диссертация, Сиракузский университет , Нью-Йорк, США. 1982.

[14] Реус, Бернхард; Штрайхер, Томас (2004). «Семантика и логика объектных исчислений» . Теор. Вычислить. Наука . 316 (1): 191–213. дои : 10.1016/j.tcs.2004.01.030 .

[15] Байо, П. (2004). «Стратифицированные когерентные пространства: денотатационная семантика легкой линейной логики» . Теор. Вычислить. Наука . 318 (1–2): 29–55. дои : 10.1016/j.tcs.2003.10.015 .

[16] О'Хирн, PW; Рике, JG (июль 1995 г.). «Логические отношения Крипке и ПКФ» . Информация и вычисления . 120 (1): 107–116. дои : 10.1006/inco.1995.1103 . S2CID 6886529 .

[17] Мартин Абади. «Защита при переводах с языков программирования». Учеб. ICALP'98 . ЛНКС 1443. 1998.

[18] Кеннеди, Эндрю (2006). «Защита модели программирования .NET» . Теор. Вычислить. Наука . 364 (3): 311–7. дои : 10.1016/j.tcs.2006.08.014 .

[19] Кюрьен, Пьер-Луи (2007). «Определимость и полная абстракция» . Электронные заметки по теоретической информатике . 172 : 301–310. дои : 10.1016/j.entcs.2007.02.011 .

[20] Милнер, Робин (2009). Пространство и движение общающихся агентов . Издательство Кембриджского университета. ISBN 978-0-521-73833-0 . Черновик 2009 г. Архивировано 2 апреля 2012 г. в Wayback Machine .

[21] «Что такое денотационная семантика?», Серия выдающихся лекций Лаборатории компьютерных наук Массачусетского технологического института, 17 апреля 1980 г., цитируется в Clinger (1981).

[clinger1981-22] Клингер, Уильям Д. (май 1981 г.). Основы акторной семантики (кандидатская диссертация). Массачусетский технологический институт. hdl : 1721.1/6935 . АИТР-633.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]