Programming Language Theory: Difference between revisions
| Line 8: | Line 8: | ||
''Higher-order functions'' map one or more functions to a function. | ''Higher-order functions'' map one or more functions to a function. | ||
===Combinatory Logic=== | ===Combinatory Logic=== | ||
====SKI Calculus==== | |||
*<tt>I ≡ λx. x</tt> | |||
*<tt>K ≡ λx, y. x</tt> | |||
*<tt>S ≡ λx, y, z. (x z (y z))</tt> | |||
====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: | ||
| Line 14: | Line 18: | ||
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> (via η-expansion on Y) | * <tt>Z ≡ λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))</tt> (via [http://mlton.org/EtaExpansion η-expansion] on Y) | ||
The infinitely many fixed-point combinators of untyped λ-calculus are recursively enumerable. | The infinitely many fixed-point combinators of untyped λ-calculus are recursively enumerable. | ||