Введение

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

Подходы

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

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

Семантика редукции — это альтернативное представление операционной семантики. Её ключевые идеи были впервые применены к чисто функциональным вариантам подстановки по имени и подстановки по значению в лямбда-исчислении Гордоном Плоткиным в 1975 году и обобщены на функциональные языки высшего порядка с императивными возможностями Маттиасом Феллейзеном в его диссертации 1987 года. Метод был далее разработан Маттиасом Феллейзеном и Робертом Хибом в 1992 году в полноценную эквациональную теорию управления и состояния. Семантика редукции задаётся как набор правил редукции, каждое из которых определяет один потенциальный шаг редукции. Например, следующее правило редукции утверждает, что оператор присваивания может быть сведён, если он находится непосредственно рядом с объявлением своей переменной:

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

где обозначает произвольные выражения, а — полностью сведённые значения. Каждый контекст вычисления включает в себя ровно одну "дыру", в которую термин подставляется захватывающим образом. Форма контекста указывает, где с помощью этой дыры может происходить редукция. Для описания "всплытия" с помощью контекстов вычисления достаточно одной аксиомы:

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

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

Большой шаг структурной операционной семантики также известен под названиями естественная семантика, реляционная семантика и семантика вычислений. Большой шаг операционной семантики был введен Жилем Каном под названием естественная семантика при представлении Mini ML – чистого диалекта ML. Определения большого шага можно рассматривать как определения функций или, в более общем случае, отношений, интерпретирующих каждую конструкцию языка в соответствующей области. Благодаря своей интуитивности, большой шаг является популярным выбором для спецификации семантики языков программирования, однако он имеет некоторые недостатки, которые делают его неудобным или невозможным для использования во многих ситуациях, например, в языках с развитыми средствами управления или поддержкой параллелизма. Семантика большого шага описывает, как конечные результаты вычисления языковых конструкций могут быть получены путем комбинирования результатов вычисления их синтаксических соответствий (подвыражений, подкоманд и т.п.) в стиле "разделяй и властвуй".

Сравнение

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