Lambda calculus logical operators

Question

1. Define the and operator in lambda calculus and prove your definition
2. Define the exclusive or operator in lambda calculus, and prove your definition

My answer for #1 is:

AND $\equiv$ $\lambda$x.$\lambda$y.((x y) false)

Because if x is true then it becomes ((true y) false) which reduces to y. Therefore AND will always be true if y=true and false if y=false. However if x is false, then the function is false regardless. Which matches the truth table for logical and.

However, I could not get the logical exclusive or definition, could someone please suggest an idea.

Answer 1

From your explanation for AND I take it that you're working with the usual Church booleans:

$\top = [\lambda x,y. x]$,

$\bot = [\lambda x,y. y]$.

You then define AND using $\bot$ as follows:

$\land = [\lambda x,y.(x~y~\bot)]$,

which, as your correctly assessed, has the desired property of selecting the minimum of x and y.

• When x is $\bot$ we "short-circuit" to $\bot$: $(\land~\bot~\circ) \Rightarrow \bot$, since $(\land~\bot~\circ)$ $\equiv$ $[\lambda x,y(x~y~\bot)](\bot)(\circ)$
  $\rightarrow_{\beta} [\lambda y(\bot~y~\bot)](\circ)$
  $\rightarrow_{\beta} (\bot~(\circ)~\bot) = \bot$.

• When x is $\top$, then we reduce to $y$: $(\land~\top~\circ) \Rightarrow (\circ)$, since $(\land~\top~\circ) \equiv$ $[\lambda x,y(x~y~\bot)](\top)(\circ)$
  $\rightarrow_{\beta}$ $[\lambda y(\top~y~\bot)](\circ)$
  $\rightarrow_{\beta}$ $(\top~(\circ)~\bot) = (\circ)$.

To get exclusive or let's first define $\lnot$, so that we have a functionally complete set of operators:

$\lnot = [\lambda b,x,y. (b~y~x)]$.

Recall what our truth-values $\top,\bot$ do: they take terms $x,y$ and the first returns $x$, the second $y$. Intuitively, $\lnot$ is plausible for it swaps $x$ and $y$, so that $\top$ returns $y$ and $\bot$ returns $x$. Let's check:

• When x is $\top$ we want to get $\bot$. Since $(\lnot \top) \equiv [\lambda b,x,y. (b~y~x)]~([\lambda x,y. x])$
  $\rightarrow_{\alpha}[\lambda b,u,v. (b~v~u)]~([\lambda x,y. x])$
  $\rightarrow_{\beta} [\lambda u,v. (([\lambda x,y. x])~v~u)]$
  $\rightarrow_{\beta} [\lambda u,v. v)]$
  $\rightarrow_{\alpha} [\lambda x,y. y)] = \bot$.

• When x is $\bot$ we want to get $\top$. Since $(\lnot \bot) \equiv [\lambda b,x,y. (b~y~x)]~([\lambda x,y. y])$
  $\rightarrow_{\alpha}[\lambda b,u,v. (b~v~u)]~([\lambda x,y. y])$
  $\rightarrow_{\beta} [\lambda u,v. (([\lambda x,y. y])~v~u)]$
  $\rightarrow_{\beta} [\lambda u,v. u)]$
  $\rightarrow_{\alpha} [\lambda x,y. x)] = \top$.

Using $\land$ and $\lnot$, we can define inclusive or ($\lor$) in the usual way:

$\lor = [\lambda x,y.\lnot(\land~(\lnot x)~(\lnot y))]$.

I'll leave it to you as an exercise to verify that it acts as a disjunction operator. Now exclusive or is:

$\oplus = [\lambda x,y.\land~(\lor~x~y)~(\lnot~(\land~x~y))]$,

which, as is expected, will take terms $x,y$ and return $\top$ if $x\not=y$ and $\bot$ otherwise. I'll let you verify.