Unary Combinatory Logic

Marvin Borner

2023-10-06

Jot (/dʒɑt/) was created by Chris Barker as a 2-symbol (binary) encoding of iota combinators. It’s described as “a better Gödel-numbering” and, using SKI combinators, has a map to lambda calculus; it’s therefore a Turing complete programming language.

Since 2 symbols are clearly too many for any programming language, I derived a 1 symbol (unary) variant of Jot called Jottary.

And yes, theoretically you could easily convert any binary encoding of computation to a unary representation – this one has some fun evaluation techniques though!

Translation

The SKI combinator calculus consists of three combinators and the normal application notation:

Σ= {s,k,i} {(MN)MΣNΣ} \begin{align*} \Sigma=\ &\{\texttt{s}, \texttt{k}, \texttt{i}\}\\ \cup\ &\{\texttt{(}MN\texttt{)}\mid M\in\Sigma\land N\in\Sigma\} \end{align*}

Jot is defined by the translation function τι:{0,1}Σ\tau_\iota:\{\texttt{0},\texttt{1}\}^*\to\Sigma

τι(ε)=iτι(M0)=((τι(M)s)k)τι(M1)=(s(kτι(M))) \begin{align*} \tau_\iota(\varepsilon)&=\texttt{i}\\ \tau_\iota(M\texttt{0})&=\texttt{((}\tau_\iota(M)\texttt{s)k)}\\ \tau_\iota(M\texttt{1})&=\texttt{(s(k}\tau_\iota(M)\texttt{))} \end{align*}

Since Jot only consists of ones and zeroes, you can create a decimal version of any Jot program. You first prepend a 1, convert the bitstring to decimal, and finally subtract 11. Creating the unary variant Jottary then just consists of repeating the symbol σ\sigma as described by the translation function τσ:{0,1}{σ}\tau_\sigma:\{\texttt{0},\texttt{1}\}^*\to\{\sigma\}^*

τσ(b)=σdec(1b)1.\tau_\sigma(b)=\sigma^{\mathrm{dec}(\texttt{1}b)-1}.

With σ=1\sigma=\texttt{1}, this results in the following equivalencies:

εσειi1σ0ι((is)k)11σ1ι(s(ki))111σ00ι((((is)k)s)k)1111σ01ι(s(k((is)k)))11111σ10ι(((s(ki))s)k)111111σ11ι(s(k(s(ki)))) \begin{alignat*}{2} \varepsilon_\sigma&\equiv\varepsilon_\iota&&\equiv\texttt{i}\\ \texttt{1}_\sigma&\equiv\texttt{0}_\iota&&\equiv\texttt{((is)k)}\\ \texttt{11}_\sigma&\equiv\texttt{1}_\iota&&\equiv\texttt{(s(ki))}\\ \texttt{111}_\sigma&\equiv\texttt{00}_\iota&&\equiv\texttt{((((is)k)s)k)}\\ \texttt{1111}_\sigma&\equiv\texttt{01}_\iota&&\equiv\texttt{(s(k((is)k)))}\\ \texttt{11111}_\sigma&\equiv\texttt{10}_\iota&&\equiv\texttt{(((s(ki))s)k)}\\ \texttt{111111}_\sigma&\equiv\texttt{11}_\iota&&\equiv\texttt{(s(k(s(ki))))}\\ & &&\vdots \end{alignat*}

Evaluation

There are several ways to evaluate Jottary. The goal here is to somehow convert to lambda calculus for beta reduction; while reducing SKI combinators directly is also possible, I personally prefer beta reduction by converting to lambda calculus first.

The boring way would then be to translate the program to Jot first, then to SKI combinators, then to lambda calculus, and finally reduce it.

A slightly better solution would be to use dynamic programming to convert to SKI combinators directly. η:{σ}Σ\eta:\{\sigma\}^*\to\Sigma

η(ε)=iη(1112n)=(s(kη(1n1)))η(1112n+1)=((η(1n)s)k) \begin{align*} \eta(\varepsilon)&=\texttt{i}\\ \eta(\texttt{1}_1\dots\texttt{1}_{2n})&=\texttt{(s(k}\eta(\texttt{1}^{n-1})\texttt{))}\\ \eta(\texttt{1}_1\dots\texttt{1}_{2n+1})&=\texttt{((}\eta(\texttt{1}^{n})\texttt{s)k)} \end{align*}

The most beautiful solution, however, would be a direct translation to lambda calculus – skipping the final intermediate step. And, because why not, let’s do the translation to lambda calculus in pure lambda calculus!

To do this, I used my bruijn programming language since it has a big library of lambda calculus functions. The following program serves as a full parser and evaluator of Jottary:

:import std/Combinator .
:import std/List .
:import std/Monad .
:import std/Number .

go [eval-r (<~>((concat gen) !! 0) ; i)]
    gen (\replicate-m (l : {}r)) <$> (iterate ++ (+0))
        l [(0 s) k]
        r [s (k 0)]

main go  length

go accepts a number (the length of the unary string) and returns the respective lambda calculus code. It works by first generating an ordered list of all combinations of left/right iota applications; it uses the monadic replicate-m and an infinite numbered list (iterate). The combinations then get lazily1 indexed by the argument (Number), before getting concatenated with i and, finally, right-associatively evaluated. Since the l/r repeatedly get inserted into each other, the final application of i fills the last remaining hole 0 and thus makes the evaluator Jot/Jottary/Turing-complete!

Note that every function/operator/type used is implemented 100% in pure lambda calculus: It uses Church lists, Mogensen ternary numerals, Tromp-inspired monads, …. You can find more information about the functions in the code (e.g. by clicking on the imports above).

While the code could definitely be optimized (for example by using a different generator), it’s not even that slow! For example, evaluating the Jottary 1503\texttt{1}^{503} (aka Jot 11111000, the s combinator):

$ hyperfine "printf '1%.0s' {1..503} | bruijn -y jottary.bruijn"
    Time (mean ± σ):     756.4 ms ±  35.2 ms    [User: 1816.9 ms, System: 1735.2 ms]
    Range (min … max):   706.9 ms … 808.2 ms    10 runs

A self-hosting evaluator on the other hand, would be very slow (if even practically possible). Theoretically converting jottary.bruijn to BLC (541B), to SKI, to Jot (2.4KB), and finally to Jottary, would result in around 2200002^{20000}B.

You can find the bruijn program here. I also wrote an evaluator and transpiler in Haskell here.

* * *

I actually hoped I would be able to find a better algorithm for direct evaluation, but all my attempts (e.g. by using Church numerals or other more “native” logic) failed or had immense space complexity. So please let me know if you found other techniques! I also asked a question on math stackexchange about creating a unary base that does not require arbitrary associativity, but works with strictly alternating associative syntax – I have not yet received an answer.

Thanks for reading. Suggest improvements or fixes via email. Support on Ko-fi.

动态网自由门 天安門 天安门 法輪功 李洪志 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 劉曉波动态网自由门


Imprint · AI Statement · RSS