Computational Adequacy Theorem

This states that for any program (a non-function typed term inthe typed lambda-calculus with constants) normal order reduction (outermost first) fails to terminate if and only ifthe 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 willbe equal. This theorem is significant because it relates theoperational notion of a reduction sequence and thedenotational semantics of the input and output of areduction sequence.

单词	computational adequacy theorem
释义	Computational Adequacy Theorem Computational Adequacy Theorem This states that for any program (a non-function typed term inthe typed lambda-calculus with constants) normal order reduction (outermost first) fails to terminate if and only ifthe 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 willbe equal. This theorem is significant because it relates theoperational notion of a reduction sequence and thedenotational semantics of the input and output of areduction sequence.
随便看	judas hamaccabi judas hole judas-hole judas holes judas iscariot judas ishcariot judas iskariot judas kiss judas kisses judas maccabaeus judas maccabee judas maccabeus judas machabeus judas of galilee judas of gamala judas the galilean judas the maccabi judas tree judas trees judas window juddah juddaism judd, charles hubbard judd, donald judd, donald clarence