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 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.
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},
}