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. Properties An 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 is expected to preserve a number of properties. Preservation of compositions soundness For every n-ary operator of A, there exists an n-ary operator of B such that completeness For every n-ary operator of A, there exists an n-ary operator of B such that (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. Preservation of reductions 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 for one step of reduction and for any number of steps of reduction. soundness For every terms of language A, if then . completeness For every term of language A and every terms of language B, if then there exists some such that . 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