Extraordinary Ordinals

Linear

Mackie Parigot

Affine

Scott Bruijn

Non-Linear

Church Mogensen Wadsworth

References

Syntax. Expressionse,b,f,a∷=xVariable∣x⇒bAbstraction∣f←aApplicationVariablesx∈k,x,y,…Numbersn∈0,1,2,… \small\begin{array}{lrcll} \mathrm{Expressions}\quad & e,b,f,a & {\Coloneqq} & x & \quad\mathrm{Variable} \\ & & {\mid} & x\Rightarrow b & \quad\mathrm{Abstraction} \\ & & {\mid} & f\leftarrow a & \quad\mathrm{Application} \\ \mathrm{Variables} & x & {\in} & \mathsf{k}, \mathsf{x}, \mathsf{y}, \dots \\ \mathrm{Numbers} & n & {\in} & 0, 1, 2, \dots \end{array} There are 3 categories—Linear, Affine, and Non-Linear—each having several encodings. Notably, every presented encoding can be used for arithmetic. (all diagrams are drawn by hand in latex+tikz without ai; pow: source, draft notes) Linear Variables xx are names for the edges connecting free vertices. Application. T(k[f←a])\mathcal{T}(k[f\leftarrow a]):

Abstraction. T(k[x⇒b])\mathcal{T}(k[x\Rightarrow b]):

β\beta-reduction. k[(x⇒b)←a] ⊳ k[b{a/x}]k[(x\Rightarrow b)\leftarrow a]\ \rhd\ k[b\{a/x\}]

i.e. xx gets bound to aa, whereas the substituted body bb gets returned to the application’s context.

Mackie Mackie (2019) Definition ⟨0⟩≏x⇒x⟨1⟩≏x⇒x←(x⇒x)⟨2⟩≏x⇒x←(x⇒x)←(x⇒x)⟨3⟩≏x⇒x←(x⇒x)←(x⇒x)←(x⇒x)  ⋮⟨S(n)⟩≏x⇒⟨n⟩←x←(x⇒x) \begin{align*} \braket{0} &\bumpeq \mathsf{x}\Rightarrow \mathsf{x} \\ \braket{1} &\bumpeq \mathsf{x}\Rightarrow \mathsf{x}\leftarrow (\mathsf{x}\Rightarrow \mathsf{x}) \\ \braket{2} &\bumpeq \mathsf{x}\Rightarrow \mathsf{x}\leftarrow (\mathsf{x}\Rightarrow \mathsf{x})\leftarrow (\mathsf{x}\Rightarrow \mathsf{x}) \\ \braket{3} &\bumpeq \mathsf{x}\Rightarrow \mathsf{x}\leftarrow (\mathsf{x}\Rightarrow \mathsf{x})\leftarrow (\mathsf{x}\Rightarrow \mathsf{x})\leftarrow (\mathsf{x}\Rightarrow \mathsf{x}) \\ &\ \,\vdots\\ \braket{S(n)} &\bumpeq \mathsf{x}\Rightarrow \braket{n}\leftarrow \mathsf{x}\leftarrow (\mathsf{x}\Rightarrow \mathsf{x}) \end{align*}

⟨0⟩\braket{0} and ⟨3⟩\braket{3}:

Parigot Parigot

