\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{float}
\floatstyle{boxed}
\restylefloat{figure}
\usepackage{setspace}
\onehalfspacing
\author{Artyom Bologov \href{mailto:blc-hard@aartaka.me}{(email)}}
\date{\today}
\title{Binary Lambda Calculus is Hard}
\makeatletter
\def\endenv{\expandafter\end\expandafter{\@currenvir}}
\makeatother
\begin{document}
\maketitle

\includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{./assets/blc-hard.png}

So Binary Lambda Calculus (BLC) is this idea.
Encoding Lambda Calculus terms with bits.
For binary transfer or complexity measurement.
John Tromp came up with the idea by joining what was in the air at some point:

\begin{itemize}\item single-argument curried applications
\item single-binding lambdas
\item and de Brujin indices for arguments
\end{itemize}

So one has something like \verb|000000101110110| representing \verb|(lambda (x y f) (f x y))|.
(Or, technically, \verb|(lambda (x) (lambda (y) (lambda (f) ((f x) y))))|, but that’s too wordy.)
These binaries are terse, and thus fun to play with!
John Tromp himself uses BLC to measure complexity of algorithms by how many bits they take.
\href{https://github.com/tromp/AIT/issues/6}{As a fruit of a joint effort, sorting is known to take as little as 300 bits}.
\href{https://rosettacode.org/wiki/Sorting_algorithms/Merge_sort#Binary_Lambda_Calculus}{And sorting without hardcoded predicate is 248 bits}.

And yet Binary Lambda Calculus is hard, in many ways.
Working with it as my current phase crush, I encounter some quirks inherent to it.
And things that were even stopping me from picking it up at some point.
Like the burden of implementation:

\section*{BLC is Hard to Implement: Closures} \label{closures}

It’s called Lambda Calculus for a reason: BLC is just a representation of lambda terms.
BLC semantics are retained from its big sis.
Which means: implementing BLC is implementing closures and call stacks.
\href{run:lambda-1}{Maybe even add laziness as a built-in (section lazy)}?
Most Lambda Calculus “programs” use the
\href{run:lambda-6}{stack-destroying Y combinator (section y)}.
\href{run:lambda-6}{Or even Omega (section omega)}😰
So one has to re-implement them with Z/Z2 etc. or support lazy/call-by-need semantics.

I always thought that using BLC means implementing one’s own interpreter/reduction engine for it.
Why? just a persistent thought.
At some point though, I’ve seen that John Tromp, creator of BLC…
Uses Haskell to run his programs and compiles this Haskell to BLC for code golfing.
So I decided to ease my implementation burden and just use Lisp lambdas as runtime.

\section*{BLC is Hard to Write: Optimization and Compilation} \label{write}

Now, you don’t expect me to write all these ones and zeros by hand?
Not in the binary form either—my Emacs hex editor setup is not yet there.
Given that I already use Lisp runtime for my lambdas,
I’m compiling all my bits from a Lisp-like language too.
(Though it’s more like Scheme, incidentally.)

Opportunities for hand-crafted optimization are inevitably lost in translation.
I need to face that.
I have to

\begin{itemize}\item re-shuffle the order of my Lisp functions,
\item inline some of the utils
\item use \verb|cons| destructuring instead of \verb|cons| accessors (\verb|car|, \verb|cdr|)
\item put locally useful functions closer to their use site
\end{itemize}

Every layer of lambdas adds a bit to every reference to the outside world.
So one has to do this mathematical optimization problem:
put functions where references to them are smallest.
I’m bad at math and optimization problems, but I have a good sense for where
\href{run:cutting-corners}{corners can be cut}.
So I do cut them.

\includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{./assets/blc-hard-lisp.png}

\section*{BLC is Hard to Run: Runtime Implications} \label{runtime}

But okay, writing BLC programs is easier when you compile them from Lisp.
And it removes a whole layer of problems when you have ready-made closures implemented in the language.
So it’s all rainbow pony stairway to heaven now?
No.
Writing functions is not enough, they also have to run in some environment.
At the very least, by taking some input and returning output.

That’s where another “standard” choice lurks awaiting unsuspecting programmers.
BLC I/O, as defined by John Tromp, is a list of bits.
As Church booleans.
Or, in the byte mode, I/O is list of lists of booleans, one list per input byte.

So my beautiful functions sorting Church numerals… won’t work with that.
Whatever function I write, I have to be ready for the runtime to throw raw bits at it.
And I have to make my implementation commit this treachery too!

I did add BLC I/O to my tools.
But I’d better write more ivory tower style programs, not bothering about I/O quirks.
I sort lists of numbers, the rest doesn’t matter.

\section*{BLC is Hard to Scope: Leaky Abstractions} \label{scope}

Now, lists of numbers are not exactly the simplest structure to work with.
\href{run:lambda-2}{Numbers are repeated compositions (section compositions)}.
\href{run:lambda-5}{And lists are cons trees awaiting continuations (section cons)}.
Not really the type of thing C programmer would use.

Binary Lambda Calculus is hard to scope and measure.
Yes, your sorting algo takes 300 bits.
But it bears with it the idea of input.
And the input is Church list of Church lists of booleans.
Every boolean takes 6/7 bits.
Every list adds 6 bits per 6/7 bit element.
So a mere "abc" string takes 200 bits:

\begin{figure}[h!]\begin{verbatim}
01010101010101010100001000001100000110000010000010000010000010000011001010101010101000010000011000001100000100000100000100000110000010010101010101010000100000110000011000001000001000001000001100000110
\end{verbatim}\caption{"abc" the way you’ve never seen it}\end{figure}

200 bits for simple and barely practical input is too much to ignore.
We have to write that in as a cost (paid by a surprised programmer!)
BLC is no longer just an optimal complexity measure.
It’s also the weight of structures and types.

(And I don’t even mention BLC I/O encoding input model, that’d take twice as much space.)

But then, every program implies a certain runtime convention.
Be it \verb|cdecl| or Web browser.
We humans are good at abstracting things and bootstrapping them from nothing.
(In a bloated way.)
So why hoard our bits when they can be used for algorithmic good?
Let’s not.

\section*{BLC is Fun!} \label{use}

So yeah, Binary Lambda Calculus has its weird parts.
But it’s also fun!
Optimizing higher-order functions for bit count.
Deranged stuff, smart talk.
\href{https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861}{So go read on BLC}!
\href{https://codeberg.org/aartaka/cl-blc}{And maybe use cl-blc CLI to write and run some BLC too}!


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