Jot
| Designed by | Chris Barker |
|---|---|
| Appeared in | 2001 |
| Computational class | Turing-complete |
| Reference implementation | Bracket abstraction to lambda calculus |
| Influenced by | Iota, lambda calculus, combinatory logic |
Jot (pronounced /dʒɑt/) is a Turing tarpit originally described as "a better Gödel-numbering" than its sister language Iota. Every binary sequence is a valid Jot program, including the empty sequence as the null program; nonetheless, Jot exhibits Turing-complete behavior.
Syntax
Jot is the trivial regular language recognizing possibly-empty sequences of bits:
Jot ::= (0|1)*
Semantics
Jot was originally defined via the following bracket abstraction which converts the Jot program F to lambda calculus. The bracket [F] moves from right to left, parsing bits.
[] -> λx.x [F0] -> [F](λx.λy.λz.(xz)(yz))(λx.λy.x) [F1] -> λx.λy.[F](xy)
Note that almost all of these are combinators.
I = λx.x K = λx.λy.x S = λx.λy.λz.(xz)(yz)
We can interpret this as a formal grammar, specifically a nondeterministic context-free grammar.
- F → I
- F → F(S)(K)
- F → λx.λy.F(xy)
This grammar generates the language of Jot programs decoded into lambda calculus. If we interpret this as producing a derivation tree, then at each step we can take one of three paths; apply (right), nest (left), or end (center). If we assign apply/right to 0, nest/left to 1, and end/center to end of input, then we can label all derivation paths uniquely with a binary number. The number of a path is identical to the corresponding Jot program for the derived lambda calculus program, with the bits reversed.
Computational class
Barker gives the following bracket {X} mapping combinators X from combinatory logic to Jot via the Turing-complete SK basis.
{K} -> 11100
{S} -> 11111000
{AB} -> 1{A}{B}
We can compose this bracket with [F] to translate any expression from combinatory logic to lambda calculus. This shows that, while Jot may be a trivial language in terms of membership, it is computationally universal:
Theorem (Turing-completeness). It is undecidable whether lambda expressions in the image of F have a normal form. (Barker, 2001)
Further, Jot may be used as a Gödel encoding since the image of F is universal and Jot programs are merely numbers written in binary. To make this work, note that Barker's bracket {X} will always generate programs without leading zeros, and there is only one way to write a natural number in binary without leading zeros. Therefore:
Theorem (Gödel numbering). Jot programs without leading zeros are in bijection with the natural numbers and represent effectively computable functions. (Barker, 2001)
Note that there can be more efficient encodings. For example, given the I combinator, the empty program technically does not have leading zeros:
{I} ->
So this rule can be added to Barker's bracket to create a valid Gödel numbering for the SKI basis.
Related languages
- Iota, Jot's sister language described in the same article
- Binary combinatory logic, a binary language for the SK basis
- Zot, Jot with I/O
- Jottary, unary variant of Jot