Adequacy

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 adequate for \approx_\mathcal{S} if for any two \mathcal{S}-programs P, Q

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

In other words: programs that are equivalent after translation were already equivalent.

The point of adequate translations is that \approx_{\mathcal{T}} is often significantly easier to reason about than \approx_{\mathcal{S}}. It is thus simpler to translate programs to \mathcal{T}, prove them equivalent there, and then use adequacy to 'lift' that into an equivalence between the original programs.

Often, \mathcal{T} is not an actual language, but a mathematical model for the language - for example a denotational semantics.

References

• The notion of adequacy 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},
}