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:

$$\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 $\tau_\iota:\{\texttt{0},\texttt{1}\}^*\to\Sigma$

$$\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 $1$. Creating the unary variant Jottary then just consists of repeating the symbol $\sigma$ as described by the translation function $\tau_\sigma:\{\texttt{0},\texttt{1}\}^*\to\{\sigma\}^*$

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

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

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

$$\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 lazily¹ 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 $\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 $2^{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.