Exercise
13 March
Definition:A combinator
is a λ-term with no free variables.
Some important combinators:
- I = λ x . x
- K = λ x . λ y . x
- S = λ f . λ g . λ x . f x (g x)
- B = λ f . λ g . λ x . f (g x)
- C = λ f . λ x . λ y . f y x
- W = λ f . λ x . f x x
- Y = λ f . (λ x . f (x x)) (λ x . f (x x))
These definitions are frequently presented directly as a
simple rewriting system:
- I x = x
- K x y = x
- S f g x = f x (g x)
- B f g x = f (g x)
- C f x y = f y x
- W f x = f x x
One can show equations relating these combinators
using the above combinator equations and extensionality,
for example, I = S K K
because
S K K x = K x (K x) = x = I x.
Theorem:
All combinators can be proven equal to some combination of S.
Exercise:
Derive such combinations for the remaining combinators listed above.
Wolfram Kahl: FP2006