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

редактировать

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

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

Содержание

1 Свойства
- 1.1 Сохранение композиций
- 1.2 Сохранение сокращений
- 1.3 Сохранение окончаний
- 1.4 Сохранение наблюдений
- 1.5 Сохранение моделирования
- 1.6 Сохранение эквивалентностей
- 1.7 Сохранение распределения
2 См. Также
3 Внешние ссылки

Свойства

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

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

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

звук: Для каждого n-арного оператора $op A {\ displaystyle op_ {A}}$ ${\ displaystyle op_ { A}}$ в A существует n-арный оператор $op B {\ displaystyle op_ {B}}$ ${\ displaystyle op_ {B}}$ of B такой, что; $∀ TA 1, TA 2,…, TA n, [op A (TA 1, TA 2, ⋯, TA n)] = op B ([TA 1], [TA 2], ⋯, [TA n]) {\ displaystyle \ forall T_ {A} ^ {1}, T_ {A} ^ {2 }, \ точек, 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}])}$ ${\ displaystyle \ 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 {\ displaystyle op_ {A}}$ ${\ displaystyle op_ { A}}$ of A существует n-арный оператор $op B {\ displaystyle op_ {B }}$ ${\ displaystyle op_ {B}}$ из B такой, что; $∀ TB 1, TB 2,…, TB n, ∃ TA 1,…, TA n, op B (TB 1, ⋯, TBN) = [op A (TA 1, TA 2, ⋯, TA n)] {\ displaystyle \ forall T_ {B} ^ {1}, T_ {B} ^ {2}, \ dots, T_ {B} ^ {n}, \ существует 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})]}$ ${\ displaystyle \ forall T_ {B} ^ {1}, T_ {B} ^ {2}, \ dots, T_ {B} ^ {n}, \ существует 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. Обычно в случае языка программирования редукция - это отношение, моделирующее выполнение программы.

Мы пишем $⟶ {\ displaystyle \ longrightarrow}$ $\ longrightarrow$ для одного шага сокращения и $⟶ ∗ {\ displaystyle \ longrightarrow ^ {*}}$ ${\ displaystyle \ longrightarrow ^ {*}}$ для любого количества ступеней редукции.

звук: Для каждого термина $TA 1, TA 2 {\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ языка A, если $TA 1 ⟶ ∗ TA 2 {\ displaystyle T_ {A} ^ {1} \ longrightarrow ^ {*} T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1} \ longrightarrow ^ {*} T_ {A} ^ {2}}$ , то $[TA 1] ⟶ ∗ [TA 2] {\ displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} [T_ {A} ^ {2}] }$ .
полнота: Для каждого термин $TA 1 {\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {1}}$ языка A и все термины $TB 2 {\ displaystyle T_ {B} ^ {2}}$ ${ \ displaystyle T_ {B} ^ {2}}$ языка B, если $[TA 1] ⟶ ∗ TB 2 {\ displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} T_ {B} ^ {2}}$ ${\ displaystyle [T_ {A} ^ {1}] \ longrightarrow ^ {*} T_ {B} ^ {2}}$ тогда существует некая $TA 2 {\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ такая, что $TB 2 = [TA 2] {\ displaystyle T_ {B} ^ {2} = [T_ {A} ^ {2}]}$ ${\ displaystyle T_ {B} ^ {2} = [T_ {A} ^ {2}]}$ .

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

Сохранение завершения

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

звук: для любого термина $TA {\ displaystyle T_ {A}}$ $T_ {A}$ , если все сокращения $TA {\ displaystyle T_ {A}}$ $T_ {A}$ сходятся, то все сокращения $[TA] { \ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A}]}$ converge.
полнота: для любого термина $[TA] {\ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A}]}$ , если все сокращения $[TA] {\ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A}]}$ сходятся, то все сокращения $TA {\ displaystyle T_ {A}}$ $T_ {A}$ сходиться.

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

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

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

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

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

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

звук: для каждого члена $TA 1, TA 2 {\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ , если $TA 2 {\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ имитирует $TA 1 {\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {1}}$ , затем $[TA 2] {\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {2}]}$ имитирует $[TA 1] {\ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle [T_ {A} ^ {1}]}$ .
полнота: для каждого термина $TA 1, TA 2 {\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1}, T_ {A} ^ {2}}$ , если $[TA 2] {\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {2}]}$ имитирует $[TA 1] {\ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle [T_ {A} ^ {1}]}$ затем $TA 2 {\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ имитирует $TA 1 {\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {1}}$ .

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

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

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

звук: если два члена $TA 1 {\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {1}}$ и $TA 2 {\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ эквивалентны в A, тогда $[TA 1] {\ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle [T_ {A} ^ {1}]}$ и $[TA 2 ] {\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {2}]}$ эквивалентны в B.
полнота: , если два члена $[TA 1] { \ displaystyle [T_ {A} ^ {1}]}$ ${\ displaystyle [T_ {A} ^ {1}]}$ и $[TA 2] {\ displaystyle [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {2}]}$ эквивалентны в B, затем $TA 1 {\ displaystyle T_ {A} ^ {1}}$ ${\ displaystyle T_ {A} ^ {1}}$ и $TA 2 {\ displaystyle T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {2}}$ эквивалентны в A.

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

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

звук: , если термин $T A {\ displaystyle T_ {A}}$ $T_ {A}$ представляет собой композицию двух агентов $T A 1 | TA 2 {\ displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ , затем $[TA] {\ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A}]}$ должен быть составом двух агентов $[TA 1] | [TA 2] {\ displaystyle [T_ {A} ^ {1}] ~ | ~ [T_ {A} ^ {2}]}$ ${\ displaystyle [T_ {A} ^ {1}] ~ | ~ [T_ {A} ^ {2}]}$ .
полнота: , если термин $[TA] {\ displaystyle [T_ {A}]}$ ${\ displaystyle [T_ {A}]}$ - это композиция из двух агентов $TB 1 | TB 2 {\ displaystyle T_ {B} ^ {1} ~ | ~ T_ {B} ^ {2}}$ ${\ displaystyle T_ {B} ^ {1} ~ | ~ T_ {B} ^ { 2}}$ , затем $TB {\ displaystyle T_ {B}}$ $T_ {B}$ должен быть составом двух агентов $ТА 1 | TA 2 {\ displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ ${\ displaystyle T_ {A} ^ {1} ~ | ~ T_ {A} ^ {2}}$ такой, что $[TA 1] = TB 1 {\ displaystyle [T_ {A } ^ {1}] = T_ {B} ^ {1}}$ ${\ displaystyle [T_ {A} ^ {1}] = T_ {B} ^ {1}}$ и $[TA 2] = TB 2 {\ displaystyle [T_ {A} ^ {2}] = T_ {B } ^ {2}}$ ${\ displaystyle [T_ {A} ^ {2} ] = T_ {B} ^ {2}}$ .

См. Также

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

Wiki по преобразованию программ