Алгебраическая семантика (информатика)

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

Синтаксис

Синтаксис . алгебраической спецификации формулируется в два этапа: (1) определение формальной сигнатуры типов данных и символов операций и (2) интерпретация сигнатуры через множества и функции

Определение подписи

Сигнатура . алгебраической спецификации определяет ее формальный синтаксис Слово «подпись» используется как понятие « ключевая подпись » в нотной записи .

Подпись состоит из набора $S$ типов данных , известных как сортировки , вместе с семейством $\Sigma$ наборов, каждый набор содержит символы операций (или просто символы), которые связывают виды.Мы используем $\Sigma _{s_{1}s_{2}...s_{n},~s}$ для обозначения набора символов операций, относящихся к сортам $s_{1},~s_{2},~...,~s_{n}\in S$ в сорте $s\in S$.

Например, для подписи целочисленных стеков мы определяем два вида, а именно: $int$ и $stack$и следующее семейство символов операций:

${\begin{aligned}\Sigma _{\Lambda ,~stack}&=\{{\rm {new}}\}\\\Sigma _{int~stack,~stack}&=\{{\rm {push}}\}\\\Sigma _{stack,~stack}&=\{{\rm {pop}}\}\\\Sigma _{stack,~int}&=\{{\rm {depth}},{\rm {top}}\}\\\end{aligned}}$

где $\Lambda$ обозначает пустую строку .

Теоретико-множественная интерпретация сигнатуры

Алгебра ​ $A$ интерпретирует символы видов и операций как множества и функции .Каждый сорт $s$ интерпретируется как набор $A_{s}$, который называется носителем $A$ своего рода $s$, и каждый символ $\sigma$ в $\Sigma _{s_{1}s_{2}...s_{n},~s}$ отображается в функцию $\sigma _{A}:A_{s_{1}}\times A_{s_{2}}\times ~...\times ~A_{s_{n}}$ называется операцией , что $A$.

Что касается сигнатуры целочисленных стеков, мы интерпретируем сортировку $int$ как набор $\mathbb {Z}$ целых чисел и интерпретировать сортировку $stack$ как набор $Stack$ целочисленных стеков. Далее мы интерпретируем семейство символов операций как следующие функции:

${\begin{aligned}{\rm {new}}&:~\to Stack\\{\rm {push}}&:~\mathbb {Z} \times Stack\to Stack\\{\rm {pop}}&:~Stack\to Stack\\{\rm {depth}}&:~Stack\to \mathbb {Z} \\{\rm {top}}&:~Stack\to \mathbb {Z} \\\end{aligned}}$

Семантика

Семантика относится к значению или поведению . Алгебраическая спецификация обеспечивает как значение, так и поведение объекта рассматриваемого .

Эквациональные аксиомы

Семантика алгебраической спецификации определяется аксиомами в форме условных уравнений .

Что касается сигнатуры целочисленных стеков, у нас есть следующие аксиомы:

Для любого $z\in \mathbb {Z}$ и $s\in Stack$,

${\begin{aligned}&A1:~~{\rm {pop}}({\rm {push}}(z,s))=s\\&A2:~~{\rm {depth}}({\rm {push}}(z,s))={\rm {depth}}(s)+1\\&A3:~~{\rm {top}}({\rm {push}}(z,s))=z\\&A4:~~{\rm {pop}}({\rm {new}})={\rm {new}}\\&A5:~~{\rm {depth}}({\rm {new}})=0\\&A6:~~{\rm {top}}(s)=-404~{\rm {if~depth}}(s)=0\\\end{aligned}}$

где " $-404$" означает "не найдено".

Математическая семантика

Математическая семантика (также известная как денотатационная семантика ) спецификации относится к ее математическому смыслу.

Математическая семантика алгебраической спецификации — это класс всех алгебр, удовлетворяющих этой спецификации.В частности, классический подход Gogen et al. принимает исходную алгебру ( единственную с точностью до изоморфизма ) как «наиболее представительную» модель алгебраической спецификации.

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

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

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

Рассмотрим аксиомы для целочисленных стеков. Позволять " $\Rrightarrow$" обозначают "перезаписывает в".

${\begin{aligned}&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {pop}}({\rm {new}})))))))&\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))))&({\rm {by~Axiom~}}A4)\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&{\rm {top}}({\rm {push}}(3,~{\rm {new}}))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&3&({\rm {by~Axiom~}}A3)\\\end{aligned}}$

Каноническое свойство

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

При любой канонической алгебраической спецификации математическая семантика согласуется с операционной семантикой.

В результате канонические алгебраические спецификации стали широко применяться для решения проблем корректности программ. Например, многие исследователи применяли такие спецификации для эквивалентности объектов в программировании проверки объектно -ориентированном . Увидеть Чена и Цзе в качестве вторичного источника , дающего исторический обзор выдающихся исследований с 1981 по 2013 год.

См. также

• Алгебраическая семантика (математическая логика)
• OBJ (язык программирования)
• Джозеф Гоген