# Defining equality function between booleans in lambda calculus

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?

• 'or' can be simplified to $\lambda xy.xxy$ ; 'and' can be simplified to $\lambda xy.xyx$ ; that should suggest a simpler way of writing equality. Apr 15, 2016 at 0:22

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$$