[Math] Lambda calculus logical operators

lambda-calculus

  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.

Best Answer

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.

Related Question