<p><strong>Summary:</strong> 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 ]\!]}$</p>

<p><strong>Details:</strong> 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.</p>

<ul>
<li><p>Types $A$ of the source language to types $\semb{A}$ in the
target language.</p></li>
<li><p>Contexts $\Gamma$ in the source language to contexts
$\semb{\Gamma}$ in the target language.</p></li>
<li><p>Programs in context $\Gamma \vdash P : \alpha$ to programs in
context $\semb{\Gamma} \vdash \semb{P} : \semb{\alpha}$.</p></li>
</ul>

<p>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>

<p>$$
   P \cong^S Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T \semb{Q}
$$</p>

<p>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>

<p>$$
   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 &amp; 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.</p>

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

<p>Full completeness means that the map $\semb{.}$ is (complete and) surjective <strong>on
programs in context</strong> 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.</p>

CC BY-SA 3.0
2013-11-27T06:04:32.903Z
2013-11-27T09:25:55.537Z
2013-11-27T09:25:55.537Z
Martin Berger
<p>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.</p>

<p><strong>Full completeness</strong>:  "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 <em>logic</em> is sound and complete for a particular semantic model.  When we come to <em>constructive logic</em>, 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.  <em>A "complete" logic can prove everything it needs to.  A "fully complete" logic has all the proofs that it needs to have.</em>  So "full completeness" means "constructive completeness" or "proof completeness".  This has nothing to do with full abstraction.</p>

<p><strong>Full abstraction</strong>: "Adequate and fully abstract" is a property you want for the <em>semantic model</em> of a programming language.  (Note the first difference: we are now dealing with the properties of the <em>semantic model</em>, 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 <em>constructive</em> proof method.  (But, such a thing is theoretically possible, and one of these days somebody might do so.)</p>

<p>In your case, you are interested in <strong>translations</strong> 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 <em>adequate</em> 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 <em>fully abstract</em> if, whenever two source programs are observationally equivalent in the source language, their translations are equivalent in the target language.</p>

<p>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)$$</p>

<p>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 <em>fully complete</em> 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$$</p>

<p>Now for the <strong>vague connection</strong> 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.</p>

<p>Why do we want such properties?  It has <em>nothing</em> 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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-11-29T11:44:48.340Z
What do you mean by saying that there aren't any languages that we really fully "understand"?
Martin Berger
CC BY-SA 3.0
2013-11-29T11:45:30.983Z
What to you mean by saying that nobody has yet produced a semantic model that represents a constructive proof method?
Martin Berger
CC BY-SA 3.0
2013-11-29T11:46:50.473Z
@MartinBerger I mean that we understand them on the basis of an intrinsic notion of equality or equivalence, without having to appeal to observational equivalence.
Uday Reddy
CC BY-SA 3.0
2013-11-29T12:49:32.680Z
What's an "intrinsic notion of equality or equivalence"?
Martin Berger
CC BY-SA 3.0
2013-11-29T13:50:01.270Z
@MartinBerger: Without getting too philosophical about it, any definition of equality the way it is done for mathematical concepts in mathematics is good enough for me as an "intrinsic notion of equality".
Uday Reddy
CC BY-SA 3.0
2013-11-29T16:50:04.603Z
Looking at the prototypical mathematical equality, the ZF axiom of extensionality, I don't see why this is in some way better than contextual congruence. The latter is philosophically the right notion of equality for programs, while extensionality is the right concept for (well-founded) sets. Note that often, e.g. for typed processes, we can use bisimilarity to give an alternative characterisation of contextual congruence, one that does not require quantification over contexts.
Martin Berger
CC BY-SA 3.0
2014-03-26T03:39:15.797Z
Sorry, but the implications for "translations" seem in the wrong direction to me, compared to your earlier text. Full abstraction for, say, PCF asks for M≅N⟹τ(M)≅τ(N) (with τ being the denotational semantics, and ignoring the need to change symbols): as you say, "Full abstraction means that, if two terms are observationally equivalent, they have the same meaning in the semantic model".
But your implication is the other way around (namely, you write τ(M)≅τ(N)⟹M≅N)!

