or structural equivalence. soundness if two terms and are equivalent in A, then and are equivalent in B. completeness if two terms and are equivalent in B, then and 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, JoCaml or E, this means distribution of processes and data among several computers or CPUs. soundness if a term is the composition of two agents then must be the composition of two agents . completeness if a term is the composition of two agents then must be the composition of two agents such that and . See also Bisimulation Compiler Semantics Semantic dictionary encoding (SDE) External links The Program Transformation Wiki Formal languages