Encoding pair in lambda calculus

Question

I am confused about the logic behind how lambda calculus encodes the pair data structure.

In lambda calculus, PAIR is encoded as

PAIR := λx.λy.λf. f x y

.

Why can't I just encode it as

PAIR := λx.λy. x y

or

PAIR := λf.λx.λy. f x y

?

What is the design choice when doing such encoding?

Answer 1

Given two arguments x, y, the pair function is supposed to take a new function f and apply it to the "pair" of arguments. I will try to give an intuitive view, now let's see what your examples do:

λx.λy. x y

This function takes two arguments, and passes the second (y) as an argument to the first (x). So this is just function application.

λf.λx.λy. f x y

On the surface this looks similar to the original, but it has an issue. Here we get the function to which the two arguments are gonna be supplied to as the first argument. This means it is not possible to actually store the two arguments x,y, which is why the original is the version that makes sense.

Answer 2

This is known as Church pairs.

One should keep in mind that pair and PAIR are not the same thing.

• PAIR build a pair: given two arguments, PAIR return pair
• pair allow to retrieve the pair elements

To retrieve the pair elements, you need to be able to feed it with a callback function, that why you need f.

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.