Semantics encoding: Difference between revisions

Revision as of 00:13, 18 May 2005

Latest revision as of 17:32, 19 July 2025

(19 intermediate revisions by 19 users not shown)

Line 1:

{{refimprove|date=July 2025}}

A '''semantics encoding''' is a "translation" between [[formal language]]s.

A '''semantics encoding''' is a translation between [[formal language]]s.<ref>{{Citation |last=van Glabbeek |first=Rob |title=A Theory of Encodings and Expressiveness (Extended Abstract) |date=2018 |work=Lecture Notes in Computer Science |pages=183–202 |url=https://doi.org/10.1007/978-3-319-89366-2_10 |access-date=2025-07-19 |place=Cham |publisher=Springer International Publishing |isbn=978-3-319-89365-5}}</ref> For programmers, the most familiar form of encoding is the compilation of a programming language into [[machine code]] or [[Bytecode|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 CamlOCaml]]'s Camlp4 or [[Apple]]'s [[WorldScriptCamlp4]], 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.

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.

== DefinitionProperties ==

ThisAn 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.

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 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 <math>[\cdot]: A \longrightarrow B</math> is expected to preserve a number of properties.

Line 22 ⟶ 17:

:<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>

(Note: as far as the author is aware of, this criteriumcriterion 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.

Line 60 ⟶ 55:

; 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 [[bisimulation|bisimulations]]s. As in previous cases, soundness is important for compilation, while completeness is useful for testing or proving properties.

=== Preservation of equivalences ===

Line 68 ⟶ 63:

; soundness : 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.

; completeness : 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 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 (programming language)|Acute]], [[JoCaml]] or E, this means distribution of processes and data among several computers or CPUs.

; soundness : if a term <math>T_A</math> is the composition of two agents <math>T_A^1~|~T_A^2</math> then <math>[T_BT_A]</math> must be the composition of two agents <math>[T_A^1]~|~[T_A^2]</math>.

; 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>.

== See also ==

* [[Compilation]]

* [[Bisimulation]]

* [[Compiler]]

* [[Semantics]]

* [[Semantic dictionary encoding]] (SDE)

==References==

{{reflist}}

==External links==

* [http://catamaranwww.labsprogram-transformation.cs.uu.nl/twiki/pt/bin/view/Transformorg/WebChanges| The Program Transformation Wiki]

[[Category:ComputerFormal sciencelanguages]]

[[Category:Computer science]]