Lambda representability for boolean function 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.
 A: 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}

