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:
“It is a dogma of the Roman Church that the existence of God can be proved by natural reason. Now this dogma would make it impossible for me to be a Roman Catholic. If I thought of God as another being like myself, outside myself, only infinitely more powerful, then I would regard it as my duty to defy him.”
—Ludwig Wittgenstein (1889–1951)