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:
“If I should go out of church whenever I hear a false statement I could never stay there five minutes. But why come out? The street is as false as the church, and when I get to my house, or to my manners, or to my speech, I have not got away from the lie.”
—Ralph Waldo Emerson (1803–1882)