Content deleted Content added
Yoric~enwiki (talk | contribs) No edit summary |
Yoric~enwiki (talk | contribs) No edit summary |
||
Line 1:
== Introduction ==
An [[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 [[Objective Caml]]'s Camlp4 or [[Apple]]'s [[WorldScript]] also involve encoding of a programming language into another.
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 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.
This notion varies with the application. Commonly, an encoding <math>[\cdot]: A \longrightarrow B</math> can be judged on the following properties:▼
; preservation of compositions : for every n-ary operator <math>op_A</math> of A, there is an n-ary operator <math>op_B</math> of B such that▼
▲
=== Preservation of compositions ===
▲;
:<math>\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])</math>
;
:<math>\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)]</math>
; preservation of observations (completeness) : assuming the existence of a notion of observation, for every observable behaviour <math>obs_A</math> of terms of A, there is a behaviour <math>obs_B</math> of terms of B such that for any term <math>[T_A]</math> with behaviour <math>obs_B</math>, <math>T_A</math> has behaviour <math>obs_A</math>.▼
; 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 <math>T_A^1</math> and <math>T_A^2</math> are equivalent in A, then <math>[T_A^1]</math> and <math>[T_A^2]</math> are equivalent in B.▼
(Note: as far as the author is aware of, this criterium of completeness is never used.)
; 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 <math>[T_A^1]</math> and <math>[T_A^2]</math> are equivalent in B, then <math>T_A^1</math> and <math>T_A^2</math> are equivalent in A.▼
; preservation of termination (soundness) : assuming a notion of reduction/rewriting, for any term <math>T_A</math>, if all reductions of <math>T_A</math> converge, then all reductions of <math>[T_A]</math> converge.▼
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.
; preservatio of termination (completeness) : assuming a notion of reduction/rewriting, for any term <math>[T_A]</math>, if all reductions of <math>[T_A]</math> converge, then all reductions of <math>T_A</math> converge.▼
=== 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 <math>\longrightarrow</math> for one step of reduction and <math>\longrightarrow^*</math> for any number of steps of reduction.
; soundness : For every terms <math>T_A^1, T_A^2</math> of language A, if <math>T_A^1 \longrightarrow^* T_A^2</math> then <math>[T_A^1] \longrightarrow^* [T_A^2]</math>.
; completeness : For every term <math>T_A^1</math> of language A and every terms <math>T_B^2</math> of language B, if <math>[T_A^1] \longrightarrow^* T_B^2</math> then there exists some <math>T_A^2</math> such that <math>T_B^2 = [T_A^2]</math>.
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.
=== Preservation of termination ===
This also assumes the existence of a notion of reduction on both language A and language B.
▲;
▲;
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.
=== Preservation of observations ===
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 languages such as [[HTML]], a typical observable is the result of page rendering.
; soundness : for every observable <math>obs_A</math> on terms of A, there is an observable <math>obs_B</math> of terms of B such that for any term <math>T_A</math> with observable <math>obs_A</math>, <math>[T_A]</math> has observable <math>obs_B</math>.
▲;
=== Preservation of simulations ===
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 <math>T_A^1, T_A^2</math>, if <math>T_A^2</math> simulates <math>T_A^1</math> then <math>[T_A^2]</math> simulates <math>[T_A^1]</math>.
; completeness : for every terms <math>T_A^1, T_A^2</math>, if <math>[T_A^2]</math> simulates <math>[T_A^1]</math> then <math>T_A^2</math> simulates <math>T_A^1</math>.
Preservation of simulations is a much stronger property than preservation 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.
=== Preservation of equivalences ===
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.
▲;
▲;
=== Preservation of distribution ===
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.
;
; completeness : if a term <math>[T_A]</math> is the composition of two agents <math>T_B^1~|~T_B^2</math> then <math>T_B</math> must be the composition of two agents <math>T_A^1~|~T_A^2</math> such that <math>[T_A^1]=T_B^1</math> and <math>[T_A^2]=T_B^2</math>.
▲; preservation of distribution : if a term <math>T_A</math> is the composition of two agents <math>T_A^1~|~T_A^2</math> then <math>[T_B]</math> must be
== See also ==
* [[Compilation]]
[[Category:Computer science]]
| |||