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

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

6 мин чтения

100%

Источник: Denotational semantics — Wikipedia

Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.

Содержание

Введение

Изучение языков программирования с помощью математических объектов

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Важным аспектом денотационной семантики языков программирования является композиционность, посредством которой денотация программы строится из денотаций ее частей. Например, рассмотрим выражение "7 + 4". Композиционность в этом случае заключается в том, чтобы предоставить значение для "7 + 4" с точки зрения значений "7", "4" и "+". Базовая денотационная семантика в теории доменов является композиционной, поскольку она задается следующим образом. Начнем с рассмотрения фрагментов программы, то есть программ со свободными переменными. Контекст типизации присваивает тип каждой свободной переменной. Например, выражение (x + y) может рассматриваться в контексте типизации (x:, y:). Теперь мы даем денотационную семантику фрагментам программы, используя следующую схему. Начнем с описания значения типов нашего языка: значение каждого типа должно быть доменом. Мы пишем 〚τ〛 для домена, обозначающего тип τ. Например, значение типа ℕ должно быть доменом натуральных чисел: 〚ℕ〛 = ⊥. Из значения типов мы получаем значение для контекстов типизации. Мы устанавливаем 〚x1:τ1, ..., xn:τn〛 = 〚τ1〛 × ... × 〚τn〛. Например, 〚x:, y:〛 = ⊥ × ⊥. В качестве специального случая значение пустого контекста типизации, без переменных, является доменом с одним элементом, обозначаемым 1. Наконец, мы должны придать смысл каждому фрагменту программы в контексте типизации. Предположим, что P – это фрагмент программы типа σ в контексте типизации Γ, часто записываемый как Γ ⊢ P:σ. Тогда значение этой программы в контексте типизации должно быть непрерывной функцией 〚Γ ⊢ P:σ〛: 〚Γ〛 → 〚σ〛. Например, 〚⊢ 7:ℕ〛: 1 → ⊥ – это постоянная функция, возвращающая "7", а 〚x:, y: ⊢ x + y:ℕ〛: ⊥ × ⊥ → ⊥ – это функция, которая складывает два числа. Теперь значение составного выражения (7 + 4) определяется путем композиции трех функций 〚⊢ 7:ℕ〛: 1 → ⊥, 〚⊢ 4:ℕ〛: 1 → ⊥ и 〚x:, y: ⊢ x + y:ℕ〛: ⊥ × ⊥ → ⊥. Фактически, это общая схема для композиционной денотационной семантики. Здесь нет ничего специфичного относительно доменов и непрерывных функций. Можно работать с другой категорией. Например, в семантике игр категория игр имеет игры в качестве объектов и стратегии в качестве морфизмов: мы можем интерпретировать типы как игры, а программы как стратегии. Для простого языка без общей рекурсии мы можем обойтись категорией множеств и функций. Для языка с побочными эффектами мы можем работать в категории Клейсли для монады. Для языка с состоянием мы можем работать в категории функторов. Милнер выступал за моделирование местоположения и взаимодействия, работая в категории с интерфейсами в качестве объектов и биграфами в качестве морфизмов.

An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example, consider the expression "7 + 4". Compositionality in this case is to provide a meaning for "7 + 4" in terms of the meanings of "7", "4" and "+". A basic denotational semantics in domain theory is compositional because it is given as follows. We start by considering program fragments, i. e. programs with free variables. A typing context assigns a type to each free variable. For instance, in the expression (x + y) might be considered in a typing context (x:,y:). We now give a denotational semantics to program fragments, using the following scheme. We begin by describing the meaning of the types of our language: the meaning of each type must be a domain. We write 〚τ〛 for the domain denoting the type τ. For instance, the meaning of type should be the domain of natural numbers: 〚〛= ⊥. From the meaning of types we derive a meaning for typing contexts. We set 〚 x1:τ1, , xn:τn〛 = 〚 τ1〛× ×〚τn〛. For instance, 〚x:,y:〛= ⊥×⊥. As a special case, the meaning of the empty typing context, with no variables, is the domain with one element, denoted 1. Finally, we must give a meaning to each program fragment in typing context. Suppose that P is a program fragment of type σ, in typing context Γ, often written Γ⊢P:σ. Then the meaning of this program in typing context must be a continuous function 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛. For instance, 〚⊢7:〛:1→⊥ is the constantly "7" function, while 〚x:,y:⊢x+y:〛:⊥×⊥→⊥ is the function that adds two numbers. Now, the meaning of the compound expression (7+4) is determined by composing the three functions 〚⊢7:〛:1→⊥, 〚⊢4:〛:1→⊥, and 〚x:,y:⊢x+y:〛:⊥×⊥→⊥. In fact, this is a general scheme for compositional denotational semantics. There is nothing specific about domains and continuous functions here. One can work with a different category instead. For example, in game semantics, the category of games has games as objects and strategies as morphisms: we can interpret types as games, and programs as strategies. For a simple language without general recursion, we can make do with the category of sets and functions. For a language with side effects, we can work in the Kleisli category for a monad. For a language with state, we can work in a functor category. Milner has advocated modelling location and interaction by working in a category with interfaces as objects and bigraphs as morphisms.

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

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