Or do translations work differently from denotational semantics?
Blaisorblade
CC BY-SA 3.0
2014-03-27T21:23:04.380Z
@Blaisorblade: You are absolutely right!  I made a correction to the text of my answer.
Uday Reddy
CC BY-SA 3.0
2014-05-28T20:46:10.600Z
Full abstraction is also of interest for language level security, and potentially for cross-language integration. I.e. it's useful to know that nothing in the target language can violate abstractions of the source language.
dmbarbour
CC BY-SA 3.0
2014-05-30T10:57:05.370Z
@dmbarbour: Those are interesting observations.  Perhaps you can amplify them by adding some text to the answer or, perhaps, in another answer of your own?  If you can give citations too, that would be brilliant.
Uday Reddy
CC BY-SA 3.0
2015-03-30T15:24:50.763Z
@UdayReddy: the security implications have been studied e.g. by Derek Dreyer. I recommend his research statement: https://mpi-sws.org/~dreyer/research.pdf
Blaisorblade
CC BY-SA 3.0
2013-11-28T23:07:30.010Z
2014-03-27T21:22:19.383Z
2014-03-27T21:22:19.383Z
Uday Reddy
<p>Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences.</p>

<p>Instead of providing full abstraction proofs, some recent (categorical based) compiler verification work by Hasegawa [<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops02.pdf">1</a>,<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops2004.pdf%E2%80%8E">2</a>] and Egger et. al. [<a href="http://arxiv.org/pdf/1209.4268v2">3</a>] prove the full completeness of various CPS translations.</p>

<p><strong>Question:</strong>
What is the difference between full completeness and full abstraction?</p>

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

