Is Semantic Preservation Soundness (or Correctness) or Completeness

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?

This is really a question about the notion of operational correspondence.

The paper Towards a Unified Approach to Encodability and
Separation Results for Process Calculi by Daniele Gorla (http://wwwusers.di.uniroma1.it/~gorla/papers/G-CONCUR08.pdf) is concerned with correctness criteria for translations between process calculi.

In his work, Gorla introduces a notion of behavioural equivalence; I will leave it out here in order not to complicate the explanation overly.

Let $[ \! [ \; ] \! ]$ be an encoding, let $\rightarrow_1$ be the transition relation defined for the source language and let $\rightarrow_2$ be the transition relation defined for the target language. If we have that

• If $S \rightarrow_1 S'$ then $[ \! [ S ] \! ] \rightarrow^*_2 [ \! [ S' ] \! ]$, we say that the encoding is complete

• If $[ \! [ S ] \! ] \rightarrow^_2 T$, then there exists a $S'$ such that $S \rightarrow^_1 S'$ and $T \rightarrow^*_2 [ \! [ S' ] \! ]$, we say that the encoding is sound.

So yes, the notion mentioned in the questions is indeed that of completeness. The notion of soundness is shaped by the fact that the target language will often be richer than the target language or contain syntactic constructs whose behaviour does not correspond to anything in the source language. This explains why we speak of the intermediate configuration $T$ in the definition instead of requiring injectivity.

StackExchange Computer Science Q#64856, answer score: 3