Computer Dictionary/Computational Adequacy Theorem

Jump to: navigation, search

This states that for any program (a non-function typed term in the typed lambda-calculus with constants) [[Computer Dictionary/normal order reduction|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 [[Computer Dictionary/head normal form|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.

Discussion about "Computer Dictionary/Computational Adequacy Theorem":

None Discussion Now.

Add Discussion