(1989) and Mackie (2019) Definition ⟨0⟩≏z⇒z⟨1⟩≏z⇒s⇒s←z⟨2⟩≏z⇒s⇒s←(s⇒s←z)⟨3⟩≏z⇒s⇒s←(s⇒s←(s⇒s←z))  ⋮⟨S(n)⟩≏z⇒s⇒s←(⟨n⟩←z) \begin{align*} \braket{0} &\bumpeq \mathsf{z}\Rightarrow \mathsf{z} \\ \braket{1} &\bumpeq \mathsf{z}\Rightarrow \mathsf{s}\Rightarrow \mathsf{s}\leftarrow \mathsf{z}\\ \braket{2} &\bumpeq \mathsf{z}\Rightarrow \mathsf{s}\Rightarrow \mathsf{s}\leftarrow(\mathsf{s}\Rightarrow \mathsf{s}\leftarrow \mathsf{z})\\ \braket{3} &\bumpeq \mathsf{z}\Rightarrow \mathsf{s}\Rightarrow \mathsf{s}\leftarrow(\mathsf{s}\Rightarrow \mathsf{s}\leftarrow(\mathsf{s}\Rightarrow \mathsf{s}\leftarrow \mathsf{z}))\\ &\ \,\vdots\\ \braket{S(n)} &\bumpeq \mathsf{z}\Rightarrow \mathsf{s}\Rightarrow \mathsf{s}\leftarrow(\braket{n}\leftarrow \mathsf{z}) \end{align*}

Affine If a variable is not bound, let’s just leave it hanging!

Scott Scott (1963) Definition ⟨0⟩≏s⇒z⇒z⟨1⟩≏s⇒z⇒s←s⇒z⇒z⟨2⟩≏s⇒z⇒s←s⇒z⇒s←s⇒z⇒z⟨3⟩≏s⇒z⇒s←s⇒z⇒s←s⇒z⇒s←s⇒z⇒z  ⋮⟨S(n)⟩≏s⇒z⇒s←⟨n⟩ \begin{align*} \braket{0} &\bumpeq \mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{z} \\ \braket{1} &\bumpeq \mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{z} \\ \braket{2} &\bumpeq \mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{z} \\ \braket{3} &\bumpeq \mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{z}

\\ &\ \,\vdots\\ \braket{S(n)} &\bumpeq \mathsf{s}\Rightarrow\mathsf{z}\Rightarrow\mathsf{s}\leftarrow\braket{n} \end{align*}

Bruijn Borner (2026) Definition ⟨0⟩≏x⇒x⟨1⟩≏x⇒_⇒x⟨2⟩≏x⇒_⇒_⇒x⟨3⟩≏x⇒_⇒_⇒_⇒x  ⋮⟨S(n)⟩≏x⇒_⇒⟨n⟩←x \begin{align*} \braket{0} &\bumpeq \mathsf{x}\Rightarrow \mathsf{x} \\ \braket{1} &\bumpeq \mathsf{x}\Rightarrow \_\Rightarrow \mathsf{x}\\ \braket{2} &\bumpeq \mathsf{x}\Rightarrow \_\Rightarrow \_\Rightarrow \mathsf{x}\\ \braket{3} &\bumpeq \mathsf{x}\Rightarrow \_\Rightarrow \_\Rightarrow \_\Rightarrow \mathsf{x}\\ &\ \,\vdots\\ \braket{S(n)} &\bumpeq \mathsf{x}\Rightarrow \_\Rightarrow \braket{n}\leftarrow \mathsf{x} \end{align*}

Non-Linear If a variable is bound multiple times, let’s duplicate it explicitly! Duplication. T(x)\mathcal{T}(x), with any xx being linearly substituted for xix_i:

(read Asperti and Guerrini (1998) for

more details) Church Church (1932) Definition ⟨0⟩≏s⇒z⇒z⟨1⟩≏s⇒z⇒s←z⟨2⟩≏s⇒z⇒s←(s←z)⟨3⟩≏s⇒z⇒s←(s←(s←z))  ⋮⟨S(n)⟩≏s⇒z⇒s←(⟨n⟩←s←z) \begin{align*} \braket{0} &\bumpeq \mathsf{s}\Rightarrow \mathsf{z}\Rightarrow \mathsf{z} \\ \braket{1} &\bumpeq \mathsf{s}\Rightarrow \mathsf{z}\Rightarrow \mathsf{s}\leftarrow \mathsf{z} \\ \braket{2} &\bumpeq \mathsf{s}\Rightarrow \mathsf{z}\Rightarrow \mathsf{s}\leftarrow (\mathsf{s}\leftarrow \mathsf{z}) \\ \braket{3} &\bumpeq \mathsf{s}\Rightarrow \mathsf{z}\Rightarrow \mathsf{s}\leftarrow (\mathsf{s}\leftarrow (\mathsf{s}\leftarrow \mathsf{z})) \\ &\ \,\vdots\\ \braket{S(n)} &\bumpeq \mathsf{s}\Rightarrow \mathsf{z}\Rightarrow \mathsf{s}\leftarrow (\braket{n}\leftarrow \mathsf{s}\leftarrow \mathsf{z}) \end{align*}

