
\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-2@aartaka.me}{(email)}}
\date{\today}
\title{Making Sense of Lambda Calculus 2: Numerous Quirks of Numbers}
\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-0}{basic terms} and
\href{run:lambda-1}{order of evaluation} out of the way,
we can finally get to practical things.
Like numbers.

Numbers in Lambda Calculus (LC) are usually represented by Church Numerals.
These are usually two-argument functions taking a function and a value.
Numbers apply the function to the value N times and return the result.
Here are some numbers:
\begin{figure}[h!]\begin{verbatim}
0 = λfx.x
1 = λfx.f x
2 = λfx.f (f x)
5 = λfx.f (f (f (f (f x))))
...
\end{verbatim}\caption{Examples of Church Numerals}\end{figure}

There’s also an encoding of numbers with pairs.
But that’s too much overhead for questionable benefit.
So let’s stick with regular Church numerals and see that...

\section*{Numbers Are Compositions} \label{compositions}

This wasn’t immediately clear: numbers are compositions.
A Church numeral is applying a function it’s given a certain number of times.
So you can compose a function with itself by passing it to a number.
Elegant, yet non-obvious.

Imagine you want a function taking the fifth (zero-indexed) element of the linked list.
So you strip off list beginnings five times and then get the fifth element directly.
Implying that \verb|tail| returns the tail of the list and \verb|head| returns the head:
\begin{figure}[h!]\begin{verbatim}
head ((5 tail) list)
head (((λfx.(f (f (f (f (f x)))))) tail) list)
head ((λx.(tail (tail (tail (tail (tail x)))))) list)
head (tail (tail (tail (tail (tail list)))))
\end{verbatim}\caption{Example of numbers as function compositions}\end{figure}

\section*{Successor} \label{succ}

So numbers are clearly compositions.
If we want to increase some number, we can simply take this number and compose another function call on top of it.
That’s the logic of Successor function:
\begin{figure}[h!]\begin{verbatim}
succ = λnfx.f (n f x)
succ 5
succ (λdy.(d (d (d (d (d y)))))) // α-substitution fx -> dy
λfx.f ((λdy.(d (d (d (d (d y)))))) f x)
λfx.f (f (f (f (f (f x))))) // η-reduction
\end{verbatim}\caption{Successor function}\end{figure}

\subsection*{Form-closing Bracket} \label{bracket}

