1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ You're very welcome! $\endgroup$ – Hunan Rostomyan Apr 20 '14 at 8:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.