Mogensen Mogensen (2001) Definition Mogensen’s system works for arbitrary bases bb. For example, with b=2b=2, the system is binary. An nn-digit number gets decomposed into dn−1 … d1 d0d_{n-1}\,\dots\,d_1\,d_0 (with dn−1>0d_{n-1}>0): ⟨n⟩b≏z⇒xb−1⇒xb−2⋯⇒x0⇒xd0←(xd1←(…(xdn−1←z)…

))⟨0⟩2≏z⇒i⇒o⇒z⟨1⟩2≏z⇒i⇒o⇒i←z⟨2⟩2≏z⇒i⇒o⇒o←(i←z)⟨3⟩2≏z⇒i⇒o⇒i←(i←z)  ⋮ \begin{align*} \braket{n}_b &\bumpeq \mathsf{z}\Rightarrow\mathsf{x}_{b-1}\Rightarrow\mathsf{x}_{b-2}\dots\Rightarrow\mathsf{x}_0\Rightarrow\mathsf{x}_{d_0}\leftarrow(\mathsf{x}_{d_1}\leftarrow(\dots(\mathsf{x}_{d_{n-1}}\leftarrow\mathsf{z})\dots)) \\ \\ \braket{0}_2 &\bumpeq \mathsf{z}\Rightarrow\mathsf{i}\Rightarrow\mathsf{o}\Rightarrow\mathsf{z} \\ \braket{1}_2 &\bumpeq \mathsf{z}\Rightarrow\mathsf{i}\Rightarrow\mathsf{o}\Rightarrow\mathsf{i}\leftarrow\mathsf{z} \\ \braket{2}_2 &\bumpeq \mathsf{z}\Rightarrow\mathsf{i}\Rightarrow\mathsf{o}\Rightarrow\mathsf{o}\leftarrow(\mathsf{i}\leftarrow\mathsf{z}) \\ \braket{3}_2 &\bumpeq \mathsf{z}\Rightarrow\mathsf{i}\Rightarrow\mathsf{o}\Rightarrow\mathsf{i}\leftarrow(\mathsf{i}\leftarrow\mathsf{z}) \\ &\ \,\vdots\\ \end{align*}

in binary:

challenge: what does the following encode?