<p><strong>Note</strong>: Both Curien [<a href="http://www.pps.univ-paris-diderot.fr/~curien/gordon-fs-plc.pdf%E2%80%8E">7</a>] and Abramsky [<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6390">8</a>] 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.</p>

<p><strong>Some Background</strong>:
The term "full completeness" was coined by Abramsky and Jagadeesan [<a href="http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=1C774E49D8104A9706EBD4359D334BE8?doi=10.1.1.12.6946&amp;rep=rep1&amp;type=pdf">4</a>] to characterize the correctness of a game-semantic model of Multiplicative Linear Logic.</p>

<p>Blute [<a href="http://www.site.uottawa.ca/~phil/papers/catsurv.web.pdf%E2%80%8E">5</a>] provides the following definition:</p>

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

<p>As far as I can tell, Hasegawa in [<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/girard.pdf">6</a>] 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 [<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops02.pdf">1</a>], he defines full completeness of the CPS translation $(\cdot)^\circ$ as:</p>

<blockquote>
  <p>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.</p>
</blockquote>

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

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

<p>Egger et. al. [<a href="http://arxiv.org/pdf/1209.4268v2">3</a>] define full completeness of a CPS translation $(\cdot)^v$ as a combination of (1) completeness and (2) fullness:</p>

<blockquote>
  <p>(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$</p>
  
  <p>(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$</p>
</blockquote>

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

<hr>

<p>[1] "<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops02.pdf">Linearly Used Effects: Monadic and CPS Transformations into Linear Lambda Calculus</a>", Hasegawa 2002</p>

<p>[2] "<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops2004.pdf%E2%80%8E">Semantics of Linear Continuation-Passing in Call-by-Name</a>", Hasegawa 2004</p>

<p>[3] "<a href="http://arxiv.org/pdf/1209.4268v2">Linear-use CPS Translations in the Enriched Effect Calculus</a>", Egger et. al. 2012</p>

<p>[4] "<a href="http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=1C774E49D8104A9706EBD4359D334BE8?doi=10.1.1.12.6946&amp;rep=rep1&amp;type=pdf">Games and Full Completeness for Multiplicative Linear Logic</a>", Abramsky and Jagadeesan 1992</p>

<p>[5] "<a href="http://www.site.uottawa.ca/~phil/papers/catsurv.web.pdf%E2%80%8E">Category Theory for Linear Logicians</a>", Blute 2003</p>

<p>[6] "<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/girard.pdf">Girard Translation and Logical Predicates</a>", Hasegawa 2000</p>

<p>[7] "<a href="http://www.pps.univ-paris-diderot.fr/~curien/gordon-fs-plc.pdf%E2%80%8E">Definability and full abstraction</a>", Curien 2007</p>

<p>[8] "<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6390">Axioms for Definability and Full Completeness</a>", Abramsky 1999</p>

<pl.programming-languages><ct.category-theory><semantics><denotational-semantics><program-verification>
Full Completeness vs Full Abstraction of a program translation
Phillip Mates
# Full Completeness vs Full Abstraction of a program translation

(Asked by: username_0 on 2013-11-27)

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](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops02.pdf),[2](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops2004.pdf%E2%80%8E)] and Egger et. al. [[3](http://arxiv.org/pdf/1209.4268v2)] 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](http://www.pps.univ-paris-diderot.fr/~curien/gordon-fs-plc.pdf%E2%80%8E)] and Abramsky [[8](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6390)] 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](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=1C774E49D8104A9706EBD4359D334BE8?doi=10.1.1.12.6946&rep=rep1&type=pdf)] to characterize the correctness of a game-semantic model of Multiplicative Linear Logic.

Blute [[5](http://www.site.uottawa.ca/~phil/papers/catsurv.web.pdf%E2%80%8E)] 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](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/girard.pdf)] 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](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops02.pdf)], 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](http://arxiv.org/pdf/1209.4268v2)] 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](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops02.pdf)", Hasegawa 2002

[2] "[Semantics of Linear Continuation-Passing in Call-by-Name](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/flops2004.pdf%E2%80%8E)", Hasegawa 2004

[3] "[Linear-use CPS Translations in the Enriched Effect Calculus](http://arxiv.org/pdf/1209.4268v2)", Egger et. al. 2012

[4] "[Games and Full Completeness for Multiplicative Linear Logic](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=1C774E49D8104A9706EBD4359D334BE8?doi=10.1.1.12.6946&rep=rep1&type=pdf)", Abramsky and Jagadeesan 1992

[5] "[Category Theory for Linear Logicians](http://www.site.uottawa.ca/~phil/papers/catsurv.web.pdf%E2%80%8E)", Blute 2003

[6] "[Girard Translation and Logical Predicates](http://www.kurims.kyoto-u.ac.jp/~hassei/papers/girard.pdf)", Hasegawa 2000

[7] "[Definability and full abstraction](http://www.pps.univ-paris-diderot.fr/~curien/gordon-fs-plc.pdf%E2%80%8E)", Curien 2007

[8] "[Axioms for Definability and Full Completeness](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6390)", Abramsky 1999

**Tags:** pl.programming-languages, ct.category-theory, semantics, denotational-semantics, program-verification

---

## 2 answers

### Answer by username_2 on 2013-11-28. Score: 13 | Accepted answer

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.

> **Comments:**
> **username_1**: What do you mean by saying that there aren't any languages that we really fully "understand"?  
> **username_1**: What to you mean by saying that nobody has yet produced a semantic model that represents a constructive proof method?  
> **username_2**: @MartinBerger I mean that we understand them on the basis of an intrinsic notion of equality or equivalence, without having to appeal to observational equivalence.  
> **username_1**: What's an "intrinsic notion of equality or equivalence"?  
> **username_2**: @MartinBerger: Without getting too philosophical about it, any definition of equality the way it is done for mathematical concepts in mathematics is good enough for me as an "intrinsic notion of equality".  
> **username_1**: Looking at the prototypical mathematical equality, the ZF axiom of extensionality, I don't see why this is in some way better than contextual congruence. The latter is philosophically the right notion of equality for programs, while extensionality is the right concept for (well-founded) sets. Note that often, e.g. for typed processes, we can use bisimilarity to give an alternative characterisation of contextual congruence, one that does not require quantification over contexts.  
> **username_3**: Sorry, but the implications for "translations" seem in the wrong direction to me, compared to your earlier text. Full abstraction for, say, PCF asks for M≅N⟹τ(M)≅τ(N) (with τ being the denotational semantics, and ignoring the need to change symbols): as you say, "Full abstraction means that, if two terms are observationally equivalent, they have the same meaning in the semantic model". But your implication is the other way around (namely, you write τ(M)≅τ(N)⟹M≅N)!  Or do translations work differently from denotational semantics?  
> **username_2**: @Blaisorblade: You are absolutely right!  I made a correction to the text of my answer.  
> **username_4**: Full abstraction is also of interest for language level security, and potentially for cross-language integration. I.e. it's useful to know that nothing in the target language can violate abstractions of the source language.  
> **username_2**: @dmbarbour: Those are interesting observations.  Perhaps you can amplify them by adding some text to the answer or, perhaps, in another answer of your own?  If you can give citations too, that would be brilliant.  
> **username_3**: @UdayReddy: the security implications have been studied e.g. by Derek Dreyer. I recommend his research statement: https://mpi-sws.org/~dreyer/research.pdf  

---

### Answer by username_1 on 2013-11-27. Score: 5

**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.


---

