Операционная семантика

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

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

Возможно, первым формальным воплощением операционной семантики было использование лямбда-исчисления для определения семантики Lisp . ^[1] Абстрактные машины в традиции машины SECD также тесно связаны.

История

Концепция операционной семантики была впервые использована при определении семантики Алгола 68. Следующее утверждение является цитатой из пересмотренного отчета Алгола 68:

Значение программы на строгом языке объясняется в терминах гипотетического компьютера, который выполняет набор действий, составляющих разработку этой программы. (Algol68, Раздел 2)

Первое использование термина «операциональная семантика» в его нынешнем значении приписывается Дане Скотту (Plotkin04). Далее следует цитата из основополагающей статьи Скотта о формальной семантике, в которой он упоминает «операциональные» аспекты семантики.

Конечно, очень хорошо стремиться к более «абстрактному» и «чистому» подходу к семантике, но если план должен быть хоть сколько-нибудь хорош, нельзя полностью игнорировать операциональные аспекты. (Scott70)

Подходы

Гордон Плоткин представил структурную операциональную семантику, Маттиас Феллейзен и Роберт Хиб — редукционную семантику ^[2] , а Жиль Кан — естественную семантику.

Семантика малых шагов

Структурно-операциональная семантика

Структурная операционная семантика (SOS, также называемая структурированной операционной семантикой или семантикой малых шагов ) была введена Гордоном Плоткиным в (Plotkin81) как логическое средство определения операционной семантики. Основная идея SOS заключается в определении поведения программы в терминах поведения ее частей, тем самым обеспечивая структурный, т. е. синтаксически-ориентированный и индуктивный , взгляд на операционную семантику. Спецификация SOS определяет поведение программы в терминах (набора) отношений перехода (отношений). Спецификации SOS принимают форму набора правил вывода , которые определяют допустимые переходы составного фрагмента синтаксиса в терминах переходов его компонентов.

Для простого примера рассмотрим часть семантики простого языка программирования; соответствующие иллюстрации даны в Plotkin81 и Hennessy90, а также в других учебниках. Пусть range по программам языка, и пусть range по состояниям (например, функции из ячеек памяти в значения). Если у нас есть выражения (ранжированные по ), значения ( ) и ячейки ( ), то команда обновления памяти будет иметь семантику: $C_{1},C_{2}$ $s$ $E$ $V$ $L$

${\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}$

Неформально правило гласит, что « если выражение в состоянии сводится к значению , то программа обновит состояние с помощью присваивания ». $E$ $s$ $V$ $L:=E$ $s$ $L=V$

Семантику последовательности можно задать следующими тремя правилами:

${\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}$

Неформально, первое правило гласит, что если программа в состоянии завершается в состоянии , то программа в состоянии сведется к программе в состоянии . (Вы можете думать об этом как о формализующем «Вы можете запустить , а затем запустить с использованием полученного хранилища памяти».) Второе правило гласит, что если программа в состоянии может свестись к программе с состоянием , то программа в состоянии сведется к программе в состоянии . (Вы можете думать об этом как о формализующем принципе для оптимизирующего компилятора: «Вам разрешено преобразовывать так, как если бы это было автономно, даже если это всего лишь первая часть программы».) Семантика структурна, поскольку значение последовательной программы определяется значением и значением . $C_{1}$ $s$ $s'$ $C_{1};C_{2}$ $s$ $C_{2}$ $s'$ $C_{1}$ $C_{2}$ $C_{1}$ $s$ $C_{1}'$ $s'$ $C_{1};C_{2}$ $s$ $C_{1}';C_{2}$ $s'$ $C_{1}$ $C_{1};C_{2}$ $C_{1}$ $C_{2}$

Если у нас также есть булевы выражения над состоянием, ранжированные по , то мы можем определить семантику команды while : $B$ ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$

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

