When transforming terms from one language to another, the intuitively desired property is the preservation of semantics (as used e.g. here for a CPS transformatation):
$$ s \Downarrow v \implies c(s) \Downarrow c(v) $$
I am a little troubled, however, by reconciling this with the classical terms correctness (or soundness) and completeness of logic systems. Usually, I would consider the above statement the completeness property of $c$ (and the converse the definition of correctness).
Intuitively, however, a compiler should be correct rather than complete (as e.g. type-checking often rules out correct programs). The converse of the statement above is only true if $c$ is injective: If the source language contains for instance booleans and operations on them and the compilation replaces them via Church-encoding, the target language can evaluate boolean operations on terms compiled from boolean literals and lambda-abstractions, which the source language cannot evaluate.
- Am I right to assume, that the above statement is the completeness property of $c$ (so the intuitive requirement actually has a counter-intuitive name)?
- Am I also right in my conclusion that a non-injective compiler then is usually not correct?