Church Pairs
See also: ConsChurch pairs are the Church encoding of the pair (two-tuple) type. The pair is represented as a function that takes a function argument. When given its argument it will apply the argument to the two components of the pair.
Formal definition in lambda calculus:
- pair ≡
λx.λy.λz.z x y - fst ≡
λp.p (λx.λy.x) - snd ≡
λp.p (λx.λy.y)
An example:
- fst (pair a b) ≡
(λp.p (λx.λy.x)) ((λx.λy.λz.z x y) a b) ≡ (λp.p (λx.λy.x)) (λz.z a b) ≡ (λz.z a b) (λx.λy.x) ≡ (λx.λy.x) a b ≡ a
Read more about this topic: Church Encoding
Famous quotes containing the word church:
“A State, in idea, is the opposite of a Church. A State regards classes, and not individuals; and it estimates classes, not by internal merit, but external accidents, as property, birth, etc. But a church does the reverse of this, and disregards all external accidents, and looks at men as individual persons, allowing no gradations of ranks, but such as greater or less wisdom, learning, and holiness ought to confer. A Church is, therefore, in idea, the only pure democracy.”
—Samuel Taylor Coleridge (1772–1834)