Semantics encoding

soundness

For every n-ary operator ${\displaystyle op_{A}}$ of A, there exists an n-ary operator ${\displaystyle op_{B}}$ of B such that

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

completeness

For every n-ary operator ${\displaystyle op_{A}}$ of A, there exists an n-ary operator ${\displaystyle op_{B}}$ of B such that

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

(Note: as far as the author is aware of, this criterion of completeness is never used.)

Preservation of compositions is useful insofar as it guarantees that components can be examined either separately or together without "breaking" any interesting property. In particular, in the case of compilations, this soundness guarantees the possibility of proceeding with separate compilation of components, while completeness guarantees the possibility of de-compilation.

This assumes the existence of a notion of reduction on both language A and language B. Typically, in the case of a programming language, reduction is the relation which models the execution of a program.

We write ${\displaystyle \longrightarrow }$ for one step of reduction and ${\displaystyle \longrightarrow ^{*}}$ for any number of steps of reduction.

soundness

For every terms ${\displaystyle T_{A}^{1},T_{A}^{2}}$ of language A, if ${\displaystyle T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}}$ then ${\displaystyle [T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]}$.

completeness

For every term ${\displaystyle T_{A}^{1}}$ of language A and every terms ${\displaystyle T_{B}^{2}}$ of language B, if ${\displaystyle [T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}}$ then there exists some ${\displaystyle T_{A}^{2}}$ such that ${\displaystyle T_{B}^{2}=[T_{A}^{2}]}$.

This preservation guarantees that both languages behave the same way. Soundness guarantees that all possible behaviours are preserved while completeness guarantees that no behaviour is added by the encoding. In particular, in the case of compilation of a programming language, soundness and completeness together mean that the compiled program behaves accordingly to the high-level semantics of the programming language.

This also assumes the existence of a notion of reduction on both language A and language B.

soundness

for any term ${\displaystyle T_{A}}$, if all reductions of ${\displaystyle T_{A}}$ converge, then all reductions of ${\displaystyle [T_{A}]}$ converge.

completeness

for any term ${\displaystyle [T_{A}]}$, if all reductions of ${\displaystyle [T_{A}]}$ converge, then all reductions of ${\displaystyle T_{A}}$ converge.

In the case of compilation of a programming language, soundness guarantees that the compilation does not introduce non-termination such as endless loops or endless recursions. The completeness property is useful when language B is used to study or test a program written in language A, possibly by extracting key parts of the code: if this study or test proves that the program terminates in B, then it also terminates in A.

This assumes the existence of a notion of observation on both language A and language B. In programming languages, typical observables are results of inputs and outputs, by opposition to pure computation. In a description language such as HTML, a typical observable is the result of page rendering.

soundness

for every observable ${\displaystyle obs_{A}}$ on terms of A, there exists an observable ${\displaystyle obs_{B}}$ of terms of B such that for any term ${\displaystyle T_{A}}$ with observable ${\displaystyle obs_{A}}$, ${\displaystyle [T_{A}]}$ has observable ${\displaystyle obs_{B}}$.

completeness

for every observable ${\displaystyle obs_{A}}$ on terms of A, there exists an observable ${\displaystyle obs_{B}}$ on terms of B such that for any term ${\displaystyle [T_{A}]}$ with observable ${\displaystyle obs_{B}}$, ${\displaystyle T_{A}}$ has observable ${\displaystyle obs_{A}}$.

This assumes the existence of notion of simulation on both language A and language B. In a programming languages, a program simulates another if it can perform all the same (observable) tasks and possibly some others. Simulations are used typically to describe compile-time optimizations.

soundness

for every terms ${\displaystyle T_{A}^{1},T_{A}^{2}}$, if ${\displaystyle T_{A}^{2}}$ simulates ${\displaystyle T_{A}^{1}}$ then ${\displaystyle [T_{A}^{2}]}$ simulates ${\displaystyle [T_{A}^{1}]}$.

completeness

for every terms ${\displaystyle T_{A}^{1},T_{A}^{2}}$, if ${\displaystyle [T_{A}^{2}]}$ simulates ${\displaystyle [T_{A}^{1}]}$ then ${\displaystyle T_{A}^{2}}$ simulates ${\displaystyle T_{A}^{1}}$.

Preservation of simulations is a much stronger property than preservation of observations, which it entails. In turn, it is weaker than a property of preservation of bisimulations. As in previous cases, soundness is important for compilation, while completeness is useful for testing or proving properties.

This assumes the existence of a notion of equivalence on both language A and language B. Typically, this can be a notion of equality of structured data or a notion of syntactically different yet semantically identical programs, such as structural congruence or structural equivalence.

soundness

if two terms ${\displaystyle T_{A}^{1}}$ and ${\displaystyle T_{A}^{2}}$ are equivalent in A, then ${\displaystyle [T_{A}^{1}]}$ and ${\displaystyle [T_{A}^{2}]}$ are equivalent in B.

completeness

if two terms ${\displaystyle [T_{A}^{1}]}$ and ${\displaystyle [T_{A}^{2}]}$ are equivalent in B, then ${\displaystyle T_{A}^{1}}$ and ${\displaystyle T_{A}^{2}}$ are equivalent in A.

This assumes the existence of a notion of distribution on both language A and language B. Typically, for compilation of distributed programs written in Acute, JoCaml or E, this means distribution of processes and data among several computers or CPUs.

soundness

if a term ${\displaystyle T_{A}}$ is the composition of two agents ${\displaystyle T_{A}^{1}~|~T_{A}^{2}}$ then ${\displaystyle [T_{A}]}$ must be the composition of two agents ${\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}$.

completeness

if a term ${\displaystyle [T_{A}]}$ is the composition of two agents ${\displaystyle T_{B}^{1}~|~T_{B}^{2}}$ then ${\displaystyle T_{B}}$ must be the composition of two agents ${\displaystyle T_{A}^{1}~|~T_{A}^{2}}$ such that ${\displaystyle [T_{A}^{1}]=T_{B}^{1}}$ and ${\displaystyle [T_{A}^{2}]=T_{B}^{2}}$.