I'm trying to define a function that simulates equality between booleans.
To achieve equality operator, I can use the negation operator together with the xor operator, since for two boolean variables $p,q$, it holds that:
$\neg(p\oplus q)=T$ iff $p$ and $q$ have the same value.
If I simplify the above, I get:
$(p\vee\neg q)\wedge(\neg p\vee q)$
Which is the function I want to define.
So first let me start with the definitions, because I'll use them in this post:
$T=\lambda xy.x$
$F=\lambda xy.y$
$\bigvee_{or}=\lambda xy.xTy$
$\bigwedge_{and}=\lambda xy.xyF$
$\neg_{negaion}=\lambda x.xFT$
Now, thanks to @dtldarek I was able to define $(\neg p\vee q)$:
$$\overbrace{\lambda st.
\underbrace{(\lambda x.xFT)s}_\text{negates first arg}Tt}^{\text{represents }\neg p\vee q}=_{\beta}\lambda st.sFTTt$$
and in the same way, I defined $(\neg p\vee q)$:
$$\overbrace{\lambda mn.
mT\underbrace{\Big((\lambda x.xFT)n\Big)}_\text{negates second arg}}^{\text{represents } p\vee \neg q}=_{\beta}\lambda mn.mT(nFT)$$
Which works, I tried it…
Now, applying $\bigwedge_{and}$ operator on these two above functions, I'd expect to get a function that takes two arguments and return $T$ if they are equal and $F$ otherwise, but:
$\big(\lambda xy.xyF\big)\big(\lambda st.sFTTt\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}\big(\lambda y.(\lambda st.sFTTt)yF\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}\big(\lambda y.(\lambda t.yFTTt)F\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}\big(\lambda y.yFTTF\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}(\lambda mn.mt(nFT))FTTF$
There's no need to go further to see that I got an erroneous result, since this last application produces an expression rather than what I need which is a function that gets two arguments…
What did I do wrong?
Best Answer
You need to move the $\lambda$-abstraction of $s$ and $t$ outside: For booleans $s$ and $t$ you have $sFTTt$ representing $(\neg s)\vee t$, $s T (t FT)$ representing $s\vee (\neg t)$ and $s t F$ representing $s\wedge t$. Hence, $((\neg s)\vee t)\wedge (s\vee (\neg t))$ is represented by $(sFTTt)(sT(tFT))F$. The term you're looking for is therefore $\lambda st. (sFTTt)(sT(tFT))F$.
Quick check: $$(\lambda st. (sFTTt)(sT(tFT))F)(TF) =_\beta (TFTTF)(TT(FFT))F =_\beta F T F =_\beta F,\\ (\lambda st. (sFTTt)(sT(tFT))F)(FT) =_\beta (FFTTT)(FT(TFT))F =_\beta T(TFT)F=_\beta TFF=_\beta F\\ (\lambda st. (sFTTt)(sT(tFT))F)(TT) =_\beta (TFTTT)(TT(TFT))F =_\beta TTF=_\beta T\\ (\lambda st. (sFTTt)(sT(tFT))F)(FF) = _\beta (FFTTF)(FT(FFT))F =_\beta T(FFT)F=_\beta FFT=_\beta T$$