Programming Language Theory: Difference between revisions

Line 13: Line 13:
*<tt>S ≡ λx, y, z. (x z (y z))</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:
For a function F, its set of ''fixed points'' are those inputs which map to themselves. The ''fixed-point combinators'' 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> (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)