Source : Free On-Line Dictionary of Computing

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.