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.

  1. 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)?
  2. 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.

  • $\begingroup$ Are you sure about the one-step derivation $S \rightarrow_1 S^\prime$ I just digged up the paper, and after a short glance, they seem to use the multistep derivation. This also makes the soundness confusing: Why needs there to be exactly one Step from S to S' in that property? $\endgroup$ – choeger Oct 21 '16 at 6:08
  • $\begingroup$ No, there should indeed be a reduction sequence in the definition of soundness. The intended interpretation is that the encoding $[ \! [ S ] \! ]$ can faithfully simulate the original statement $S$; whenever $[ \! [ S ] \! ]$ performs a reduction sequence, it can completed in such a way that the results corresponds to a simulation of a reduction sequence made by $S$. I have updated my answer. $\endgroup$ – Hans Hüttel Oct 21 '16 at 13:06

Intuitively speaking, the correctness property for a transformation over a language on which a notion of evaluation is defined states that if a term has a certain semantics then the image of the term by that transformation evaluates to the image of said semantics. In other words, a correct compiler is one that transforms a program into another program with the same behavior (expressed in the target language).

Here, I infer from your notations that the source language is a language of terms $s$ with a notion of evaluation $\Downarrow$: $s \Downarrow v$ means that $s$ reduces (in any number of steps) to the value $v$. A correct compiler $c$ is one that transforms any program $s$ into a compiled program $c(s)$ which evaluates to the corresponding compiler value $c(v)$.

This corresponds to the definition on Wikipedia if values compile to themselves: if $s$ has the property $\Downarrow v$ then so does $c(s)$.

A sound compiler does not need to be injective: it's possible, and extremely common, for different source programs with the same semantics to be compiled to the same compiled program.

Compilers are generally not complete: as you note, it is common to have terms in the compiled language that cannot be the output of the compiler, i.e. the compiler isn't surjective.

  • $\begingroup$ So you are saying the exact opposte of Hans' answer? That's interesting. Your interpretation of my notation is correct, but to make things explicit: You consider the statement that of correctness (and thus the converse would be completeness)? $\endgroup$ – choeger Oct 21 '16 at 6:11
  • $\begingroup$ @choeger Strictly speaking, I would define correctness as “for all $s$ and $v$, if $c(s)$ exists and $s \Downarrow v$ then $c(v)$ exists and $s \Downarrow c(v)$”. Given that the source language is the one that defines the semantics, I don't see a way to quantify $s \Downarrow v \implies c(s) \Downarrow c(v)$ to make it a completeness property. $\endgroup$ – Gilles 'SO- stop being evil' Oct 21 '16 at 19:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.