In our previous article, we showed how the numbers are represented in lambda calculus.

The purpose of this article is to show how we represent boolean values in lambda calculus. And to show the code of the basic boolean operations: negation, conjunction and disjunction a.k.a `not`, `and` and `or`.

We are using `clojure` for the code snippets - as it belongs to the `LISP` family, and `LISP` is founded on top of lambda calculus. # Setup

All the code snippets on this article are live and interactive: feel free to modify the code and it will evaluate instantaneously!

First, let’s create a namespace for our journey, and `refer` the `disp` macro, from the gadjett repository on github:

``````
(ns lambda.boolean-algebra
```
```

More about the `disp` macro in this article

In order to load code from a github repository, we use `data-external-libs` attribute on the code snippet as explained here.

# Definition of true and false

Here is how we define `T` (`true`) and `F` (`false`) in lambda calculus:

``````(defn T [x]
(fn [y] x))

(defn F [x]
(fn [y] y))
``````

You can see `T` as a 2-arity function that returns the first argument and `F` as a 2-arity function that returns the second argument.

As we did with numerals, we can view a lambda boolean by passing to it `T` and `F`. Like this

``````(defn view-bool [bool]
((bool "T") "F"))
``````

And it works as expected: `T` returns `"T"`

``````(view-bool T)
``````

and `F` returns `"F"`:

``````(view-bool F)
``````

As we did in Numbers and Arithmetics with functions only: lambda calculus live tutorial., we are going to define the `Lambda` type to make the visualisation and comparison of the lambda booleans more convenient.

``````
(deftype Lambda [f]
Object
(toString [_] (str (view-bool f)))

IPrintWithWriter
(-pr-writer [this writer _] (-write writer (str (view-bool f))))

IEquiv
(-equiv [this other]
(= (view-bool this) (view-bool other)))

IFn
(-invoke [this g]
(f g)))

``````

(Check here for an explanation about the code of the `Lambda` type.)

Now, let’s redefine `T` and `F` using `Lambda` type:

``````(def T (Lambda.
(fn [x]
(fn [y] x))))
(def F (Lambda.
(fn [x]
(fn [y] y))))
``````

Now, the lambda booleans are viewed properly:

``````[T F T T F T]
``````

They are invokable as functions:

``````((T T) F)
``````

and they are comparable:

``````(= ((T T) F) F)
``````

Now, we are going to build the basic boolean operations, using the definition of `T` and `F`: In a nutshell, `T` returns the first argument and `F` returns the second argument.

Keep in mind that in boolean algebra, the operations are defined by their truth tables:

x y negation(x) conjunction(x, y) disjunction(x, y)
T T F T T
T F T F T
F F   F F
F T   F T

# Negation

``````(defn negation [x]
(Lambda.
((x F) T)))
``````

Basically, what this code says is: if `x` is `T` then return the first argument - which is `F`. And if `x` is `F` then return the second argument - which is `T`. This is exactly what the `negation` is supposed to do.

Let’s check that `negation` respects the truth table:

``````(disp
(negation T)
(negation F))
``````

In real lambda calculus, we cannot name things, so the real implementation of `negation` is:

``````(defn negation-lambda [x]
(Lambda.
((x (fn [x]
(fn [y] y))) (fn [x]
(fn [y] x)))))
``````

It works exactly the same as `negation`:

``````(disp
(negation-lambda T)
(negation-lambda F))
``````

But it is is much less readable.

From now on, we will use names to make our code readable and we will keep in the back on our mind that in real lambda calculus there are no names.

You might wondering how we are going to implement recursions in a language with no names?

We will answer that in another article, when we present the `Y-combinator`.

Back to our boolean operations…

# Conjunction

``````(defn conjunction [x]
(Lambda.
(fn [y]
(Lambda. ((x y) F)))))
``````

Basically, this code says: if `x` is `T` return `y` else return `F`. This is exactly the definition of the conjunction in logic.

Let’s check that `conjunction` respects the truth table:

``````(disp ((conjunction T) T)
((conjunction T) F)
((conjunction F) F)
((conjunction F) T))
``````

# Disjunction

``````(defn disjunction [x]
(Lambda.
(fn [y]
(Lambda. ((x T) y)))))
``````

Basically, this code says: if `x` is `T` return `T` else return `y`. This is exactly the definition of the disjunction in logic.

Let’s check that `conjunction` respects the truth table:

``````(disp ((disjunction T) T)
((disjunction T) F)
((disjunction F) F)
((disjunction F) T))
``````