
\documentclass[12pt]{article}
\usepackage[T2A,OT1]{fontenc}
\usepackage[default]{cantarell}
\usepackage[a4paper, top=20mm, bottom=20mm, left=20mm, right=20mm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage[russian, english]{babel}
\usepackage{tabu}
\usepackage{hyperref}
\usepackage{parskip}
\usepackage{graphicx}
\usepackage{tabularx}
\usepackage[normalem]{ulem}
\usepackage{float}
\floatstyle{boxed}
\restylefloat{figure}
\usepackage{setspace}
\onehalfspacing
\author{Artyom Bologov \href{mailto:lambda-3@aartaka.me}{(email)}}
\date{\today}
\title{Making Sense of Lambda Calculus 3: Truth or Dare With Booleans}
\makeatletter
\def\endenv{\expandafter\end\expandafter{\@currenvir}}
\makeatother
\begin{document}
\maketitle

\paragraph{Timeline of Making Sense of Lambda Calculus} \begin{quote}
\begin{itemize}\item \href{run:lambda-0}{0: Abstration, Reduction, Substitution?}
\item \href{run:lambda-1}{1: Ignorant, Lazy, and Greedy Evaluation}
\item \href{run:lambda-2}{2: Numerous Quirks of Numbers}
\item \href{run:lambda-3}{3: Truth or Dare With Booleans}
\item \href{run:lambda-4}{4: Applicative vs. Normal Order}
\item \href{run:lambda-5}{5: Bring Computation to (Aggregate) Data}
\item \href{run:threading}{Interlude: Functional Threading “Macros”}
\item \href{run:lambda-6}{6: Recurring Problems}
\end{itemize}
\end{quote}

With
\href{run:lambda-2}{numbers} out of the way,
we can finally get to booleans—a simple yet quite atypical topic (at least in its Lambda Calculus rendering).
What I’m used to since my university times is truth tables for boolean ops.
Lambda Calculus (LC) booleans work in an absolutely different way.
Abandon tables ye who enters here.

True and False, the fundamental booleans, are simple:
Just take two things and return the first (true) or second (false).

\begin{figure}[h!]\begin{verbatim}
true = λf.λx.f
false = λf.λx.x
\end{verbatim}\caption{True and false in Lambda Calculus}\end{figure}

Coincidentally, \verb|false| is the same function as 0 and null list (ooops, spoilers!)
Convenient for me as a C programmer used to \verb|0 == NULL == false|.

\section*{Booleans are Branching} \label{branching}

Numbers are
\href{run:lambda-2}{function compositions (section compositions)}.
Akin to that, booleans are computation branching.
Meaning, boolean operations are kind of building trees out of given data.
For example, here’s how
\verb|not| operator looks like in LC:

\begin{figure}[h!]\begin{verbatim}
not = λp.p false true
\end{verbatim}\caption{not operator}\end{figure}

So it takes a boolean and applies it to \verb|false| and \verb|true|.
If the boolean is \verb|true|, then it picks the \verb|false| branch, and vice versa.
A decision tree of sorts.
Some more elegant branching operations, \verb|and| \& \verb|or:|

\begin{figure}[h!]\begin{verbatim}
and = λp.λq.p q p // If p is true, check q
or = λp.λq.p p q // If p is false, check q
// Alternative versions
and = λp.λq.p q false
or = λp.λq.p true q
\end{verbatim}\caption{Basic boolean operators}\end{figure}

Again, branching operations instead of truth tables.

And here’s how
\verb|XOR| looks like:

\begin{figure}[h!]\begin{verbatim}
xor = λp.λq.p (not q) q
\end{verbatim}\caption{XOR in Lambda Calculus}\end{figure}

Simple and smart at the same time.

\section*{Ah, Logic Again} \label{logic}

But if we try to define operations like \verb|nand| or \verb|nor|, our branching doesn’t help much.
Here’s how
\verb|nand| might look like:

\begin{figure}[h!]\begin{verbatim}
nand = λp.λq.p (q false true) true
\end{verbatim}\caption{nand as a branching boolean}\end{figure}

Not too bad, but it totally obviates the meaning of the operation.
It’s just boolean juggling.
The truth tables I’m trying to avoid.
But the good thing about Lambda Calculus is that we can use the functions from before to fix that.
(Well, at least notation-wise—the compiled lambdas won’t have names.
Still, most LC implementations allow for some \verb|let| / \verb|where| syntax, so I’m safe.)
This way derivative operations look much more meaningful:

\begin{figure}[h!]\begin{verbatim}
nand = λp.λq.(not (and p q))
nor = λp.λq.(not (or p q))
xnor = λp.λq.(not (xor p q))
\end{verbatim}\caption{Derivative operations expressed almost like their formulae}\end{figure}

We built our primitives out of branching functions.
And then used them to define derivative operations.
An elegant solution mapping boolean logic directly to LC.
No truth tables, which is a win.
Now to actually using these operations:

\section*{Laconic If} \label{if}

Cutting it short, \verb|if| is:

\begin{figure}[h!]\begin{verbatim}
if = λb.λt.λe.b t e
// Or even
if = λb.b
\end{verbatim}\caption{if conditional}\end{figure}

Booleans already select between branches.
So \verb|if| doesn’t need to do anything: just apply the boolean to both options.
And watch the magic happen.

A person familiar with the regular \verb|if| that chooses and runs only one branch:
“But that’s dangerous: it’s evaluating both branches. There might be side-effects.”
There are no side-effects in LC, though.
And there is no “evaluation” in it either:
\href{run:lambda-0}{only reduction (section reduction)}.
It’s okay.

\section*{Applying Booleans to Numbers} \label{numbers}

That’s the part I’ve been teasing you with in the previous post.
Finally, we can do comparisons and predicates on numbers.
Here’s the most basic—checking for zero:

\begin{figure}[h!]\begin{verbatim}
iszero = λn.n (λx.false) true
\end{verbatim}\caption{Checking a number for zero in LC}\end{figure}

Numbers are applying a function to a value.
If they do apply it even once (number > 0), return \verb|false|.
If they don’t (number = 0), return \verb|true|.
That simple.
And it doesn’t matter if the number is arbitrarily big.
Applying \verb|(λx.false)| has no side-effects (again, there are none in LC).
So we can safely apply it as much as we wish to.

Comparisons, the simplest ones:

\begin{figure}[h!]\begin{verbatim}
leq = λm.λn.iszero (sub m n)
geq = λm.λn.iszero (sub n m)
\end{verbatim}\caption{Less-than-or-equal and greater-than-or-equal predicates}\end{figure}

The number A is greater than another number B if subtracting B from A yield non-zero.
(Notice that Church/Peano numerals are strictly non-negative.
Smallest value subtraction can yield is zero.)
And vice versa.
Having these, other predicates are easy:

\begin{figure}[h!]\begin{verbatim}
gt = λm.λn.not (leq m n)
lt = λm.λn.not (geq m n)
eq = λm.λn.and (leq m n) (leq n m)
\end{verbatim}\caption{Other number predicates}\end{figure}

Maps the mental model perfectly: number A is greater if it’s not less than or equal than B.
And equality (this is slightly tricky) is when the numbers are both less than or equal than each other.
Because if both are, then both must be the same number.
Otherwise one of these will be greater and the condition will be false.

\section*{Finally, Using Booleans!} \label{using}

The simplest example for usage of all these operators might be minimum and maximum functions:

\begin{figure}[h!]\begin{verbatim}
min = λm.λn.if (lt m n) m n
max = λm.λn.if (lt m n) n m
\end{verbatim}\caption{min and max in LC}\end{figure}

I might’ve used
\verb|leq| here, but the behavior stays the same.
It doesn’t matter which of the two we pick—both are valid numbers.
If they are the same number, they are fully
\href{run:lambda-0}{β-equivalent (section equivalence)}
and picking either is fine.
So it does not matter whether there’s
\verb|leq| or \verb|lt|.

\section*{Up Next: Consing Up The World} \label{up-next}

With that, I’m ready to conclude the booleans post.
What happened here was:

\begin{itemize}\item Booleans as decision trees.
\item Branching logic operations.
\item Perfect mapping from logic to LC for derived ops.
\item Number predicates.
\item And, finally, conditional operations on numbers (or any data, really—the idea is the same.)
\end{itemize}

With basic data types, numbers and booleans, one can already encode a lot.
But there’s a point at which one wants aggregate data types.
Like cons trees/lists/structures.
\href{run:lambda-5}{That’s the next post topic},
so byte (sic) your nails until then.
\href{run:lambda-4}{And maybe refresh your normal vs. applicative order knowledge}.


\par\noindent\rule{\textwidth}{0.4pt}
\href{https://creativecommons.org/licenses/by/4.0}{CC-BY 4.0} 2022-2026 by Artyom Bologov (aartaka,)
\href{https://codeberg.org/aartaka/pages/commit/a91befa}{with one commit remixing Claude-generated code}.
Any and all opinions listed here are my own and not representative of my employers; future, past and present.
\end{document}
