What's the intuition behind this definition of ordered pair in the $\lambda$-calculus?

393 Views Asked by At

On this page, we have the following definitions.

pair = λabf.fab
first = λp.p(λab.a)
second = λp.p(λab.b)

So I tried computing "first (pair a b)," and sure enough I got "a". But, this seems to happen almost by magic. Repeating the computation didn't really help, either.

What's the intuition behind these definitions?

1

There are 1 best solutions below

10
On BEST ANSWER

Continuation Passing Style

First, you would like get intuition about how

$$\lambda f.\ f\ 5\quad \text{ is equivalent to }\quad 5.$$

I will call the left one "cps" and the right "direct". This in not quite true (i.e. classical logic is different than intuitionistic one), but the difference, for now, is negligible. Namely, we assume that

\begin{align} \newcommand{tuple}[1]{\left\langle#1\right\rangle} \newcommand{a}{\mathtt{a}} \newcommand{b}{\mathtt{b}} \mathrm{cps} &= \lambda x.\ (\lambda f. f\ x) \\ \mathrm{direct} &= \lambda f. f (\lambda x. x) \end{align}

are transitions between the cps and the direct conventions. The intuition behind this is, how $5$ is packaged, it might be direct, e.g. you might be able to "touch" it, or it might be hidden, and to act on it you need to give away your actions to somebody else (you have no idea what they will do with them). In other words, direct style is like "here is 5 for you, do with it whatever you want", while cps is more like "here is a secure box with 5 inside it, tell me what you want to do, and I will get you the result" (if you want it to be more uniform, you can work with something like "...and I will get you a secure box with the result").

Currying

Currying and uncurrying are the transitions between

$$f_1 : \alpha \times \beta \to \gamma \quad \text{ and } \quad f_2 : \alpha \to \beta \to \gamma$$

The mappings are strightforward:

\begin{align} \mathrm{curry} &= \lambda f.\ \big(\lambda x.\ \lambda y.\ f\ \tuple{x,y}\big) \\ \mathrm{uncurry} &= \lambda f.\ \big(\lambda \tuple{x,y}.\ f\ x\ y\big) \end{align}

The important part is that when expecting a pair, you can obtain the first input, and then wait until you get the second one. The other direction is that, when you got a pair, you can extract the two inputs from it and feed it to the original function.

Church pairs

The Church pairs are combination of the above ideas. You don't have a way to express $\tuple{x,y}$, but you can pass multiple arguments around. So a Church pair is a secure box that says "I am a pair, give me a function that needs two arguments and I will tell you what is the result". You cannot touch the pair directly, because it doesn't exists, but you can treat the secure box as a pair if you don't mind giving your actions away. Surely, when you feed a function that ignores the second argument $\lambda x.\ \lambda y.\ x$, then the result will be the first argument, no magic here.

In other words, if you had pairs like $\tuple{\a,\b}$ you could make it into the secure box $$\mathrm{cps}\ \tuple{\a,\b} = \lambda f. f\ \tuple{\a,\b}.$$

Now you compose this secure box with uncurry to get

$$(\mathrm{cps}\ \tuple{\a,\b}) \circ \mathrm{uncurry} = \lambda f.\ (\mathrm{cps}\ \tuple{\a,\b})(\lambda \tuple{x,y}.\ f\ x\ y) = \lambda f. f\ \a\ \b,$$ that is, the Churych pair of $\a$ and $\b$. The other direction is similar, if you have $\lambda f.\ f\ \a\ \b$, then you could compose it with curry and then apply direct, i.e.

$$\mathrm{direct}\ ((\lambda f.\ f\ \a\ \b) \circ \mathrm{curry}) = \mathrm{direct}\ (\lambda f.\ f\ \tuple{\a,\b}) = \tuple{\a,\b} $$

I hope this helps $\ddot\smile$