Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 50: | Line 50: | ||
* ''η-reduction'' eliminates bindings unused within a scope, preserving ''η-equivalence'': | * ''η-reduction'' eliminates bindings unused within a scope, preserving ''η-equivalence'': | ||
** (λx. (f x)) →<sub>η</sub> f | ** (λx. (f x)) →<sub>η</sub> f | ||
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: | |||
* leftmost-innermost application evaluates arguments as soon as possible, and is equivalent to call-by-value | |||
* leftmost-outermost application substitutes prior to evaluation, and is equivalent to lazy call-by-name (call-by-necessity) | |||
* call-by-name terminates if any order does, but might require more total reductions | |||
====Numerics==== | ====Numerics==== | ||