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 . This translation is fully abstract (wrt 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:
Surprisingly, the second point is more often true, and in fact easier to prove - even though it looks like a sort of completeness.
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).
Milner, Robin. ‘Processes: A Mathematical Model of Computing Agents’. In Logic Colloquium ’73, 80:157–73. Studies in Logic and the Foundations of Mathematics. Elsevier, 1975. https://doi.org/10.1016/S0049-237X(08)71948-7.
@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},
}
Ong, C.-H. L. 1995. ‘Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF’. In Handbook of Logic in Computer Science, edited by S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum. Vol. 4. Oxford University Press. [pdf]
@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}
}