VDict - Definition of Computational Adequacy Theorem

Computing (FOLDOC) dictionary

Computational Adequacy Theorem

This states that for any program (a non-function typed term in

the typed lambda-calculus with constants) normal orderreduction (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 headnormal 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.

Related search result for "Computational Adequacy Theorem"

Words contain "Computational Adequacy Theorem" in its definition in Computing (FOLDOC) dictionary:
Computational Adequacy Theorem normal order reduction Green's Theorem four colour map theorem DeMorgan's theorem computational complexity ill-behaved General Recursion Theorem head normalisation theorem Infinite Monkey Theorem more...