Semantics encoding

Introduction

An semantics encoding is a "translation" between formal languages -- typically programming languages or description languages.

An encoding of a formal language A in a formal language B is a mapping of all terms of language A into language B. If there is a 'satisfactory' encoding of A in B, B is considered at least as powerful (or at least as 'expressive') as A.

Classifications of encodings

This informal notion of translation is not sufficient to help determine expressivity of languages, as it permits trivial encodings such as mapping all elements of A to the same element of B. Therefore, it is necessary to determine the definition of a "good enough" encoding.

This notion varies with the application. Commonly, an encoding ${\displaystyle [\cdot ]:A\longrightarrow B}$  can be judged on the following properties:

preservation of compositions

for every n-ary operator ${\displaystyle op_{A}}$  of A, there is 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}])}$ 

preservation of observations (soundness)

assuming the existence of a notion of observation, for every observable behaviour ${\displaystyle obs_{A}}$  of terms of A, there is a behaviour ${\displaystyle obs_{B}}$  of terms of B such that for any term ${\displaystyle T_{A}}$  with behaviour ${\displaystyle obs_{A}}$ , ${\displaystyle [T_{A}]}$  has behaviour ${\displaystyle obs_{B}}$ .

preservation of observations (completeness)

assuming the existence of a notion of observation, for every observable behaviour ${\displaystyle obs_{A}}$  of terms of A, there is a behaviour ${\displaystyle obs_{B}}$  of terms of B such that for any term ${\displaystyle [T_{A}]}$  with behaviour ${\displaystyle obs_{B}}$ , ${\displaystyle T_{A}}$  has behaviour ${\displaystyle obs_{A}}$ .

preservation of equivalences (soundness)

assuming the existence of a notion of equivalence on A (typically, equality structural congruence or structural equivalence) and a notion of equivalence on B, 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.

preservation of equivalences (completeness)

assuming the existence of a notion of equivalence on A (typically, equality, structural congruence or structural equivalence) and a notion of equivalence on B, 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.

preservation of termination (soundness)

assuming a notion of reduction/rewriting, for any term ${\displaystyle T_{A}}$ , if all reductions of ${\displaystyle T_{A}}$  converge, then all reductions of ${\displaystyle [T_{A}]}$  converge.

preservatio of termination (completeness)

assuming a notion of reduction/rewriting, for any term ${\displaystyle [T_{A}]}$ , if all reductions of ${\displaystyle [T_{A}]}$  converge, then all reductions of ${\displaystyle T_{A}}$  converge.

Domain-specific properties

Under some circumstances, other properties can be important.

For instance, in process algebras, encodings are often expected to preserve distribution:

preservation of distribution

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

the composition of two agents ${\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}$