Boolean function encoded with lambda calculus

103 Views Asked by At

I have a function $G = \lambda xy.(M(N x y))$, where $M = \lambda zxy.zyx$ and $N = \lambda xy.xyx$, which encodes a boolean function of two arguments $f(x,y)$

By $\beta$-reduction, $G T T$ and $G T F$ (where $T = \lambda xy.x$ and $F = \lambda xy.y$ represent the booleans true and false, respectively) reduce to $\lambda xy. xyx T T$ and $\lambda xy. xyx F T$ and equivalently for the other two combination of booleans.

So basically you could say, that given two arguments $A$ and $B$: $$ GAB = \lambda xy. xyx B A $$ And as far as I know, $\lambda xy. xyx$ defines AND operation.

So, that should mean that I have a logical operation $AND$ which takes the two arguments provided.

However, when I test $G$ using Mikrokosmos with those values I get a table of the logical operation $NAND$

\begin{array}{|c c|c|} x& y & f(x,y)\\ T & T & F\\ T & F & T\\ F & T & T\\ F & F & T\\ \end{array}

Am I missing something in my $\beta$-reduction or am I misinterpreting the results? Which one is correct?

1

There are 1 best solutions below

0
On BEST ANSWER

The result shown by Mikrokosmos is correct. It is not true that $GTT$ $\beta$-reduces to $\lambda xy.xyxTT$. Let us see why.

It is true that $N = \lambda xy.xyx $ represent the logical connective $\mathit{AND}$. Indeed,

\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}

and so

\begin{align} NTz &= (\lambda xy.xyx)Tz &&& NFz &= (\lambda xy.xyx)Fz \\ &\to_\beta (\lambda y.TyT)z &&& &\to_\beta (\lambda y.FyF)z \\ &\to_\beta TzT &&& &\to_\beta FzF \\ &\to_\beta^* z &&& &\to_\beta F \end{align}

Moreover, $M = \lambda zxy.zyx$ represents the logical connective $\mathit{NOT}$. Indeed,

\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}

Therefore, $G$ represents the logical connective $\mathit{NAND}$. Indeed, \begin{align} GTT &= (\lambda xy. M(Nxy))TT &&& GTF &= (\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} GFT &= (\lambda xy. M(Nxy))FT &&& GFF &= (\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^* MF &&& &\to_\beta^* MF \\ &\to_\beta^* T &&& &\to_\beta^* T \end{align}