Full Completeness vs Full Abstraction of a program translation

Question

Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences.

Instead of providing full abstraction proofs, some recent (categorical based) compiler verification work by Hasegawa [1,2] and Egger et. al. [3] prove the full completeness of various CPS translations.

Question: What is the difference between full completeness and full abstraction?

To me, completeness just looks like equivalence reflection for a translation and fullness appears to be a consequence of equivalence preservation.

Note: Both Curien [7] and Abramsky [8] explore the relationship between definability, full abstraction, and to some extent full completeness. I suspect these resources may have the answer to my question, but after a surface read I have yet to confirm that.

Some Background: The term "full completeness" was coined by Abramsky and Jagadeesan [4] to characterize the correctness of a game-semantic model of Multiplicative Linear Logic.

Blute [5] provides the following definition:

Let $\mathcal{F}$ be a free category. We say that a categorical model $\mathcal{M}$ is fully complete for $\mathcal{F}$ or that we have full completeness of $\mathcal{F}$ with respect to $\mathcal{M}$ if, with respect to some interpretation of the generators, the unique free functor $[\![ - ]\!] : \mathcal{F} \rightarrow \mathcal{M}$ is full.

As far as I can tell, Hasegawa in [6] is the first to adapt full completeness to describe a program translation instead of a categorical semantic model. In this case, the Girard translation from simply typed lambda calculus to the linear lambda calculus. Later, in [1], he defines full completeness of the CPS translation $(\cdot)^\circ$ as:

If $\Gamma^{\circ};\emptyset \vdash N : (\sigma^\circ \rightarrow o) \multimap o$ is derivable in the linear lambda calculus, then there exists $\Gamma \vdash M : \sigma$ in the computational lambda calculus such that $\Gamma^{\circ};\emptyset \vdash M^\circ = N : (\sigma^\circ \rightarrow o) \multimap o$ holds in the linear lambda calculus.

(where $o$ is a base type in the linear lambda calculus (target language), but not in the computational lambda calculus (source language).)

To me, Hasegawa's definition seems like a fullness and should really be combined with completeness to get full completeness.

Egger et. al. [3] define full completeness of a CPS translation $(\cdot)^v$ as a combination of (1) completeness and (2) fullness:

(1): If $\Theta \vdash M,N : \tau$ and $\Theta^v | - \vdash M^v =_{\beta\eta} N^v : !\tau^v$ then $\Theta \vdash M =_{\lambda_c} N : \tau$

(2): If $\Theta^v | - \vdash t : !\tau^v$ then there exists a term $\Theta \vdash M : \tau$ such that $\Theta^v | - \vdash M^v =_{\beta\eta} t : !\tau^v$

