Semantics encoding

A semantics encoding is a translation between formal languages. For programmers, the most familiar form of encoding is the compilation of a programming language into machine code or byte-code. Conversion between document formats are also forms of encoding. Compilation of TeX or LaTeX documents to PostScript are also commonly encountered encoding processes. Some high-level preprocessors, such as OCaml's Camlp4, also involve encoding of a programming language into another. Formally, an encoding of a language A into language B is a mapping of all terms of A into B. If there is a satisfactory encoding of A into B, B is considered at least as powerful (or at least as expressive) as A.

A semantics encoding is a translation between formal languages. For programmers, the most familiar form of encoding is the compilation of a programming language into machine code or byte-code. Conversion between document formats are also forms of encoding. Compilation of TeX or LaTeX documents to PostScript are also commonly encountered encoding processes. Some high-level preprocessors, such as OCaml's Camlp4, also involve encoding of a programming language into another. Formally, an encoding of a language A into language B is a mapping of all terms of A into B. If there is a satisfactory encoding of A into B, B is considered at least as powerful (or at least as expressive) as A. \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 op_A of A, there exists an n-ary operator op_B of B such that \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. completeness : For every term T_A^1 of language A and every terms T_B^2 of language B, if [T_A^1] \longrightarrow^* T_B^2 then there exists some T_A^2 such that 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. completeness : if a term [T_A] is the composition of two agents T_B^1~|~T_B^2 then T_B must be the composition of two agents T_A^1~|~T_A^2 such that [T_A^1]=T_B^1 and [T_A^2]=T_B^2 . ==References== ==External links== The Program Transformation Wiki

Text derived from https://en.wikipedia.org/w/index.php?oldid=1365857016 under CC BY-SA 4.0; modifications have been made.