Programming Language Theory: Difference between revisions
| Line 12: | Line 12: | ||
* <tt>Y ≡ λf. (λx. f (x x)) (λx. f (x x))</tt> (untyped λ-calculus) | * <tt>Y ≡ λf. (λx. f (x x)) (λx. f (x x))</tt> (untyped λ-calculus) | ||
* <tt>Y ≡ S (K (S I I)) (S (S (K S) K) (K (S I I)))</tt> (SKI calculus) | * <tt>Y ≡ S (K (S I I)) (S (S (K S) K) (K (S I I)))</tt> (SKI calculus) | ||
Divergence-free evaluation of the Y-combinator requires call-by-name semantics. Call-by-value semantics can make use of the Θ<sub></sub> | 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></sub> | * <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> | ||
The Z-combinator is derived via η-expansion on Y. | The Z-combinator is derived via η-expansion on Y. | ||