and completeness together mean that the compiled program behaves accordingly to the high-level semantics of the programming language. Preservation of termination This also assumes the existence of a notion of reduction on both language A and language B. soundness for any term , if all reductions of converge, then all reductions of converge. completeness for any term , if all reductions of converge, then all reductions of converge. In the case of compilation of a programming language, soundness guarantees that the compilation does not introduce non-termination such as endless loops or endless recursions. The completeness property is useful when language B is used to study or test a program written in language A, possibly by extracting key parts of the code: if this study or test proves that the program terminates in B, then it also terminates in A. Preservation of observations This assumes the existence of a notion of observation on both language A and language B. In programming languages, typical observables are results of inputs and outputs, by opposition to pure computation. In a description language such as HTML, a typical observable is the result of page rendering. soundness for every observable on terms of A, there exists an observable of terms of B such that for any term with observable , has observable . completeness for every observable on terms of A, there exists an observable on terms of B such that for any term with observable , has observable . Preservation of simulations This assumes the existence of notion of simulation on both language A and language B. In a programming languages, a program simulates another if it can perform all the same (observable) tasks and possibly some others. Simulations are used typically to describe compile-time optimizations. soundness for every terms , if simulates then simulates . completeness for every terms , if simulates then simulates . 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 bisimulations. As in previous cases, soundness is important for compilation, while completeness is useful for testing or proving properties. Preservation of equivalences This assumes the existence of a notion of equivalence on both language A and language B. Typically, this can be a notion of equality of structured data or a notion of syntactically different yet semantically identical programs, such as structural congruence