Semantics encoding: Difference between revisions

Revision as of 12:45, 25 February 2006

Revision as of 01:33, 13 May 2007

Line 22:

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

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

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

Line 84 ⟶ 82:

==External links==

* [http://catamaran.labs.cs.uu.nl/twiki/pt/bin/view/Transform/WebChanges|The Program Transformation Wiki]

[[Category:Formal languages]]