4
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ '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. $\endgroup$
    – DanielV
    Apr 15, 2016 at 0:22

1 Answer 1

3
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ @so.very.tired: Does this help? $\endgroup$
    – Hanno
    Feb 10, 2015 at 19:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.