Content deleted Content added
Yoric~enwiki (talk | contribs) No edit summary |
Yoric~enwiki (talk | contribs) No edit summary |
||
Line 11:
; 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
:<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>
; preservation of observations (soundness) : 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_A</math>, <math>[T_A]</math> has behaviour <math>obs_B</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.
; 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.
; 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.
| |||