Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 57: | Line 57: | ||
** An expression is in ''β-η-normal form'' ("Beta-eta-normal form") if neither β- nor η-reductions are possible | ** An expression is in ''β-η-normal form'' ("Beta-eta-normal form") if neither β- nor η-reductions are possible | ||
*** If a η-reduction is applicable, the expression is a ''η-redex''. | *** If a η-reduction is applicable, the expression is a ''η-redex''. | ||
According to the Church-Rosser Theorem, all terminating evaluations will compute the same function. Certain application orders might not terminate for a given expression, though, despite termination via other orders. This gives rise to the core difference between call-by-value and call-by-name semantics: | According to the Church-Rosser Theorem, all terminating evaluations will compute the same function. Certain application orders might not terminate for a given expression, though, despite termination via other orders (proofs under arbitrary reduction ordering are said to operate under ''full beta reduction''). This gives rise to the core difference between call-by-value and call-by-name semantics: | ||
* leftmost-innermost application evaluates arguments as soon as possible, and is equivalent to leftmost call-by-value ("applicative order") | * leftmost-innermost application evaluates arguments as soon as possible, and is equivalent to leftmost call-by-value ("applicative order") | ||
** only the outermost redexes are reduced, and the right hand side must be in β-η-normal form before reducing the left | |||
* leftmost-outermost application substitutes prior to evaluation, and is equivalent to lazy call-by-name (call-by-necessity, "normal order") | * leftmost-outermost application substitutes prior to evaluation, and is equivalent to lazy call-by-name (call-by-necessity, "normal order") | ||
Call-by-name terminates if any order does, but might require more total reductions. Call-by-value only β-reduces abstractions, not applications. Call-by-need memoizes the results of evaluated functions, and is equivalent to call-by-name if side-effects are disallowed. Call-by-name is text substitution augmented by capture avoidance. Wikipedia's [http://en.wikipedia.org/wiki/Evaluation_strategy evaluation strategy] page is pretty thorough. | Call-by-name terminates if any order does, but might require more total reductions. Call-by-value only β-reduces abstractions, not applications. Call-by-need memoizes the results of evaluated functions, and is equivalent to call-by-name if side-effects are disallowed. Call-by-name is text substitution augmented by capture avoidance. Wikipedia's [http://en.wikipedia.org/wiki/Evaluation_strategy evaluation strategy] page is pretty thorough. | ||