Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 61: | Line 61: | ||
** only the outermost redexes are reduced, and the right hand side must be in β-η-normal form before reducing the left | ** only the outermost redexes are reduced, and the right hand side must be in β-η-normal form before reducing the left | ||
** this is ''strict'' evaluation (arguments are always evaluated, whether used or not) | ** this is ''strict'' evaluation (arguments are always evaluated, whether used or not) | ||
* leftmost-outermost application substitutes prior to evaluation, and is equivalent to lazy call-by-name ( | * leftmost-outermost application substitutes prior to evaluation, and is equivalent to lazy call-by-name sans memoization ("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 operationally equivalent to call-by-name if side-effects are disallowed (it can be more efficient, but also more complicated: reduction is performed on abstract syntax graphs rather than abstract syntax trees). 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 operationally equivalent to call-by-name if side-effects are disallowed (it can be more efficient, but also more complicated: reduction is performed on abstract syntax graphs rather than abstract syntax trees). 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. | ||