Благодаря интуитивному виду и простой структуре SOS приобрел большую популярность и стал фактическим стандартом в определении операционной семантики. В качестве признака успеха, оригинальный отчет (так называемый отчет Aarhus) по SOS (Plotkin81) привлек более 1000 ссылок, согласно CiteSeer [1], что сделало его одним из самых цитируемых технических отчетов в области компьютерных наук .

Семантика сокращения

Семантика редукции — это альтернативное представление операционной семантики. Ее ключевые идеи были впервые применены к чисто функциональным вариантам вызова по имени и вызова по значению лямбда-исчисления Гордоном Плоткиным в 1975 году ^[3] и обобщены на функциональные языки более высокого порядка с императивными функциями Маттиасом Феллейзеном в его диссертации 1987 года. ^[4] Метод был далее разработан Маттиасом Феллейзеном и Робертом Хибом в 1992 году в полностью эквациональную теорию для управления и состояния . ^[2] Сама фраза «семантика редукции» была впервые придумана Феллейзеном и Дэниелом П. Фридманом в статье PARLE 1987 года. ^[5]

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

$\mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e$

Чтобы получить оператор присваивания в таком положении, он «всплывает» через применение функций и правую часть операторов присваивания, пока не достигнет нужной точки. Поскольку промежуточные выражения могут объявлять различные переменные, исчисление также требует правила вытеснения для выражений. Большинство опубликованных применений семантики редукции определяют такие «правила пузырька» с удобством контекстов оценки. Например, грамматика контекстов оценки в простом языке вызова по значению может быть задана как $\mathbf {let}$ $\mathbf {let}$

$E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e$

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

$E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}$

Это правило простого сокращения является правилом подъема из лямбда-исчисления Феллейзена и Хиба для операторов присваивания. Контексты оценки ограничивают это правило определенными терминами, но оно свободно применимо к любому термину, включая лямбды.

Следуя Плоткину, демонстрация полезности исчисления, полученного из набора правил редукции, требует (1) леммы Чёрча-Россера для одношагового отношения, которая индуцирует функцию оценки, и (2) леммы стандартизации Карри-Фейса для транзитивно-рефлексивного замыкания одношагового отношения, которая заменяет недетерминированный поиск в функции оценки на детерминированный левый/внешний поиск. Феллейзен показал, что императивные расширения этого исчисления удовлетворяют этим теоремам. Следствия этих теорем заключаются в том, что эквациональная теория — симметрично-транзитивно-рефлексивное замыкание — является обоснованным принципом рассуждения для этих языков. Однако на практике большинство приложений семантики редукции обходятся без исчисления и используют только стандартную редукцию (и оценщик, который может быть выведен из нее).

Семантика сокращения особенно полезна, учитывая легкость, с которой контексты оценки могут моделировать состояние или необычные конструкции управления (например, продолжения первого класса ). Кроме того, семантика сокращения использовалась для моделирования объектно-ориентированных языков, ^[6] систем контрактов , исключений, фьючерсов, вызова по потребности и многих других языковых функций. Тщательное современное рассмотрение семантики сокращения, в котором подробно обсуждаются несколько таких приложений, дано Маттиасом Феллейзеном, Робертом Брюсом Финдлером и Мэтью Флэттом в Semantics Engineering with PLT Redex . ^[7]

Семантика большого шага

Естественная семантика

Крупношаговая структурная операционная семантика также известна под названиями естественная семантика , реляционная семантика и оценочная семантика . ^[8] Крупношаговая операционная семантика была введена под названием естественная семантика Жилем Каном при представлении Mini-ML, чистого диалекта ML .

Определения с большим шагом можно рассматривать как определения функций или, в более общем смысле, отношений, интерпретирующих каждую языковую конструкцию в соответствующей области. Его интуитивность делает его популярным выбором для спецификации семантики в языках программирования, но у него есть некоторые недостатки, которые делают его неудобным или невозможным для использования во многих ситуациях, таких как языки с функциями, требующими интенсивного управления, или параллелизмом. ^[9]

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

Сравнение

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

