Кодирование семантики

Семантическое кодирование — это перевод между формальными языками . Для программистов наиболее знакомой формой кодирования является компиляция языка программирования в машинный код или байт-код. Преобразование между форматами документов также является формой кодирования. Компиляция документов TeX или LaTeX в PostScript также является часто встречающимся процессом кодирования. Некоторые препроцессоры высокого уровня, такие как , OCaml Camlp4 также включают кодирование одного языка программирования в другой.

Формально кодирование языка A в язык B — это отображение всех терминов A в B. Если существует удовлетворительное кодирование A в B, B считается, по крайней мере, таким же мощным (или, по крайней мере, столь же выразительным ), как и A.

Характеристики

Неформального понятия перевода недостаточно, чтобы помочь определить выразительность языков, поскольку оно допускает тривиальные кодировки, такие как отображение всех элементов A на один и тот же элемент B. Следовательно, необходимо определить определение «достаточно хорошего» кодирования. . Это понятие варьируется в зависимости от приложения.

Обычно кодировка $[\cdot ]:A\longrightarrow B$ Ожидается, что он сохранит ряд свойств.

Сохранение композиций

надежность

Для каждого n-арного оператора $op_{A}$ оператора A существует n-арный оператор $op_{B}$ из B такой, что

$\forall T_{A}^{1},T_{A}^{2},\dots ,T_{A}^{n},[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})]=op_{B}([T_{A}^{1}],[T_{A}^{2}],\cdots ,[T_{A}^{n}])$

полнота

Для каждого n-арного оператора $op_{A}$ оператора A существует n-арный оператор $op_{B}$ из B такой, что

$\forall T_{B}^{1},T_{B}^{2},\dots ,T_{B}^{n},\exists T_{A}^{1},\dots ,T_{A}^{n},op_{B}(T_{B}^{1},\cdots ,T_{B}^{N})=[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})]$

(Примечание: насколько известно автору, этот критерий полноты никогда не используется.)

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

Сохранение сокращений

Это предполагает существование понятия редукции как в языке A, так и в языке B. Обычно в случае языка программирования редукция — это отношение, которое моделирует выполнение программы.

Мы пишем $\longrightarrow$ за одну ступень снижения и $\longrightarrow ^{*}$ для любого числа шагов приведения.

надежность

Для каждого условия $T_{A}^{1},T_{A}^{2}$ языка А, если $T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}$ затем $[T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]$.

полнота

За каждый срок $T_{A}^{1}$ языка А и всех терминов $T_{B}^{2}$ языка B, если $[T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}$ тогда существует некоторый $T_{A}^{2}$ такой, что $T_{B}^{2}=[T_{A}^{2}]$.

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

Сохранение прекращения

Это также предполагает существование понятия редукции как в языке A, так и в языке B.

надежность

на любой срок $T_{A}$, если все сокращения $T_{A}$ сходятся, то все редукции $[T_{A}]$ сходиться.

полнота

на любой срок $[T_{A}]$, если все сокращения $[T_{A}]$ сходятся, то все редукции $T_{A}$ сходиться.

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

Сохранение наблюдений

Это предполагает существование понятия наблюдения как на языке A, так и на языке B. В языках программирования типичными наблюдаемыми являются результаты ввода и вывода, в отличие от чистых вычислений. В языке описания, таком как HTML , типичная наблюдаемая величина является результатом рендеринга страницы.

надежность

для каждого наблюдаемого $obs_{A}$ в терминах A существует наблюдаемая $obs_{B}$ таких членов B, что для любого термина $T_{A}$ с наблюдаемым $obs_{A}$, $[T_{A}]$ имеет наблюдаемый $obs_{B}$.

полнота

для каждого наблюдаемого $obs_{A}$ в терминах A существует наблюдаемая $obs_{B}$ на условиях B так, что для любого члена $[T_{A}]$ с наблюдаемым $obs_{B}$, $T_{A}$ имеет наблюдаемый $obs_{A}$.

Сохранение симуляций

Это предполагает существование понятия моделирования как на языке A, так и на языке B. На одном языке программирования программа имитирует другой, если она может выполнять все те же (наблюдаемые) задачи и, возможно, некоторые другие. Моделирование обычно используется для описания оптимизации во время компиляции.

надежность

на каждое условие $T_{A}^{1},T_{A}^{2}$, если $T_{A}^{2}$ имитирует $T_{A}^{1}$ затем $[T_{A}^{2}]$ имитирует $[T_{A}^{1}]$.

полнота

на каждое условие $T_{A}^{1},T_{A}^{2}$, если $[T_{A}^{2}]$ имитирует $[T_{A}^{1}]$ затем $T_{A}^{2}$ имитирует $T_{A}^{1}$.

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

Сохранение эквивалентностей

Это предполагает существование понятия эквивалентности как на языке A, так и на языке B. Обычно это может быть понятие равенства структурированных данных или понятие синтаксически разных, но семантически идентичных программ, таких как структурное соответствие или структурная эквивалентность.

надежность

если два срока $T_{A}^{1}$ и $T_{A}^{2}$ эквивалентны в A, то $[T_{A}^{1}]$ и $[T_{A}^{2}]$ эквивалентны в B.

полнота

если два срока $[T_{A}^{1}]$ и $[T_{A}^{2}]$ эквивалентны в B, то $T_{A}^{1}$ и $T_{A}^{2}$ эквивалентны в А.

Сохранение дистрибуции

Это предполагает существование понятия распределения как на языке A, так и на языке B. Обычно для компиляции распределенных программ, написанных на Acute , JoCaml или E, это означает распределение процессов и данных между несколькими компьютерами или процессорами.

надежность

если срок $T_{A}$ представляет собой композицию двух агентов $T_{A}^{1}~|~T_{A}^{2}$ затем $[T_{A}]$ должна состоять из двух агентов $[T_{A}^{1}]~|~[T_{A}^{2}]$.

полнота

если срок $[T_{A}]$ представляет собой композицию двух агентов $T_{B}^{1}~|~T_{B}^{2}$ затем $T_{B}$ должна состоять из двух агентов $T_{A}^{1}~|~T_{A}^{2}$ такой, что $[T_{A}^{1}]=T_{B}^{1}$ и $[T_{A}^{2}]=T_{B}^{2}$.

См. также

• Бисимуляция
• Компилятор
• Семантика
• Кодирование семантического словаря (SDE)

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

• Вики по трансформации программ