Lambda Calculus - Boolean Algebra

After introducing fundamentals of the lambda calculus in a previous article, along with demonstrations how it can be used for basic arithmetic, the following text has the goal to show how Boolean algebra is expressed in this formal system. Based on the definitions of true and false further basic operations of Boolean algebra can be derived, which then leads to one important aspect in programming: expressing conditionals.

True and False

The foundation for Boolean algebra are the true and false values. As the main building block of lambda calculus is the function, these two values can be represented as the following expressions:

$$ T \equiv \lambda xy.x \newline[0.5em] F \equiv \lambda xy.y $$

The definitions are simple: A function taking two arguments and returning the first one is considered true, while the function taking two arguments and returning the second one is considered false.

These definitions are also known as Church booleans and it is noteworthy that the representation of false is the same as the Church numeral for $0$ (see here).

Operations of Boolean algebra

Boolean algebra works with the operations: $\text{\small AND}$ (conjunction, symbol $\land$), $\text{\small OR}$ (disjunction, symbol $\lor$) and $\text{\small NOT}$ (negation, symbol $\neg$).

AND

The $\text{\small AND}$ operator can be defined as a function taking two arguments:

$$ \land \equiv \lambda xy.xy(\lambda mn.n) \equiv \lambda xy.xyF $$

Without introducing a formal proof that this definitions is correct, it is easily identifiable by looking at what the function does: The $\text{\small AND}$ function returns true if both of its argument can be evaluated to true. Applying the function to two true arguments results in:

$$ \begin{aligned} &\lambda xy.xyF \enspace T \thinspace T \cr &= TTF \cr &= T \end{aligned} $$

The reduction from $TTF$ to $T$ works, because $T$ is a function of two arguments returning the first one. Since in the body of the function the first $T$ function is applied to the two arguments $T$ and $F$ it returns $T$, the true value.

Applying the function to a true and a false value should therefore return false:

$$ \begin{aligned} &\lambda xy.xyF \enspace T \thinspace F \cr &= TFF \cr &= F \end{aligned} $$

OR

The $\text{\small OR}$ operator is defined as a function with two arguments as well:

$$ \lor \equiv \lambda xy.x(\lambda mn.m)y \equiv \lambda xy.xTy $$

It returns true if one of its arguments evaluates to true and to false otherwise.

This can be demonstrated with an example as well:

$$ \begin{aligned} & \lambda xy.xTy \enspace T \thinspace F \cr &= TTF \cr &= T \cr \end{aligned} \newline[0.8em] \begin{aligned} & \lambda xy.xTy \enspace F \thinspace T \cr &= FTT \cr &= T \cr \end{aligned} $$

NOT

The $\text{\small NOT}$ operator is defined as a function with one argument:

$$ \neg \equiv \lambda x.x(\lambda mn.n)(\lambda uv.u) \equiv \lambda x.xFT $$

If this function is applied to $T$ it returns $F$ and $T$ if the argument is $F$:

$$ \begin{aligned} & \lambda x.xFT \enspace T \cr &= TFT \cr &= F \end{aligned} \newline[0.8em] \begin{aligned} & \lambda x.xFT \enspace F \cr &= FFT \cr &= T \end{aligned} $$

Definition of a pair

For the following sections it is required to define the data structure of a pair (a 2-tuple) in terms of the lambda calculus. Using the Church encoding of pairs this can be done as:

$$ \text{\small PAIR} \equiv \lambda xyz.zxy $$

It is therefore defined as a function of three arguments $x$, $y$, $z$, where $z$ is a function applied to $x$ and $y$.

To extract the first and second value of a pair the following lambda expressions are used:

$$ \begin{aligned} \text{\small FIRST} &\equiv \lambda p.p(\lambda xy.x) \equiv \lambda p.pT\cr \text{\small SECOND} &\equiv \lambda p.p(\lambda xy.y) \equiv \lambda p.pF \end{aligned} $$

To give an example:

$$ \begin{aligned} &\text{\small FIRST} \enspace (\text{\small PAIR} \enspace a \thinspace b) \cr &= \lambda p.p(\lambda xy.x) \enspace (\lambda xyz.zxy \enspace a \thinspace b) \cr &= \lambda p.p(\lambda xy.x) \enspace \lambda z.zab \cr &= \lambda z.zab \enspace \lambda xy.x \cr &= Tab \cr &= a \cr[0.8em] &\text{\small SECOND} \enspace (\text{\small PAIR} \enspace a \thinspace b) \cr &= \lambda p.p(\lambda xy.y) \enspace (\lambda xyz.zxy \enspace a \thinspace b) \cr &= \lambda p.p(\lambda xy.y) \enspace \lambda z.zab \cr &= \lambda z.zab \enspace \lambda xy.x \cr &= Fab \cr &= b \end{aligned} $$

