Church Encoding - Church Pairs

Church Pairs

See also: Cons

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

Read more about this topic: Church Encoding

Famous quotes containing the word church:

“Midnight has come and the great Christ Church bell
And many a lesser bell sound through the room;
And it is All Souls’ Night.
And two long glasses brimmed with muscatel
Bubble upon the table. A ghost may come;
For it is a ghost’s right....”
—William Butler Yeats (1865–1939)