2
$\begingroup$

I was doing this exercise : Find the function $$exchange$$ such that: $$(exchange)t \simeq \lambda p(p)t_2 t_1$$ where $$t= \lambda p(p)t_1 t_2.$$ I found $$ exchange= \lambda p(p) (\lambda c (S \ \textit{FALSE} \ \textit{TRUE} (c))) $$ where $$\textit{TRUE} = \lambda x \lambda y x$$ $$\textit{FALSE}= \lambda x \lambda y y$$ $$S= \lambda x \lambda y \lambda z(xz(yz))$$

Is it correct? Thank you, Alessandro.

$\endgroup$
1
$\begingroup$

Your proposal for the term $exchange$ does not seem to work. Let's see the $\beta$-conversion step by step.

Notations: $\to_\beta$ stands for one $\beta$-reduction step, $\to_\beta^*$ stands for several $\beta$-reduction steps (i.e. some $\beta$-reduction steps are left implicit). The terms $TRUE$ and $FALSE$ are denoted by $T$ and $F$, respectively.

First, note that

$$S F T c \to_\beta^* (F c)(T c) \to_\beta (\lambda y y) (T c) \to_\beta T c \to_\beta \lambda y c.$$

Therefore, taking your definition of $exchange$, we have

$$(exchange)t \to_\beta (\lambda p (p) t_1 t_2) (\lambda c S F T c) \to_\beta (\lambda c S F T c) t_1 t_2 \to_\beta^* (\lambda c \lambda y c)t_1 t_2 \to_\beta^* t_1 \neq \lambda p (p) t_2 t_1.$$

But, if we set

$$\tag{1} exchange = \lambda z (z)(\lambda x \lambda y \lambda p (p) y x) $$

then,

$$ (exchange)t \to_\beta (\lambda p (p) t_1 t_2)(\lambda x \lambda y \lambda p (p) y x) \to_\beta (\lambda x \lambda y \lambda p (p) y x) t_1 t_2 \to_\beta^* \lambda p (p) t_2 t_1 $$

which is exactly what we are looking for!


Edit: There is no general strategy to answer questions like this, intuition is always your best friend. Anyway, I can try to explain how I found the answer. I hope you can follow my intuition.

First, since I have to switch the position of $t_1$ and $t_2$ in the argument $t$, one of the most simple (for me) idea is: let's try if I can solve the problem by moving the argument $t$ in head position (any term can be written in a unique way as $\lambda x_1 \dots \lambda x_n (s) r_1 \dots r_m$, for some $n, m \geq 0$: $s$ is the head position of this term). Under this assumption (and there is no guarantee that it will work), $exchange$ should be of the form $$ \tag{2} exchange = \lambda z \, zM $$ where $M$ is a term to define. Indeed, according to this definition of $exchange$, we have $$ (exchange)t \to_\beta tM \,. $$ Since $t = \lambda p (p) t_1 t_2$, then $$ tM \to_\beta M t_1 t_2\,. $$ Now, we have to define $M$ in order to get $$M t_1 t_2 \to_\beta^* \lambda p (p) t_2 t_1\,.$$ It is simple to find such a $M$! It should have a $p$ in head position and swap the two arguments $t_1$ and $t_2$ under the abstraction $\lambda p$. Thus, it is enough to set $$M = \lambda x \lambda y \lambda p (p) y x\,.$$ Going back to the definition $(2)$, we get (1).

$\endgroup$
  • $\begingroup$ How do I understand which is the strategy that I have to follow to create this simple function? Thank you for answering. $\endgroup$ – Alessandro Recchia Sep 13 '18 at 9:51
  • $\begingroup$ @AlessandroRecchia - I added an edit at the end of my answer. I hope it is clear. $\endgroup$ – Taroccoesbrocco Sep 13 '18 at 12:44

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.