Church Encoding - Church Pairs

Church Pairs

Church 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