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!

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*}$

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^{1} 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.