The Free On-line Dictionary of Computing (30 December 2018):

Computational Adequacy Theorem

   This states that for any program (a non-function typed term in
   the typed lambda-calculus with constants) normal order
   reduction (outermost first) fails to terminate if and only if
   the standard semantics of the term is bottom.  Moreover,
   if the reduction of program e1 terminates with some head
   normal form e2 then the standard semantics of e1 and e2 will
   be equal.  This theorem is significant because it relates the
   operational notion of a reduction sequence and the
   denotational semantics of the input and output of a
   reduction sequence.