セマンティクスエンコーディング

セマンティクスエンコーディングは、形式言語間の変換です。プログラマーにとって、最も馴染みのあるエンコーディング形式は、プログラミング言語をマシン コードまたはバイト コードにコンパイルすることです。ドキュメント形式間の変換もエンコーディングの形式です。TeX または LaTeX ドキュメントを PostScript にコンパイルすることも、よく見られるエンコーディング プロセスです。OCamlのCamlp4などの一部の高レベル プリプロセッサも、プログラミング言語を別のプログラミング言語にエンコーディングします。

正式には、言語 A を言語 B にエンコードすることは、言語 A のすべての項を言語 B にマッピングすることです。言語 Aを言語 B に適切にエンコードできる場合、言語 B は言語 A と同等以上の力がある(または同等以上の表現力がある) と みなされます。

翻訳の非公式な概念は、A のすべての要素を B の同じ要素にマッピングするなどの単純なエンコードを許可するため、言語の表現力を決定するのに十分ではありません。したがって、「十分に良い」エンコードの定義を決定する必要があります。この概念はアプリケーションによって異なります。

一般的に、エンコーディングではいくつかのプロパティが保持されることが期待されます。 ${\displaystyle [\cdot ]:A\longrightarrow B}$

健全性

Aのn項演算子のすべてに対して、 Bのn項演算子が存在し、${\displaystyle op_{A}}$${\displaystyle op_{B}}$

${\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}])}$

完全

Aのn項演算子のすべてに対して、 Bのn項演算子が存在し、${\displaystyle op_{A}}$${\displaystyle op_{B}}$

${\displaystyle \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 の両方にリダクションの概念が存在することを前提としています。通常、プログラミング言語の場合、リダクションはプログラムの実行をモデル化する関係です。

1 ステップの削減と、任意の数の削減ステップについて 記述します。${\displaystyle \longrightarrow }$${\displaystyle \longrightarrow ^{*}}$

健全性

言語 A のすべての項について、の場合には。${\displaystyle T_{A}^{1},T_{A}^{2}}$${\displaystyle T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}}$${\displaystyle [T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]}$

完全

言語 A のすべての項と言語 B のすべての項に対して、となるものが存在します。${\displaystyle T_{A}^{1}}$${\displaystyle T_{B}^{2}}$${\displaystyle [T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}}$${\displaystyle T_{A}^{2}}$${\displaystyle T_{B}^{2}=[T_{A}^{2}]}$

この保存により、両方の言語が同じように動作することが保証されます。健全性は、すべての可能な動作が保存されることを保証し、完全性は、エンコードによって動作が追加されないことを保証します。特に、プログラミング言語のコンパイルの場合、健全性と完全性が組み合わさると、コンパイルされたプログラムがプログラミング言語の高レベルセマンティクスに従って動作することを意味します。

これは、言語 A と言語 B の両方にリダクションの概念が存在することも前提としています。

健全性

任意の項 について、 のすべての簡約が収束する場合、 のすべての簡約も収束します。${\displaystyle T_{A}}$${\displaystyle T_{A}}$${\displaystyle [T_{A}]}$

完全

任意の項 について、 のすべての簡約が収束する場合、 のすべての簡約も収束します。${\displaystyle [T_{A}]}$${\displaystyle [T_{A}]}$${\displaystyle T_{A}}$

プログラミング言語のコンパイルの場合、健全性は、コンパイルによって無限ループや無限再帰などの非終了が発生しないことを保証します。完全性プロパティは、言語 B を使用して言語 A で記述されたプログラムを調査またはテストする場合に役立ちます。この調査またはテストでプログラムが B で終了することが証明された場合、A でも終了します。

これは、言語 A と言語 B の両方に観測の概念が存在することを前提としています。プログラミング言語では、典型的な観測可能オブジェクトは、純粋な計算とは対照的に、入力と出力の結果です。HTMLなどの記述言語では、典型的な観測可能オブジェクトは、ページ レンダリングの結果です。

