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

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

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

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

История

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

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

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

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

Подходы

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

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

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

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

В качестве простого примера мы рассмотрим часть семантики простого языка программирования; соответствующие иллюстрации даны в Плоткине81 , Хеннесси90 и других учебниках. Позволять $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}$ .

Если у нас также есть логические выражения для состояния, ранжированные по $B$ , то мы можем определить семантику команды while : ${\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 приобрела большую популярность и стала стандартом де-факто при определенииоперационная семантика. В качестве признака успеха первоначальный доклад (так называемый Орхусскийотчет) о 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] контрактные системы , исключения, фьючерсы, вызов по необходимости и многие другие возможности языка. Тщательное современное рассмотрение семантики редукции, в котором подробно обсуждаются несколько таких приложений, представлено Маттиасом Феллейзеном, Робертом Брюсом Финдлером и Мэтью Флаттом из отдела семантической инженерии с PLT Redex . ^[7]

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

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

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

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

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

Сравнение

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

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

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

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

См. также

Ссылки

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

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

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

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

СМИ, связанные с операционной семантикой, на Викискладе?

[1] Маккарти, Джон . «Рекурсивные функции символьных выражений и их машинное вычисление, часть I» . Архивировано из оригинала 4 октября 2013 г. Проверено 13 октября 2006 г.

[felleisen-hieb-92-2] Перейти обратно: ^а ^б Феллейзен, М.; Хиеб, Р. (1992). «Пересмотренный отчет о синтаксических теориях последовательного управления и состояния». Теоретическая информатика . 103 (2): 235–271. дои : 10.1016/0304-3975(92)90014-7 .

[3] Плоткин, Гордон (1975). «Вызов по имени, вызов по значению и λ-исчисление» (PDF) . Теоретическая информатика . 1 (2): 125–159. дои : 10.1016/0304-3975(75)90017-1 . Проверено 22 июля 2021 г.

[4] Феллейзен, Матиас (1987). Исчисления преобразования Lambda-v-CS: синтаксическая теория управления и состояния в императивных языках программирования высшего порядка (PDF) (доктор философии). Университет Индианы . Проверено 22 июля 2021 г.

[5] Феллайзен, Матиас; Фридман, Дэниел П. (1987). «Семантика редукции для императивных языков высшего порядка». Труды параллельных архитектур и языков Европы . Международная конференция по параллельным архитектурам и языкам в Европе. Том. 1. Шпрингер-Верлаг. стр. 206–223. дои : 10.1007/3-540-17945-3_12 .

[6] Абади, М.; Карделли, Л. (8 сентября 2012 г.). Теория объектов . ISBN 9781441985989 .

[7] Феллайзен, Матиас; Финдлер, Роберт Брюс; Флэтт, Мэтью (2009). Семантическая инженерия с помощью PLT Redex . Массачусетский технологический институт Пресс. ISBN 978-0-262-06275-6 .

[8] Университет Иллинойса CS422

[9] Нипков, Тобиас; Кляйн, Гервин (2014). Конкретная семантика (PDF) . стр. 101–102. дои : 10.1007/978-3-319-10542-0 . Проверено 13 марта 2024 г.

[leroy-coinductivebigstep-10] Перейти обратно: ^а ^б ^с Ксавье Лерой . «Коиндуктивная операционная семантика большого шага».

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]