Adequacy and Full Abstraction (PL Theory)

In programming language theory, we often relate:

• A source language
• A target language or model

together with notions of program equivalence and a translation between them.
The notions of Adequacy and Full Abstraction characterize how well this translation relates the two worlds.

Basic Setting

Let and be two programming languages (or models of programming languages).
Let and be two notions of equivalence of programs for each of these languages respectively.
Let be a translation from to .

Adequacy

A translation is adequate (for ) if for any two -programs :

In other words:

Programs that are equivalent after translation were already equivalent.

The point of adequate translations is that is often significantly easier to reason about than . It is thus simpler to translate programs to , prove them equivalent there, and then use adequacy to “lift” that into an equivalence between the original programs.

Often, is not an actual language, but a mathematical model for the language — for example a denotational semantics.

The notion of adequacy was introduced by Robin Milner in a paper presented at the 1973 Logic Colloquium in Bristol.

Full Abstraction

A translation is fully abstract (with respect to and ) if for any two -programs :

In other words:

A translation between programming languages is fully abstract iff it preserves and reflects program equivalence.

This consists of two directions:

1. Equivalent programs are translated to equivalent programs
   

2. Programs that are equivalent after translation were already equivalent (a.k.a. adequacy)
   

Surprisingly, the second point is more often true, and in fact easier to prove — even though it looks like a sort of completeness.

In Denotational Semantics

The above definition is intentionally informal, in order to cover more recent uses of the notion of full abstraction. However, the origin of the term comes from the case where is not a programming language at all, but rather a denotational semantics of the source language . In that case, the equivalence is mathematical equality (in the appropriate metatheory, e.g. ZFC, HOL, or type theory).

References

Milner, Robin. Processes: A Mathematical Model of Computing Agents. In Logic Colloquium ’73, Studies in Logic and the Foundations of Mathematics 80:157–173. Elsevier, 1975. https://doi.org/10.1016/S0049-237X(08)71948-7

Ong, C.-H. L. “Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF.” In Handbook of Logic in Computer Science, Vol. 4, edited by S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum. Oxford University Press, 1995.