1

Given a pair $[M_1,M_2]$ there is an easy encoding $\lambda x.x M_1 M_2$. For the n-tuple we have two options. First encoding: $$\lambda x.x M_1, M_2, \ldots , M_n$$ Second encoding: $$[M_0, [M_1 , [M_2, \ldots ]]] = \lambda x.xM_0 \lambda y.y M_1 \lambda z.z M_2 \ldots$$ For the first encoding it is easy to define projectors to extract the k-th value: $\lambda x_1 x_2 \ldots x_n . x_k$ What I can't understand is how is it possible to extract a value from an n-tuple encoded in the second way.

I am told that the following projector works: $$\pi^n_k = \lambda x.x F^k T$$ Where $T=\lambda xy.x$ and $F=\lambda xy.y$

But according to my calculations that does not work. Can you provide me with a working example?

Vitaly Olegovitch
  • 586

1 Answers1

1

Here's how you can verify that the projection works for that second encoding. Let's consider the triple $\langle M_0, \langle M_1, \langle M_2\rangle\rangle\rangle$, which according to the encoding is: $[\lambda x.xM_0\lambda y.yM_1\lambda z.zM_2]$. Let's see.

$$\pi^3_0(\langle M_0, \langle M_1, \langle M_2\rangle\rangle\rangle) \stackrel{?}{\equiv} M_0 ;$$

Let's substitute the contents of $\pi$ and the encoding of the triple into that formula:

$$[\lambda x.xF^0T]~([\lambda x.xM_0\lambda y.yM_1\lambda z.zM_2])\stackrel{?}{\equiv} M_0;$$

Cancel the $F^0$ and evaluate the redex obtaining:

$$[\lambda x.xM_0\lambda y.yM_1\lambda z.zM_2]~(T)\stackrel{?}{\equiv} M_0;$$

Since $T := [\lambda x,y.x]$, we have:

$$[\lambda x.xM_0\lambda y.yM_1\lambda z.zM_2]~([\lambda x,y.x])\stackrel{?}{\equiv} M_0;$$

Which we substitute again to obtain:

$$[\lambda x,y.x]~(M_0)(\lambda y.yM_1\lambda z.zM_2)\stackrel{?}{\equiv} M_0;$$

Which, since $T$ is the $x\text{-}id$, reduces to:

$$M_0\stackrel{\checkmark}{\equiv} M_0.$$

Even if this procedure is clear to you, try to extract the third term (viz. $M_2$) to get a feel for it. You'll have two $F$s passed to the triple, which will have the effect of skipping $M_0$ and $M_1$, leaving you with $[\lambda z.zM_2]$, which will then be selected by the $T$.

Hunan Rostomyan
  • 2,055