Введение

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

Свойства

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

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

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

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

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

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

Сохранение замечаний

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

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

Это предполагает существование понятия симуляции как на языке А, так и на языке В. В языках программирования, программа симулирует другую, если она может выполнять все те же (наблюдаемые) задачи и, возможно, некоторые другие. Симуляции обычно используются для описания оптимизаций времени компиляции. Корректность: для каждого термина, если *A* симулирует *B*, то *B* симулирует *A*. Полнота: для каждого термина, если *B* симулирует *A*, то *A* симулирует *B*. Сохранение симуляций – гораздо более сильное свойство, чем сохранение наблюдений, которое оно подразумевает. В свою очередь, оно слабее свойства сохранения бисимуляций. Как и в предыдущих случаях, корректность важна для компиляции, а полнота полезна для тестирования или доказательства свойств.

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

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

Сохранение распределения

Это предполагает существование понятия распределения как для языка А, так и для языка В. Обычно, при компиляции распределённых программ, написанных на Acute, JoCaml или E, это означает распределение процессов и данных между несколькими компьютерами или процессорами. Звукость: если терм является композицией двух агентов , то должен быть композицией двух агентов . Полнота: если терм является композицией двух агентов , то должен быть композицией двух агентов , таких, что и .