Extraordinary Ordinals

# Extraordinary Ordinals Source: [https://text.marvinborner.de/2026-04-09-17.html](https://text.marvinborner.de/2026-04-09-17.html) - [Linear](https://text.marvinborner.de/2026-04-09-17.html#linear)- [Mackie](https://text.marvinborner.de/2026-04-09-17.html#mackie) - [Parigot](https://text.marvinborner.de/2026-04-09-17.html#parigot) - [Affine](https://text.marvinborner.de/2026-04-09-17.html#affine)- [Scott](https://text.marvinborner.de/2026-04-09-17.html#scott) - [Bruijn](https://text.marvinborner.de/2026-04-09-17.html#bruijn) - [Non\-Linear](https://text.marvinborner.de/2026-04-09-17.html#non-linear)- [Church](https://text.marvinborner.de/2026-04-09-17.html#church) - [Mogensen](https://text.marvinborner.de/2026-04-09-17.html#mogensen) - [Wadsworth](https://text.marvinborner.de/2026-04-09-17.html#wadsworth) - [References](https://text.marvinborner.de/2026-04-09-17.html#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](https://text.marvinborner.de/res/strdig/2026-04-09-17.tex),[draft notes](https://text.marvinborner.de/res/notes/numeral_graph_encodings.pdf)\) ## Linear *Variables*xxare 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\.*xxgets bound toaa, whereas the substituted bodybbgets returned to the application’s context\. ## Mackie [Mackie \(2019\)](https://text.marvinborner.de/2026-04-09-17.html#ref-mackie2019linear) 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\)](https://text.marvinborner.de/2026-04-09-17.html#ref-parigot1989representation)and[Mackie \(2019\)](https://text.marvinborner.de/2026-04-09-17.html#ref-mackie2019linear) 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\)](https://text.marvinborner.de/2026-04-09-17.html#ref-scott1963func) 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\)](https://text.marvinborner.de/2023-08-22-22.html) 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 anyxxbeing linearly substituted forxix\_i:  \(read[Asperti and Guerrini \(1998\)](https://text.marvinborner.de/2026-04-09-17.html#ref-asperti1998optimal)for more details\) ## Church [Church \(1932\)](https://text.marvinborner.de/2026-04-09-17.html#ref-church1932set) 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\)](https://text.marvinborner.de/2026-04-09-17.html#ref-mogensen2001investigation) DefinitionMogensen’s system works for arbitrary basesbb\. For example, withb=2b=2, the system is*binary*\. Annn\-digit number gets decomposed intodn−1…d1d0d\_\{n\-1\}\\,\\dots\\,d\_1\\,d\_0\(withdn−1\>0d\_\{n\-1\}\>0\): ⟨n⟩b≏z⇒xb−1⇒xb−2⋯⇒x0⇒xd0←\(xd1←\(…\(xdn−1←\)…\)\)⟨0⟩2≏z⇒i⇒o⇒z⟨1⟩2≏z⇒i⇒o⇒i←z⟨2⟩2≏z⇒i⇒o⇒i←\(o←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\)\\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\{i\}\\leftarrow\(\\mathsf\{o\}\\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\)](https://text.marvinborner.de/2026-04-09-17.html#ref-wadsworth1980some) 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](https://text.marvinborner.de/mail)\. Support on[Ko\-fi](https://ko-fi.com/marvinborner)\. Subscribe on[RSS](https://text.marvinborner.de/feed.rss)\. Follow on[Mastodon](https://types.pl/@marvin)\. ## 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\. 动态网自由门 天安門 天安门 法輪功 李洪志 Free Tibet 六四天安門事件 The Tiananmen Square protests of 1989 天安門大屠殺 The Tiananmen Square Massacre 反右派鬥爭 The Anti\-Rightist Struggle 大躍進政策 The Great Leap Forward 文化大革命 The Great Proletarian Cultural Revolution 人權 Human Rights 民運 Democratization 自由 Freedom 獨立 Independence 多黨制 Multi\-party system 台灣 臺灣 Taiwan Formosa 中華民國 Republic of China 西藏 土伯特 唐古特 Tibet 達賴喇嘛 Dalai Lama 法輪功 Falun Dafa 新疆維吾爾自治區 The Xinjiang Uyghur Autonomous Region 諾貝爾和平獎 Nobel Peace Prize 劉暁波 Liu Xiaobo 民主 言論 思想 反共 反革命 抗議 運動 騷亂 暴亂 騷擾 擾亂 抗暴 平反 維權 示威游行 李洪志 法輪大法 大法弟子 強制斷種 強制堕胎 民族淨化 人體實驗 肅清 胡耀邦 趙紫陽 魏京生 王丹 還政於民 和平演變 激流中國 北京之春 大紀元時報 九評論共産黨 獨裁 專制 壓制 統一 監視 鎮壓 迫害 侵略 掠奪 破壞 拷問 屠殺 活摘器官 誘拐 買賣人口 遊進 走私 毒品 賣淫 春畫 賭博 六合彩 天安門 天安门 法輪功 李洪志 Winnie the Pooh 劉曉波动态网自由门 ---