These closing parentheses are getting unruly.
I have to introduce another notational element to handle them.
I’ll use <code>]</code> (as the Interlisp homage) at the end of deeply nested form.
That’ll mean “arbitrary number of closing parentheses”.
The final function in the example above can be rewritten as:
\begin{figure}[h!]\begin{verbatim}
λfx.f (f (f (f (f (f x]
\end{verbatim}\caption{6 in the bracket-terminated form}\end{figure}

Hopefully that’s not too off-putting.

\section*{Addition and Peano Arithmetics} \label{add}

Peano arithmetics—as far as I was able to understand it—
is all about building a complete set of numeric operations out of
constants and successor operator.
It’s also possible to implement these arithmetics in the toolkit Lambda Calculus provides.
Building on the foundations:

\begin{itemize}\item Constants are Church numerals like <code>λfx.f (f (f (f (f (f x]</code>.
\item Successor operation is \verb|succ|.
\item \verb|m+n| Addition is applying \verb|succ| to \verb|m| an \verb|n| number of times.
\item Multiplication is... let’s leave it for later.
\end{itemize}

So here’s how addition formula based on
\href{https://en.wikipedia.org/wiki/Peano_axioms}{Peano axioms}
looks in Lambda Calculus:
\begin{figure}[h!]\begin{verbatim}
// Peano
a + 0 = a
a + S(b) = S(a + b)
// Lambda Calculus:
add = λmn.n succ m,
\end{verbatim}\caption{Translating Peano addition to Lambda Calculus}\end{figure}

While these look quite different, the idea is the same:
apply the successor \verb|n| times to get \verb|n+m|.
Wikipedia page has a good example that I won’t be able to reproduce here.
But, believe me, these are the same.

\section*{Deadly Predecessor & Subtraction} \label{pred-and-sub}

Now what Peano arithmetics don’t cover is subtraction.
There are no negative numbers, so there’s no “subtraction is addition of negative number”.
So we need to somehow strip off some function applications from the number.
The smart piece of code that Wikipedia lists is:
\begin{figure}[h!]\begin{verbatim}
pred = λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
\end{verbatim}\caption{Predecessor function}\end{figure}

Here’s some reduction to show how it works.
Beware: it’s quite overwhelming!
\begin{figure}[h!]\begin{verbatim}
pred 3
(λnfx.n (λgh.h(g f)) (λu.x) (λu.u)) 3
(λnfx.n (λgh.h(g f)) (λu.x) (λu.u)) (λfx.f(f(fx]
λfx.(λgh.h(g f)) ((λgh.h(g f)) ((λgh.h(g f)) (λu.x))) (λu.u)
λfx.(λgh.h(g f)) ((λgh.h(g f)) (λh.h x)) (λu.u)
λfx.(λgh.h(g f)) ((λgh.h(g f)) (λh.h x)) (λu.u)
λfx.(λgh.h(g f)) ((λgh.h(g f)) (λd.d x)) (λu.u)
λfx.(λgh.h(g f)) (λh.h((λd.d x) f)) (λu.u)
λfx.(λgh.h(g f)) (λh.h(f x)) (λu.u)
λfx.(λgh.h(g f)) (λv.v(f x)) (λu.u)
λfx.(λh.h((λv.v(f x)) f)) (λu.u)
λfx.(λh.hf(f x)) (λu.u)
λfx.((λu.u) f(f x))
λfx.f(f x)
\end{verbatim}\caption{Reduction of “pred 3” expression}\end{figure}

Essentially (you probably got it just from looking at it, right?)
what it does is introduce a proxy function that gets passed to the number.
The first application of this function is returning \verb|x|.
And the rest of the applications just apply \verb|f| to it.
So it’s stripping off one innermost call to
\verb|f| from the number.
Scary, but useful.

Now that the predecessor is covered, subtraction is a piece of cake.
The principle is the same as addition: just apply predecessor N times:
\begin{figure}[h!]\begin{verbatim}
sub = λmn.n pred m,
\end{verbatim}\caption{Subtraction function}\end{figure}

Quite elegant...
if we don’t consider the underlying horrors of
\verb|pred|.

\section*{Multiplication and Exponentiation} \label{mult-and-expt}

Multiplication and exponentiation are beautiful in LC.
But they are not necessarily apparent in how they work.
So I’ll try to make some reductions and explain how these make their magic.
Here’s multiplication:
\begin{figure}[h!]\begin{verbatim}
mult = λmnf.m (n f)
\end{verbatim}\caption{Multiplication of m×n in Lambda Calculus}\end{figure}

The idea is clear: take \verb|n|, apply it to \verb|f|, and repeat that \verb|m| times.
But once you squint at it, it unfolds into a series of questions:

\begin{itemize}\item Where is \verb|x| in it? The zero/init/base value, I mean.
\item  How does
\href{"lambda-0#currying"}{currying}
work in there?
\item Is applying one number to another going to be useful?
\end{itemize}

To deepen the feeling of displacement, here’s the exponentiation function:
\begin{figure}[h!]\begin{verbatim}
pow = λbe.e b
\end{verbatim}\caption{Raising b to the power of e in Lambda Calculus}\end{figure}

This is basically this application of one number to another one.
Quite intuitive on the surface.
But it gives me a stack overflow when I try to mentally reduce it.
So here are written reduction to understand \verb|mult| and \verb|pow|:
\begin{figure}[h!]\begin{verbatim}
mult 2 3
(λmnf.m (n f)) 2 3
(λmnf.m (n f)) (λfx.f (f x)) 3
(λmnf.m (n f)) (λfx.f (f x)) (λfx.f (f (f x]
(λnf.(λfx.f (f x)) (n f)) (λfx.f (f (f x]
λf.(λfx.f (f x)) ((λfx.f (f (f x))) f)
λf.(λgy.g (g y)) ((λhz.h (h (h z))) f) // α-substitution
λf.(λgy.g (g y)) (λz.f (f (f z)))
λfy.(λz.f (f (f z))) ((λz.f (f (f z))) y) // NB
λfy.(λz.f (f (f z))) (f (f (f y]
λfy.f (f (f (f (f (f y]
λfx.f (f (f (f (f (f x] // SIX!!!!!
\end{verbatim}\caption{Reduction of multiplication over 2 and 3}\end{figure}

So what happens here is indeed this curried number thing.
\verb|n| is applied to the base value (implied here) \verb|m| times.
The biggest plot twist there is the line marked with \verb|NB|:
the number with \verb|f| being curried inside it is getting applied exactly \verb|m| times.
Which is the same as I said earlier, but now proven by this small reduction
(at least compared to the predecessor one.)
Now the tasty stuff with even more levels of implied currying:
\begin{figure}[h!]\begin{verbatim}
pow 3 2
(λbe.e b) 3 2
(λbe.e b) (λfx.f (f (f x))) 2
(λbe.e b) (λfx.f (f (f x))) (λfx.f (f x))
(λe.e (λfx.f (f (f x))))  (λfx.f (f x))
(λf.λx.f (f x)) (λfx.f (f (f x)))
λx.(λfx.f (f (f x))) ((λfx.f (f (f x))) x)
λx.(λfx.f (f (f x))) ((λfy.f (f (f y))) x) // α-substitution
λx.(λfx.f (f (f x))) (λy.x (x (x y))) // NB
λx.(λfz.f (f (f z))) (λy.x (x (x y))) // α-substitution
λxz.(λy.x (x (x y))) ((λy.x (x (x y))) ((λy.x (x (x y))) z))
λxz.(λy.x (x (x y))) ((λy.x (x (x y))) (x (x (x z)))
λxz.(λy.x (x (x y))) (x (x (x (x (x (x z]
λxz.x (x (x (x (x (x (x (x (x z]
λfz.f (f (f (f (f (f (f (f (f z]  // α-substitution
λfx.f (f (f (f (f (f (f (f (f x]  // α-substitution
λfx.f (f (f (f (f (f (f (f (f x] // NINE!!!
\end{verbatim}\caption{Reduction of exponentiation of 3 by 2}\end{figure}

Now what happens here, especially on the line marked with \verb|NB|, is a crime.
Crime against static type systems and fundamentalist minds.
The value that’s supposed to be a base/zero/init value...
Is used as a function.
This makes Lambda Calculus both more cryptic and beautiful:

\begin{itemize}\item Functions are all there is to LC.
\item  Even the ones supposed to be scalar values.
\item  Even the ones supposed to be “functions”.
\item  And even the ones that oscillate between the two!
\end{itemize}

This is a takeaway that the exponentiation reduction refreshed in my mind:
(After all, it’s been almost 4 months since the last Making Sense of Lambda Calculus post.)
Don’t be afraid to break the supposed contract your lambdas are establishing.
They are just that: lambdas.
Nothing else.

But there are cases when even the smart currying,
re-interpretation of data as functions and vice versa,
and other arcane stuff doesn’t help.
Like division:

\section*{Is There Division?} \label{div}

Division is always a problem.
It’s not following many rules that addition and multiplication establish.
And there’s a whole page on
\href{https://en.wikipedia.org/wiki/Division_algorithm}{division algorithms}
on Wikipedia.

The simplest algo is the subtraction-based one.
Basically subtracting the denominator from the numerator until it’s below the denominator.
Here’s how
\href{https://github.com/aartaka/stdlambda}{stdlambda}
implementation of division works:
\begin{figure}[h!]\begin{verbatim}
div = λnd.Y (λr.λq.(lt q d) 0 (succ (r (- q d)))) n
\end{verbatim}\caption{Division implementation based on recursive subtration}\end{figure}

A lot of things there:

\begin{description}\item[Y]
Y combinator for recursion on \verb|r|
\item[lt]
Less than function working as a termination condition.
\item[succ]
Successor function from above.
\item[sub]
Subtraction.
\end{description}

Putting it all together:

\begin{itemize}\item Apply the function to numerator (\verb|n|) and denominator (\verb|d|)
\item  If the quotient (\verb|q|, numerator initially) is less than the denominator, then return 0.
\item  Otherwise, subtract the denominator from the quotient and recurse.
\item  Add one to the recursive call result every time we subtract the denominator.
\item  Once the recursion terminates, 0 turns into the number of denominator subtractions.
\item  Which is basically what a division is.
\end{itemize}

And yes, that’s the simplest implementation I can think of.
No elegant stuff like applying numbers to each other.
\href{https://justine.lol/lambda/}{Justine Tunney lists a division function in her “Lambda Calculus in 383 Bytes”},
but I was not able to decipher how it works.
I’m stuck with advanced things like Y combinator for the seemingly simple operation: division.

\section*{Up Next: Truth or Dare With Booleans} \label{up-next}

Summarizing all of the above:

\begin{itemize}\item Numbers are compositions.
\item  Increasing them is a matter of composing yet another function on top.
\item  Decreasing / subtracting them is... complicated.
\item  Multiplication and exponentiation are beautiful.
\item  While division is... complicated.
\end{itemize}

One type of numeric operations that I haven’t mentioned is comparisons.
Because comparisons get us into the uncharted lands of booleans.
Reviewing booleans is a big topic beyond this (already huge) post.
So booleans come next, in Making Sense of Lambda Calculus 3!


\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}