健全性

A の項のあらゆる観測可能量に対して、B の項の観測可能量が存在し、観測可能量 を持つ任意の項に対して、観測可能量 を持つことになります。${\displaystyle obs_{A}}$${\displaystyle obs_{B}}$${\displaystyle T_{A}}$${\displaystyle obs_{A}}$${\displaystyle [T_{A}]}$${\displaystyle obs_{B}}$

完全

A の項に関するすべての観測可能量に対して、B の項に関する観測可能量が存在し、観測可能量 を持つ任意の項に対して、観測可能量 が存在します。${\displaystyle obs_{A}}$${\displaystyle obs_{B}}$${\displaystyle [T_{A}]}$${\displaystyle obs_{B}}$${\displaystyle T_{A}}$${\displaystyle obs_{A}}$

これは、言語 A と言語 B の両方にシミュレーションの概念が存在することを前提としています。プログラミング言語では、プログラムは、同じ (観測可能な) タスクをすべて実行でき、場合によっては他のタスクも実行できる場合、別のプログラムをシミュレートします。シミュレーションは通常、コンパイル時の最適化を説明するために使用されます。

健全性

すべての項 について、をシミュレートする場合はをシミュレートします。${\displaystyle T_{A}^{1},T_{A}^{2}}$${\displaystyle T_{A}^{2}}$${\displaystyle T_{A}^{1}}$${\displaystyle [T_{A}^{2}]}$${\displaystyle [T_{A}^{1}]}$

完全

すべての項 について、をシミュレートする場合はをシミュレートします。${\displaystyle T_{A}^{1},T_{A}^{2}}$${\displaystyle [T_{A}^{2}]}$${\displaystyle [T_{A}^{1}]}$${\displaystyle T_{A}^{2}}$${\displaystyle T_{A}^{1}}$

シミュレーションの保存は、それが伴う観測の保存よりもはるかに強い特性です。逆に、双シミュレーションの保存の特性よりも弱いです。以前の場合と同様に、健全性はコンパイルにとって重要であり、完全性は特性のテストや証明に役立ちます。

これは、言語 A と言語 B の両方に同等性の概念が存在することを前提としています。通常、これは構造化データの同等性の概念、または構造的合同性や構造的同等性など、構文的には異なるが意味的には同一のプログラムの概念になります。

健全性

2 つの項と がA で同等である場合、 とはB で同等です。${\displaystyle T_{A}^{1}}$${\displaystyle T_{A}^{2}}$${\displaystyle [T_{A}^{1}]}$${\displaystyle [T_{A}^{2}]}$

完全

2 つの項と がB で同等である場合、と はA で同等です。${\displaystyle [T_{A}^{1}]}$${\displaystyle [T_{A}^{2}]}$${\displaystyle T_{A}^{1}}$${\displaystyle T_{A}^{2}}$

これは、言語 A と言語 B の両方に分散の概念が存在することを前提としています。通常、Acute、JoCaml、または E で記述された分散プログラムのコンパイルの場合、これはプロセスとデータを複数のコンピューターまたは CPU に分散することを意味します。

健全性

項が2 つのエージェントの合成である場合、項は2 つのエージェントの合成である必要があります。${\displaystyle T_{A}}$${\displaystyle T_{A}^{1}~|~T_{A}^{2}}$${\displaystyle [T_{A}]}$${\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}$

完全

項が2 つのエージェントの合成である場合、 はおよびとなる2 つのエージェントの合成でなければなりません。${\displaystyle [T_{A}]}$${\displaystyle T_{B}^{1}~|~T_{B}^{2}}$${\displaystyle T_{B}}$${\displaystyle T_{A}^{1}~|~T_{A}^{2}}$${\displaystyle [T_{A}^{1}]=T_{B}^{1}}$${\displaystyle [T_{A}^{2}]=T_{B}^{2}}$

• バイシミュレーション
• コンパイラ
• セマンティクス
• セマンティック辞書エンコーディング(SDE)

• プログラム変換 Wiki