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.
Nearby terms:
Compusult Ltd. « computability theory « computable «
Computational Adequacy Theorem » computational
complexity » Computational Fluid Dynamics »
computational geometry
|
