- Define the and operator in lambda calculus and prove your definition
- 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.
Best Answer
From your explanation for AND I take it that you're working with the usual Church booleans:
You then define AND using $\bot$ as follows:
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:
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:
I'll leave it to you as an exercise to verify that it acts as a disjunction operator. Now exclusive or is:
which, as is expected, will take terms $x,y$ and return $\top$ if $x\not=y$ and $\bot$ otherwise. I'll let you verify.