writing

[N.G. de Bruijn 1972] introduced a way to eliminate names from the syntax of lambda calculus, making it much simpler and “easy to handle in metalingual discussion” and “easy for the computer and for the computer programmer”.

[J. Tromp 2023] incorporated and expanded upon this idea in his Binary Lambda Calculus (BLC) syntax, which also eliminates the notion of significant parentheses and spaces.

BLC makes for a very good binary canonical representation of lambda calculus terms.

In this article I define text-based equivalents which retain the desirable properties of BLC.

Going futher, I propose ways to also remove repetition from the syntax.

I also show how various syntax modifications and variants can be mixed-and-matched and combined to reintroduce human-readability while retaining the ease of processing.

I introduce a loose labeling scheme for lambda calculus syntax variants, with LCλ²τ₀α² denoting the most terse text-based variant of the syntax.

Compare a few well-known combinators:

combinator	conventional	de Bruijn	LCλ2τ0α2
I	λx.x	λ 0	λτ0
K	λx.λy.x	λ λ 1	λ2τ1
U	λx.x x	λ 0 0	λατ0τ0
W	λx.λy.x y y	λ λ 1 0 0	λ2α2τ1τ0τ0
S	λx.λy.λz.x z (y z)	λ λ λ 2 0 (1 0)	λ3α2τ2τ0ατ1τ0
Ω	(λx.x x) (λx.x x)	(λ 0 0) (λ 0 0)	αλατ0τ0λατ0τ0

To get the LCλ²τ₀α² syntax:

1. Eliminate significant parentheses from de Bruijn syntax by changing application to use the prefix-operator α (alpha) instead of juxtaposition.

2. Eliminate significant spaces by transforming each de Bruijn index n into τ_n. E.g.
   • 0 becomes τ₀,
   • 5 becomes τ₅,
   • etc.
3. Use superscripts to run-length encode more than one consecutive lambda and alpha. E.g.:
   • λ λ λ becomes λ³,
   • α α α α α becomes α⁵,
   • etc.

The resulting syntax is effectively Polish notation for lambda calculus, so there are no hidden precedence and associativity rules.

The LCλ²τ₀α² label signifies that the syntax:

• uses λ as the prefix abstraction operator, with run-length encoding (²),
• uses τ as the prefix for de Bruijn indices, indexing from 0 (₀), making it name-free and space-free,
• uses α as the prefix application operator (making it paren-free), with run-length encoding (²).

For an example of how this syntax can be combined with the conventional one, the Y combinator, i.e.:

\[Y = λf.(λx.f (x x)) (λx.f (x x))\]

can be rendered as:

\[\begin{aligned} Y = \lambda_f \alpha \\ & \lambda \alpha \,\tau_f\,(\alpha \tau_0 \tau_0) \\ & \lambda \alpha \,\tau_f\,(\alpha \tau_0 \tau_0) \end{aligned}\]

naming the f variable ($\lambda_f$) and then using $\tau_f$ rather than $\tau_1$ to refer to it. Also, redundant parens and formatting are added for clarity.

The described syntaxes may be useful:

• as a tool of thought,
• for learning and teaching lambda calculus,
• for communicating through papers and articles,
• for use in software such as parsers, generators, translators,
• for handwritten notes.

BTW here is how to encode UWU:

\[UWU = α^2λατ_0τ_0λ^2τ_1τ_0τ_0λατ_0τ_0\]

UWU

References

1. de Bruijn, Nicolaas Govert (1972). “Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem” (PDF). Indagationes Mathematicae. 34: 381–392. ISSN 0019-3577. Archived (PDF) from the original on 2011-05-20.

2. Tromp, John (2023). “Functional Bits: Lambda Calculus based Algorithmic Information Theory” (PDF).