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 $[\cdot ]:A\longrightarrow B$ can be judged on the following properties:

preservation of compositions: for every n-ary operator $op_{A}$ of A, there is an n-ary operator $op_{B}$ of B such that; $\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 $obs_{A}$ of terms of A, there is a behaviour $obs_{B}$ of terms of B such that for any term $T_{A}$ with behaviour $obs_{A}$ , $[T_{A}]$ has behaviour $obs_{B}$ .
preservation of observations (completeness): assuming the existence of a notion of observation, for every observable behaviour $obs_{A}$ of terms of A, there is a behaviour $obs_{B}$ of terms of B such that for any term $[T_{A}]$ with behaviour $obs_{B}$ , $T_{A}$ has behaviour $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 $T_{A}^{1}$ and $T_{A}^{2}$ are equivalent in A, then $[T_{A}^{1}]$ and $[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 $[T_{A}^{1}]$ and $[T_{A}^{2}]$ are equivalent in B, then $T_{A}^{1}$ and $T_{A}^{2}$ are equivalent in A.
preservation of termination (soundness): assuming a notion of reduction/rewriting, for any term $T_{A}$ , if all reductions of $T_{A}$ converge, then all reductions of $[T_{A}]$ converge.
preservatio of termination (completeness): assuming a notion of reduction/rewriting, for any term $[T_{A}]$ , if all reductions of $[T_{A}]$ converge, then all reductions of $T_{A}$ converge.