Predecessor function

The predecessor function $\text{\small PRED}$ is a function of one argument. It returns the predecessor of the given input as:

$$ \text{\small PRED} \thinspace n = \begin{cases} n-1 &\text{if } n>0 \cr 0 &\text{if } n \leq 0 \end{cases} $$

Among the different ways to define the predecessor function, the method using $\text{\small PAIR}$ seems to be the easiest to understand.

The predecessor function is here described as an operation of picking the first value from a pair $(n, n+1)$. In order to generate this pair the following function can be used:

$$ \Phi \equiv \lambda x.\text{\small PAIR} \thinspace (\text{\small SECOND} \thinspace x) (\text{\small SUCC} \thinspace (\text{\small SECOND} \thinspace x)) $$

This function takes the tuple $(m,n)$ as input and creates the tuple $(n,n+1)$.

$$ \begin{aligned} &\Phi \thinspace (\text{\small PAIR } \thinspace a \thinspace b) \cr &= \Phi \enspace \lambda z.zab \cr &= \text{\small PAIR } \thinspace b \thinspace (\text{\small SUCC } \thinspace b) \cr &\equiv (b, b+1) \end{aligned} $$

The predecessor function itself can then be expressed as:

$$ \text{\small PRED} \equiv \lambda n.\text{\small FIRST}(n \thinspace \Phi \thinspace (\text{\small PAIR} \thinspace 0\thinspace 0)) $$

This is easier to understand with an example:

$$ \begin{aligned} &\text{\small PRED} \enspace 2 \cr &= \text{\small FIRST}(2 \thinspace \Phi \thinspace (\text{\small PAIR} \thinspace 0\thinspace 0))\cr &= \text{\small FIRST}(\Phi(\Phi(\text{\small PAIR}\thinspace 0 \thinspace 0) \cr &= \text{\small FIRST}(1,2) \cr &= 1 \end{aligned} $$

Once again, the Church numerals were used to reduce this lambda expression. Remember: The Church numeral for $2$ is a function with two arguments that applies its first argument two times to the second argument.

Therefore, the predecessor of $0$ in this definition is $0$ as well:

$$ \begin{aligned} &\text{\small PRED} \enspace 0 \cr &= \text{\small FIRST}(0 \thinspace \Phi \thinspace (\text{\small PAIR} \thinspace 0\thinspace 0))\cr &= \text{\small FIRST}(0,0) \cr &= 0 \end{aligned} $$

Subtraction function

The subtraction operator can be defined in terms of the predecessor function.

$$ \text{\small SUB} \equiv \lambda xy.y\thinspace \text{\small PRED}\thinspace x $$

For $x > y$ it yields $x-y$ and $0$ otherwise. This can be demonstrated with:

$$ \begin{aligned} &\text{\small SUB} \thinspace 2\thinspace 1 \cr &= 1\thinspace \text{\small PRED} \thinspace 2 \cr &= (\lambda yx.yx) \thinspace \text{\small PRED} \thinspace 2 \cr &= \text{\small PRED}\thinspace 2 \cr &= 1 \cr[0.8em] &\text{\small SUB} \thinspace 1\thinspace 2 \cr &= 2\thinspace \text{\small PRED} \thinspace 1 \cr &= (\lambda yx.y(yx)) \thinspace \text{\small PRED} \thinspace 1 \cr &= \text{\small PRED}\thinspace (\text{\small PRED}\thinspace 1) \cr &= \text{\small PRED}\thinspace 0 \cr &= 0 \end{aligned} $$

Predicates

Predicates are functions that return a boolean value. Predicates taking one argument are called unary, predicates taking two arguments binary and so forth. Some examples of how to define predicates in terms of lambda calculus are given below.

IS-ZERO

The basic predicate function (abbreviated as $Z$) is the one which tests an input value for the Church numeral $0$:

$$ \begin{aligned} Z &\equiv \lambda x.x(\lambda ab.b)T \cr &\equiv \lambda x.xFT \cr &\equiv \lambda x.xF\neg F \end{aligned} $$

At this point is it necessary to understand that the Church numeral for $0$ is defined as a function $\lambda yx.x$, which is equivalent to $F$. Therefore, $Z$ applied to $0$ yields true:

$$ \begin{aligned} &\lambda x.xFT \enspace 0 \cr &= 0FT \cr &\equiv (\lambda yx.x)FT \cr &= FFT \cr &= T \end{aligned} $$

LESS-OR-EQUAL

The next predicate is a test if the first argument is less or equal to the second:

$$ \text{\small LEQ} \equiv \lambda xy.Z (\text{\small SUB}\thinspace x y) $$

An example testing if $0 \leq 1$ evaluates to:

$$ \begin{aligned} &\text{\small LEQ} \thinspace 0 \thinspace 1 \cr &= Z(\text{\small SUB}\thinspace 0 \thinspace 1) \cr &= Z \thinspace 0 \cr &= T \end{aligned} $$

Another example testing $1 \leq 1$ evaluates to:

$$ \begin{aligned} &\text{\small LEQ} \thinspace 1 \thinspace 1 \cr &= Z(\text{\small SUB}\thinspace 1 \thinspace 1) \cr &= Z(1\thinspace \text{\small PRED}\thinspace 1) \cr &= Z \thinspace (\text{\small PRED}\thinspace 1) \cr &= Z \thinspace 0 \cr &= T \end{aligned} $$

EQUAL

Testing for equality of two arguments can be defined in terms of $\text{\small LEQ}$ using the property that when $x \leq y$ and $y \leq x$ then $x = y$:

$$ \text{\small EQ} \equiv \lambda xy.\land(\text{\small LEQ}\thinspace x \thinspace y)\thinspace (\text{\small LEQ}\thinspace y \thinspace x) $$

GREATER

Testing if a number is greater than another one can be defined in terms of $\text{\small SUB}$: A number is greater than another one if the subtraction of the two gives a non-zero result (please refer back to the definition of $\text{\small SUB}$).

Therefore, the predicate can be defined as:

$$ GT \equiv \lambda xy.\text{\small NOT}\thinspace (Z(\text{\small SUB}\thinspace x \thinspace y)) $$

That can be demonstrated with:

$$ \begin{aligned} &GT \thinspace 2\thinspace 1 \cr &= \lambda xy.\text{\small NOT}\thinspace (Z(\text{\small SUB}\thinspace x \thinspace y)) \enspace 2 \thinspace 1 \cr &= \text{\small NOT}\thinspace (Z(\text{\small SUB}\thinspace 2 \thinspace 1)) \cr &= \text{\small NOT}\thinspace (Z(1)) \cr &= \text{\small NOT}\thinspace (F) \cr &= T \end{aligned} $$

Conditional testing

It is very useful for practical applications of the lambda calculus to be able to express conditionals. That is, doing a different operation when an expression evaluates to true as when it evaluates to false. Something that can be expressed in pseudo-code as:

IF expr = true THEN
  Do_X
ELSE
  Do_Y
ENDIF

This can be expressed in lambda calculus as

$$ \text{\small IF-THEN-ELSE} \equiv \lambda pxy.pxy $$

where $p$ is a predicate function. If it evaluates to true $x$ is returned and $y$ otherwise.

The following example tests if two numbers $n$ and $m$ are equal and returns the predecessor of $n$ if true and the successor of $m$ if false:

$$ \begin{aligned} &(\lambda pxy.pxy) \enspace (\text{\small EQ} \thinspace n \thinspace m) \thinspace (\text{\small PRED} \thinspace n) \thinspace (\text{\small SUCC} \thinspace m) \cr &= \lambda nm.((\text{\small EQ} \thinspace n \thinspace m) \thinspace (\text{\small PRED} \thinspace n) \thinspace (\text{\small SUCC} \thinspace m)) \end{aligned} $$

Applying this function to two equal arguments evaluates to:

$$ \begin{aligned} &\lambda nm.((\text{\small EQ} \thinspace n \thinspace m) \thinspace (\text{\small PRED} \thinspace n) \thinspace (\text{\small SUCC} \thinspace m)) \thinspace 2 \thinspace 2 \cr &= (\text{\small EQ} \thinspace 2 \thinspace 2) \thinspace (\text{\small PRED} \thinspace 2) \thinspace (\text{\small SUCC} \thinspace 2) \cr &= T \thinspace (\text{\small PRED} \thinspace 2) \thinspace (\text{\small SUCC} \thinspace 2) \cr &= \text{\small PRED} \thinspace 2 \cr &= 1 \end{aligned} $$