Семантика с большим шагом имеет то преимущество, что она часто проще (требует меньше правил вывода) и часто напрямую соответствует эффективной реализации интерпретатора для языка (поэтому Кан называет их «естественными»). Оба варианта могут привести к более простым доказательствам, например, при доказательстве сохранения корректности при некотором преобразовании программы . ^[10]

Основным недостатком семантики большого шага является то, что нетерминированные ( расходящиеся ) вычисления не имеют дерева вывода, что делает невозможным установление и доказательство свойств таких вычислений. ^[10]

Семантика малых шагов дает больше контроля над деталями и порядком оценки. В случае инструментированной операционной семантики это позволяет операционной семантике отслеживать, а семантику устанавливать и доказывать более точные теоремы о поведении языка во время выполнения. Эти свойства делают семантику малых шагов более удобной при доказательстве надежности типа системы типов против операционной семантики. ^[10]

Смотрите также

Ссылки

^ Маккарти, Джон . "Рекурсивные функции символических выражений и их вычисление машиной, часть I". Архивировано из оригинала 2013-10-04 . Получено 2006-10-13 .
^ ab Felleisen, M.; Hieb, R. (1992). «Пересмотренный отчет о синтаксических теориях последовательного управления и состояния». Теоретическая информатика . 103 (2): 235–271. doi :10.1016/0304-3975(92)90014-7.
^ Плоткин, Гордон (1975). «Вызов по имени, вызов по значению и λ-исчисление» (PDF) . Теоретическая информатика . 1 (2): 125–159. doi : 10.1016/0304-3975(75)90017-1 . Получено 22 июля 2021 г. .
^ Felleisen, Matthias (1987). Исчисления преобразования Lambda-v-CS: синтаксическая теория управления и состояния в императивных языках программирования высшего порядка (PDF) (PhD). Университет Индианы . Получено 22 июля 2021 г.
^ Феллейзен, Маттиас; Фридман, Дэниел П. (1987). «Семантика редукции для императивных языков высшего порядка». Труды Параллельные архитектуры и языки Европы . Международная конференция по параллельным архитектурам и языкам Европы. Том 1. Springer-Verlag. С. 206–223. doi :10.1007/3-540-17945-3_12.
^ Абади, М.; Карделли, Л. (8 сентября 2012 г.). Теория объектов. ISBN 9781441985989.
^ Феллейзен, Маттиас; Финдлер, Роберт Брюс; Флэтт, Мэтью (2009). Семантическая инженерия с PLT Redex. MIT Press. ISBN 978-0-262-06275-6.
^ Университет Иллинойса CS422
^ Нипков, Тобиас; Кляйн, Гервин (2014). Конкретная семантика (PDF) . стр. 101–102. дои : 10.1007/978-3-319-10542-0 . Проверено 13 марта 2024 г.
^ abc Ксавье Лерой . «Коиндуктивная крупношаговая операционная семантика».

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

Жиль Кан . «Естественная семантика». Труды 4-го ежегодного симпозиума по теоретическим аспектам компьютерной науки . Springer-Verlag. Лондон. 1987.
Гордон Д. Плоткин. Структурный подход к операционной семантике. (1981) Технический представитель DAIMI FN-19, Кафедра компьютерных наук, Орхусский университет, Орхус, Дания. (Перепечатано с исправлениями в J. Log. Algebr. Program. 60-61: 17-139 (2004), препринт).
Гордон Д. Плоткин. Истоки структурной операционной семантики. J. Log. Algebr. Program. 60-61:3-15, 2004. (препринт).
Дэна С. Скотт. Очерк математической теории вычислений, Исследовательская группа программирования, Техническая монография PRG–2, Оксфордский университет, 1970.
Адриан ван Вейнгаарден и др. Пересмотренный отчет об алгоритмическом языке АЛГОЛ 68 . ИФИП. 1968. ([2] ^{[ постоянная неработающая ссылка ]} )
Мэтью Хеннесси . Семантика языков программирования. Wiley, 1990. доступно онлайн.

Внешние ссылки

Медиа, связанные с Операционная семантика на Wikimedia Commons