Content deleted Content added
criterium --> criterion, etc. using AWB |
No edit summary |
||
| (12 intermediate revisions by 12 users not shown) | |||
Line 1:
{{refimprove|date=July 2025}}
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 [[
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 Computer]]'s [[WorldScript]] also involve encoding of a programming language into another.
==
▲If there is a 'satisfactory' encoding of A into B, B is considered 'at least as powerful' (or 'at least as expressive') as A.
▲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 70 ⟶ 65:
=== 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>[
; 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>.
Line 79 ⟶ 74:
* [[Compiler]]
* [[Semantics]]
* [[Semantic dictionary encoding]] (SDE)
==References==
{{reflist}}
==External links==
* [http://
[[Category:Formal languages]]
| |||