Wadsworth Wadsworth (1980) Definition ⟨0⟩≏z⇒z←(K←K)⟨1⟩≏z⇒s1⇒z←(s1←(K←K))←s1⟨2⟩≏z⇒s1⇒s2⇒z←(s1←(s2

←(K←K)))←s1←s2⟨3⟩≏z⇒s1⇒s2⇒s3⇒z←(s1←(s2←(s3←(K←K)))←s1←s2←s3  ⋮⟨S(n)⟩≏z⇒s⇒⟨n⟩←p⇒z←(s←p)←s \begin{align*} \braket{0} &\bumpeq \mathsf{z}\Rightarrow\mathsf{z}\leftarrow(\mathsf{K}\leftarrow\mathsf{K}) \\ \braket{1} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_1\Rightarrow\mathsf{z}\leftarrow(\mathsf{s}_1\leftarrow(\mathsf{K}\leftarrow\mathsf{K}))\leftarrow\mathsf{s}_1 \\ \braket{2} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_1\Rightarrow\mathsf{s}_2\Rightarrow\mathsf{z}\leftarrow(\mathsf{s}_1\leftarrow(\mathsf{s}_2\leftarrow(\mathsf{K}\leftarrow\mathsf{K})))\leftarrow\mathsf{s}_1\leftarrow\mathsf{s}_2 \\ \braket{3} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_1\Rightarrow\mathsf{s}_2\Rightarrow\mathsf{s}_3\Rightarrow\mathsf{z}\leftarrow(\mathsf{s}_1\leftarrow(\mathsf{s}_2\leftarrow(\mathsf{s}_3\leftarrow(\mathsf{K}\leftarrow\mathsf{K})))\leftarrow\mathsf{s}_1\leftarrow\mathsf{s}_2\leftarrow\mathsf{s}_3 \\ &\ \,\vdots\\ \braket{S(n)} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}\Rightarrow\braket{n}\leftarrow\mathsf{p}\Rightarrow\mathsf{z}\leftarrow(\mathsf{s}\leftarrow\mathsf{p})\leftarrow\mathsf{s} \end{align*}

∗ ∗ ∗*\ *\ * Definition

⟨0⟩≏z⇒s0⇒z←s0⟨1⟩≏z⇒s0⇒s1⇒s0←(z←s1)⟨2⟩≏z⇒s0⇒s1⇒s2⇒s0←s1←(z←s2)⟨3⟩≏z⇒s0⇒s1⇒s2⇒s3⇒s0←s1←s2←(z←s3)  ⋮⟨S(n)⟩≏z⇒s0⇒s1⇒⟨n⟩←z←(s0←s1)[1] \begin{align*} \braket{0} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_0\Rightarrow\mathsf{z}\leftarrow\mathsf{s}_0 \\ \braket{1} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_0\Rightarrow\mathsf{s}_1\Rightarrow\mathsf{s}_0\leftarrow(\mathsf{z}\leftarrow\mathsf{s}_1) \\ \braket{2} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_0\Rightarrow\mathsf{s}_1\Rightarrow\mathsf{s}_2\Rightarrow\mathsf{s}_0\leftarrow\mathsf{s}_1\leftarrow(\mathsf{z}\leftarrow\mathsf{s}_2) \\ \braket{3} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_0\Rightarrow\mathsf{s}_1\Rightarrow\mathsf{s}_2\Rightarrow\mathsf{s}_3\Rightarrow\mathsf{s}_0\leftarrow\mathsf{s}_1\leftarrow\mathsf{s}_2\leftarrow(\mathsf{z}\leftarrow\mathsf{s}_3) \\ &\ \,\vdots\\

\braket{S(n)} &\bumpeq \mathsf{z}\Rightarrow\mathsf{s}_0\Rightarrow\mathsf{s}_1\Rightarrow\braket{n}\leftarrow\mathsf{z}\leftarrow(\mathsf{s}_0\leftarrow\mathsf{s}_1)^{[1]} \end{align*} [1]: see note in original paper for successor of ⟨0⟩\braket{0}.

❦❦ Contact me via email. Support on Ko-fi. Subscribe on RSS. Follow on Mastodon. References

Asperti, Andrea, and Stefano Guerrini. 1998. The Optimal Implementation of Functional Programming Languages. Vol. 45. Cambridge University Press.

Church, Alonzo. 1932. “A Set of Postulates for the Foundation of Logic.” Annals of Mathematics 33 (2): 346–66.

Mackie, Ian. 2019. “Linear Numeral Systems.” Journal of Automated Reasoning 63 (4): 887–909.

Mogensen, Torben Æ. 2001. “An Investigation of Compact and Efficient Number Representations in the Pure Lambda Calculus.” In International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 205–13. Springer.

Parigot, Michel. 1989. “On the Representation of Data in Lambda-Calculus.” In International Workshop on Computer Science Logic, 309–21. Springer.

Scott, Dana. 1963. “A System of Functional Abstraction (Lecture Notes).” University of California, Berkeley.

Wadsworth, Christopher. 1980. “Some Unusual λ\lambda-Calculus Numeral Systems.” To HB Curry: Essays on Combinatory Logic, Lambda Calculus; Formalism.