Search code examples
lambda-calculus

Encoding pair in lambda calculus

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?

Solution

  • 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.