Full abstraction

Let \mathcal{S} and \mathcal{T} be two programming languages (or models of programming languages). Let \approx_\mathcal{S} and \approx_\mathcal{T} be two notions of equivalence of programs for each of these languages respectively.

Let \llbracket - \rrbracket be a translation from \mathcal{S} to \mathcal{T}. This translation is fully abstract (wrt to \approx_\mathcal{S} and \approx_\mathcal{T}) if for any two \mathcal{S}-programs P, Q

  P \approx_\mathcal{S} Q
  \quad  \Longleftrightarrow \quad
  \llbracket P \rrbracket \approx_\mathcal{T} \llbracket Q \rrbracket

In other words: a translation between programming languages is fully abstract iff it preserves and reflects program equivalence:

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 \mathcal{T} is not a programming language at all, but rather a denotational semantics of the source language \mathcal{S}. In that case, the equivalence \approx_\mathcal{T} is mathematical equality = (in the appropriate metatheory, e.g. ZFC, HOL, or type theory).

See also

• Full abstraction for PCF

References

• The notion of full abstraction was introduced by Robin Milner in a paper presented at the 1973 Logic Colloqium in Bristol:

@inproceedings{milner_1975,
	title = {Processes: A Mathematical Model of Computing Agents},
	volume = {80},
	doi = {10.1016/S0049-237X(08)71948-7},
	series = {Studies in Logic and the Foundations of Mathematics},
	pages = {157--173},
	booktitle = {Logic Colloquium '73},
	publisher = {Elsevier},
	author = {Milner, Robin},
	date = {1975},
}

• A survey of the full abstraction problem, in particular as it relates to PCF, is

@incollection{ong_correspondence_1995,
	title = {Correspondence between operational and denotational semantics: the full abstraction problem for {PCF}},
	volume = {4},
	booktitle = {Handbook of {Logic} in {Computer} {Science}},
	publisher = {Oxford University Press},
	author = {Ong, C.-H. L.},
	editor = {Abramsky, S. and Gabbay, Dov M. and Maibaum, T. S. E.},
	year = {1995}
}