How to find a simple function in Lambda Calculus?

98 Views Asked by At

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.

1

There are 1 best solutions below

2
On

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