Programming Language Theory: Difference between revisions
| Line 10: | Line 10: | ||
====Fixed-Point Combinators==== | ====Fixed-Point Combinators==== | ||
Higher-order functions which compute the fixed points of their inputs. Curry's ''Y-combinator'' was the first: | Higher-order functions which compute the fixed points of their inputs. Curry's ''Y-combinator'' was the first: | ||
* <tt>Y ≡ λf. (λx. f (x x)) (λx. f (x x))</tt> | * <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) | |||
Divergence-free evaluation of the Y-combinator requires call-by-name semantics. Call-by-value semantics can make use of the Θ<sub></sub>v (Turing) or Z-combinators: | |||
* <tt>Θ<sub></sub>v ≡ (λ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> | |||
The Z-combinator is derived via η-expansion on Y. | |||
===Untyped λ-calculus=== | ===Untyped λ-calculus=== | ||