Programming Language Theory: Difference between revisions
| Line 14: | Line 14: | ||
Divergence-free evaluation of the Y-combinator requires call-by-name semantics. Call-by-value semantics can make use of the Θ<sub>v</sub> (Turing) or Z-combinators: | Divergence-free evaluation of the Y-combinator requires call-by-name semantics. Call-by-value semantics can make use of the Θ<sub>v</sub> (Turing) or Z-combinators: | ||
* <tt>Θ<sub>v</sub> ≡ (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))</tt> | * <tt>Θ<sub>v</sub> ≡ (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))</tt> | ||
* <tt>Z ≡ λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))</tt> | * <tt>Z ≡ λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))</tt> (via η-expansion on Y) | ||
The infinitely many fixed-point combinators of untyped λ-calculus are recursively enumerable. | |||
===Untyped λ-calculus=== | ===Untyped λ-calculus=== | ||