(where $=_{\lambda_c}$ is Moggi's computational equational theory)

---

[1] "Linearly Used Effects: Monadic and CPS Transformations into Linear Lambda Calculus", Hasegawa 2002

[2] "Semantics of Linear Continuation-Passing in Call-by-Name", Hasegawa 2004

[3] "Linear-use CPS Translations in the Enriched Effect Calculus", Egger et. al. 2012

[4] "Games and Full Completeness for Multiplicative Linear Logic", Abramsky and Jagadeesan 1992

[5] "Category Theory for Linear Logicians", Blute 2003

[6] "Girard Translation and Logical Predicates", Hasegawa 2000

[7] "Definability and full abstraction", Curien 2007

[8] "Axioms for Definability and Full Completeness", Abramsky 1999

Answer 1

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer.

Full completeness: "Sound and complete" is a property you want for a traditional logic to have with respect to its semantics. Soundness means that whatever you can prove in the logic is true in the semantic model. Completeness means that whatever is true in the semantic model is provable in the logic. We say that a logic is sound and complete for a particular semantic model. When we come to constructive logic, such as Martin-Lof type theory or linear logic, we care not only about whether formulas provable, but also what their proofs are. A provable formula may have many proofs and a constructive logic wants to keep them apart. So, a semantics for a constructive logic involves specifying not only whether a formula is true, but also some abstract semantic notion of "proof" ("evidence") for its truth. Abramsky and colleagues coined the term "full completeness" to mean that the proofs in the logic can express all the semantic proofs in the model. So, "full" refers to proofs here. A "complete" logic can prove everything it needs to. A "fully complete" logic has all the proofs that it needs to have. So "full completeness" means "constructive completeness" or "proof completeness". This has nothing to do with full abstraction.

Full abstraction: "Adequate and fully abstract" is a property you want for the semantic model of a programming language. (Note the first difference: we are now dealing with the properties of the semantic model, not the properties of the language!) Adequacy means that, whenever two terms have the same meaning in the semantic model, they are observationally equivalent in the programming language (with respect to some notion of execution). Full abstraction means that, if two terms are observationally equivalent, they have the same meaning in the semantic model. These ideas can be related to soundness and completeness, but in a somewhat contrived way. If we think of the semantic model of a programming language as a "logic" or a "proof method" to talk about observational equivalence, then adequacy means that this proof method is sound; full abstraction means that this proof method is complete. There is no notion of "full completeness" here because nobody has yet produced a semantic model that represents a constructive proof method. (But, such a thing is theoretically possible, and one of these days somebody might do so.)

In your case, you are interested in translations rather than semantic models. The properties of adequacy and full abstraction can be extended to deal with translations as follows. You think of the target language as your "semantic model", i.e., a formalism that you fully understand somehow. If so, you have some notion of equivalence for it. Then, we say that the translation is adequate if, whenever the translations of two source programs are equivalent in the target language, they are observationally equivalent in the source language. We say that it is fully abstract if, whenever two source programs are observationally equivalent in the source language, their translations are equivalent in the target language.

In reality, I don't know of any target languages that we really fully "understand". All we know is some other notion of observational equivalence for the target language. In that case, the translation is adequate if the observational equivalence of the translations in the target language implies observational equivalence in the source language. $$ \tau(M) \cong \tau(N) \Longrightarrow M \cong N$$ The translation is fully abstract if the observational equivalence of the terms in the source language implies the observational equivalence of the translations in the target language. $$M \cong N \Longrightarrow \tau(M) \cong \tau(N)$$ Some authors take "fully abstract translation" to mean the combination of these two properties: $$M \cong N \iff \tau(M) \cong \tau(N)$$

Egger et al seem to be similarly extending the idea of full completeness to translations. In their set-up, formulas are types and proofs are terms. Their translation translates types as well as terms. They call their translation fully complete if the translation of a type $A$ has only those terms that are obtained by translating the original terms of type $A$. $$\forall N : \tau(A).\; \exists M : A.\, \tau(M) = N$$

Now for the vague connection between full completeness and full abstraction. Proving that a semantic model or a translation is fully abstract often involves some of definability. This is because our languages are generally higher-order. So, if the semantic model or the target language has too many "contexts" then it will be able to poke our terms or semantic meanings in undesirable ways and spoil their equivalence. "Undesirable ways" means in ways that the programming language itself cannot poke them. So, to get full abstraction, we need to ensure that the "contexts" available in the semantic model or the target language do come from those in the source language in some form. Note that this relates to the full completeness property.

Why do we want such properties? It has nothing to do with compilers! We want these properties in order to claim that the source language embeds into the target language. If we are happy with a particular target language (as being clean, understandable, somehow fundamental or God-given) then, if the source language embeds into it, then we can claim that there is nothing new in the source language. It is just a fragment of the target language that we know and love. It is just syntactic sugar. So, fully abstract translations are given by people to establish that particular target languages are great. They are also sometimes given by people who have a big or complicated language to deal with. So, instead of defining a semantics for it directly, they translate it to some core language and then give semantics to the core language. For instance, the Haskell report does this. But the full abstraction of these translations is rarely ever proved because the source languages are big and complicated. People take it on faith that the translation is good.

Once again, this has nothing to do with compilers. Compilers are rarely ever adequate or fully abstract. And, they don't need to be! All that a compiler needs to do is to preserve the execution behavior of complete programs. The target language of a compiler is generally huge, which means that it has lots of contexts that can mess up equivalence. So, equivalent programs in the source language are almost never contextually equivalent when compiled.

Answer 2

Summary: full completeness means that the interpretation function is not just complete, but also surjective on programs. Full abstraction has no requirement for surjectivity. $\newcommand{\semb}[1]{[\![ #1 ]\!]}$

Details: The detailed meaning of full abstraction and full completeness depends on the nature of what/where/how you are interpreting. Here is a rendition for the interpretation of one typed programming language into another. You have an interpretation function $\semb{.}$ which maps three things.

• Types $A$ of the source language to types $\semb{A}$ in the target language.

• Contexts $\Gamma$ in the source language to contexts $\semb{\Gamma}$ in the target language.

• Programs in context $\Gamma \vdash P : \alpha$ to programs in context $\semb{\Gamma} \vdash \semb{P} : \semb{\alpha}$.

In a categorical interpretation the first two maps collapse into one. The interpretation function can have various properties, e.g. it can be compositional, or preserve termination or ... Full abstraction is one such property. Recall that full abstraction of $\semb{.}$ means that

$$ P \cong^S Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T \semb{Q} $$

for all $P, Q$. Here $\cong^S$ is the chosen notion of typed program equivalence for the source language while $\cong^T$ plays that role for the target language. More precisely, because we are in a typed setting,

$$ P \cong^S_{\Gamma, \alpha} Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T_{\semb{\Gamma}, \semb{\alpha}} \semb{Q} $$ for all appropriate $\Gamma, \alpha, P, Q$. Full abstraction implies that $\semb{.}$ is sound and complete.The reason we speak of full abstraction and not just soundness & completeness is that we also want that the target language is 'somehow' non-trivial, e.g. not a term model. But formalising this non-triviality is hard, and we just allude to non-triviality by terminology.

Now full abstraction does not imply that $\semb{.}$ is surjective on types, contexts or programs in context.

Full completeness means that the map $\semb{.}$ is (complete and) surjective on programs in context for all definable contexts and definable types, i.e. any program $\semb{\Gamma} \vdash Q : \semb{\alpha}$ in the target language is the denotation of some $\Gamma \vdash P : \alpha$ in the source language, i.e. $Q = \semb{P}$. Note that this does not require $\semb{.}$ to be surjective on types and contexts, because that property rarely holds in the interpretations we are typically interested in.