Lambda representability for boolean function

Question

I have the following $\lambda$-term $$F=\lambda xy.(M(Nxy))$$
where $$M=\lambda zxy.zyx \qquad N=\lambda xy.xxy$$
The term $F$ represents some boolean function of two arguments $f(x,y)$. So I need to describe this function. I think that I should act with this term on the terms $\mathsf{T} = \lambda xy.x$ and $\mathsf{F} = \lambda xy.y$ and do $\beta$-reduction after that. Is it true? Or I need to act differently? It is hard to understand for me, because I haven’t dealt with $\lambda$-representability before.

Answer 1

Yes, your idea is correct. For $P = \lambda xy.M(Nxy)$ (I renamed the term $P$ to avoid confusion with $F = \lambda xy.y$), you have to consider all the possible applications to two booleans (which are $T$ and $F$), i.e. you have to consider the terms $PTT$, $PTF$, $PFT$ and $PFF$, and $\beta$-reduce them to their normal forms, which are still booleans. In this way, you can draw a truth table for $P$, which is the truth table of the boolean function represented by $P$.

---

Concretely, first consider that ($x,y,z$ stands for a term whatsoever)

\begin{align} NTz &= (\lambda xy.xxy)Tz &&& NFz &= (\lambda xy.xxy)Fz \\ &\to_\beta (\lambda y.TTy)z &&& &\to_\beta (\lambda y.FFy)z \\ &\to_\beta TTz &&& &\to_\beta FFz \\ &= (\lambda x'y'.x')Tz &&& &= (\lambda x'y'.y')Fz \\ &\to_\beta (\lambda y'.T)z &&& &\to_\beta (\lambda y'.y')z \\ &\to_\beta T &&& &\to_\beta z \end{align}

\begin{align} Txy &= (\lambda x'y'.x')xy &&& Fxy &= (\lambda x'y'.y')xy \\ &\to_\beta (\lambda y'.x)y &&& &\to_\beta (\lambda y'.y')y \\ &\to_\beta x &&& &\to_\beta y \end{align}

\begin{align} MT &= (\lambda zxy.zyx)T &&& MF &= (\lambda zxy.zyx)F \\ &\to_\beta \lambda xy.Tyx &&& &\to_\beta \lambda xy.Fyx \\ &\to_\beta^* \lambda xy.y &&& &\to_\beta^* \lambda xy.x \\ &= F &&& &= T \end{align}

Hence,

! \begin{align} PTT &= (\lambda xy.M(Nxy))TT &&& PTF &= (\lambda xy.M(Nxy))TF \\ &\to_\beta (\lambda y. M(NTy))T &&& &\to_\beta (\lambda y. M(NTy))F \\ &\to_\beta M(NTT) &&& &\to_\beta M(NTF) \\ &\to_\beta^* MT &&& &\to_\beta^* MF \\ &\to_\beta^* F &&& &\to_\beta^* T \end{align}

! \begin{align} PFT &= (\lambda xy.M(Nxy))FT &&& PFF &= (\lambda xy.M(Nxy))FF \\ &\to_\beta (\lambda y. M(NFy))T &&& &\to_\beta (\lambda y. M(NFy))F \\ &\to_\beta M(NFT) &&& &\to_\beta M(NFF) \\ &\to_\beta^* MT &&& &\to_\beta^* MF \\ &\to_\beta^* F &&& &\to_\beta^* T \end{align}