Tableaux

Tableaux is an esoteric programming language created by User:ais523 in 2017. It aims to be the equivalent of a "Turing tarpit" for a very high-level model of programming. In particular, it aims to make it possible to write very succinct/simple programs for what are fundamentally very difficult problems, despite having only three commands. Unfortunately, this comes at the cost of incredibly abstract semantics which is hard to implement.

The basic idea

A tableau is basically a quarter-infinite grid of nonnegative integers; alternatively, you can see it as a map from (pairs of nonnegative integers) to nonnegative integers. It can be expressed as a function t for which t(y, x) is the element of the tableau at row y and column x.

The tableaux is an infinite set of these, which obeys two fundamental rules:

1. Arbitrary first column. For any sequence of nonnegative integers, some tableau in the set contains that sequence as its leftmost column. Or to put it another way, for any function f from nonnegative integers to nonnegative integers, there is some t in the set such that t(y, 0) = f(y) no matter the value of y.
2. Prefix-determinism. For any nonnegative integer n, the first n rows in each tableau are determined entirely by the first n entries of its leftmost column. Or to put it another way, for any t, u in the set, if t(y, 0) = u(y, 0) for every y from 0 to n, then t(y, x) = u(y, x) for every y from 0 to n and every nonnegative x.

Execution of a Tableaux program consists of attempting to find some tableaux that obeys the rule above, and also an additional restriction stated by the program.

Expressions

There are three types of expression in Tableaux: nullary, unary, and binary. Each, given a particular tableau, evaluates to a nonnegative integer. Expressions are mostly defined recursively in terms of other expressions. Note that although there are infinitely many expressions, each is only finitely large, i.e. expressions must be well-founded.

• The nullary expression is the base case of expression definition. There is only one such expression, and it evaluates to 0.
• For each expression, there is a corresponding unary expression. It evaluates to 1 + the value that the the original expression evaluates to.
• For each pair of expressions, there is a corresponding binary expression. It evaluates to the element of the tableau at the row given by evaluating the first expression in the pair, and the column given by the second expression in the pair.

A Tableaux program is simply a finite set of pairs of expressions. The program succeeds if some tableaux exists, such that for each tableau in the tableaux, and each pair in the program, evaluating the two elements of the pair over the tableau gives two identical integers.

I/O extension

Tableaux can be expanded to perform batch I/O via designating some input expressions and/or output expressions. Before running the program, the implementation will input a nonnegative integer for each input expression. The program now only succeeds if, for each tableau within the tableaux, each input expression will evaluate (over that tableau) to the value that was input. If the program does succeed, the value of each output expression is evaluated for an arbitrary tableau within the tableaux and output.

Syntax

The set of pairs of expressions is expressed as a list of expressions (the first element of an arbitrary pair, the second element of that pair, the first element of another pair, the second element of that pair, and so on).

In order to help make programs more logically organized, the recommended order in which to list the set elements is "min-y order": the min-y value of an expression or expression-pair is equal to the minimum number of unary expressions that surround the first argument of a binary expression within that expression or expression-pair, and min-y order places expressions with lower min-y values first. For example, if you have a binary expression formed from (a unary expression formed from a nullary expression) and a nullary expression (which would in the readable syntax be written as [1, 0]), its min-y value would be 1. An expression that does not contain a binary expression anywhere has an infinite min-y value. min-y order applies both to the order of expression-pairs in the program and to the order of expressions within an expression-pair.

There are two different syntaxes, a readable syntax and a compressed syntax:

Readable syntax

• A program is represented as a sequence of characters, which are in turn represented as ASCII.
• The nullary expression is represented as 0.
• A unary expression formed from an expression e is represented as +e. This can be run-length-encoded; n+e (with n a decimal integer) represents n unary expressions applied to e. Additionally, n+0 can be further abbreviated to just n.
• A binary expression formed from two expressions e, f is represented as [e,f].
• The two elements of each pair in the program are separated by =. The pairs that make up the program are separated by ;. The program ends with ..
• The program does not have to be in min-y order, although writing it in a different order will produce a compiler warning. You can take advantage of min-y order to make the program more readable; writing @y: will specify that y unary expressions should be added around the first argument of all subsequently appearing binary expressions (this stacks with itself). For example, @2: [1, [0,4]] is equivalent to [3, [2,4]] (except that the scope of the @2: lasts all program).
• When using the I/O extension, an input expression is represented by prefixing a >, and an output expression by prefixing a <. These expressions are listed at the start of the program, separated from each other and the program by ;.
• Whitespace is allowed anywhere except inside a decimal integer used for run-length encoding.
• Comments are also allowed; they run from # to end of line, and are ignored.

Compressed syntax

• A program is represented as a sequence of bits. This can be stored in a file of 8-bit bytes via storing the first 8 bits in the first byte of the file (little-endian), the second 8 bits in the second byte of the file, and so on, padding the program with 0 bits to produce a multiple of 8.
• Numbers are represented as sequences of bits in little-endian base-Fibonacci; they cannot contain two 1s in a row and cannot end in 0, with a 1 in the first position being worth 1, a 1 in the second position being worth 2, a 1 in the third position being worth 3, a 1 in the fourth position being worth 5, a 1 in the fifth position being worth 8, and so on. (Each positive integer has a unique representation of this form.)
• n nested unary expressions surrounding a nullary expression are represented as n+1, followed by the bit sequence 10.
• n nested unary expressions surrounding a binary expression (which in turn is based on a pair e, f) are represented as n+1, followed by the bit sequence 11, followed by the representation of e, followed by the representation of f.
• The program simply lists all the expressions that form it (in the order given above), with no delimiter or the like separating them. (It's always unambiguous where an expression ends.) However, the expressions must be in min-y order. Additionally, if an expression pair appears whose min-y value is not 0, its min-y value is implicitly added to the first argument of all binary expressions for the rest of the program (like the @y: syntax in the readable syntax). Likewise, if the first expression in an expression pair has a min-y value that is not 0, its min-y value is implicitly added to the first argument of all binary expressions within the second expression of the pair.
• When using the I/O extension, a program's input and output expressions are represented as unfinished binary expressions at its end; specifically, an input expression e is represented as 111e, and an output expression f as 0111f.
• No whitespace, comments, or the like are allowed in the compressed syntax.

Examples

Addition

>[1,1]; >[0,1]; <[0,+[1,1]];
+[0, +[1,0]] = [0, 2+[1,0]].

The constraint here causes row 0 of each tableau (apart from its first element) to be an increasing sequence of consecutive integers; the values on row 0 must be constant even if +[1,0] changes (due to the prefix-determinism condition), and yet no matter the value of +[1,0], the cell to the right of (0, +[1,0]) (i.e. (0, 2+[1,0])) must have a value 1 greater (due to the arbitrary first column restriction). This means that for any m, if [0,1] = n, then [0,+m] = m+n. Store m in [1,1], n in [0,1], and we can thus read out m+n from [0,+[1,1]].

In the compressed notation, this program would be 0111 110 0111 0110 110 111 110 00111 0110 110 111 111 0110 0110 111 110 0110 0111 111 110 0111 0110 0110 (whitespace added for readability), i.e. 36 bits for the constraint plus 46 bits for the I/O rules.

Multiplication

>[2,2]; >[2,1]; <[0,+[2,2]];
[0,1] = 0;
[0, +[1,0]] = [1,1]; [0, 2+[1,0]] = [1, +[2,1]];
@1: +[0, +[1,0]] = [0, 2+[1,0]].

First off, look at the last constraint here; it's identical to the addition program above (with a consistent y change). Thus, it's enforcing that [1,+[2,1]] is always equal to [2,1] plus [1,1]. Incidentally, this is the point behind min-y order: it makes it possible to write a structured program via using different y-ranges for different purposes.

Now, we need to constrain row 0 (other than its first element) to be an arithmetic progression with delta [2,1]. In other words, whatever the value of [1,0], we need [0,+[1,0]] plus [2,1] to equal [0,2+[1,0]]. (Note that we need to use [1,0] specifically as the universally quantified variable; if we used [0,0] we could pick a different sequence for each pair of elements that needed to be spaced correctly, and if we used [3,0] the sequence we used for addition wouldn't be able to depend on the numbers we were adding.) We can do this with two constraints: constraining [0, +[1,0]] to equal [1,1], and constraining [1,+[2,1]] to equal [0,2+[1,0]].

We also need to constrain the starting element of this progression. The simplest value to choose is 0, i.e. we constrain [0,1] to equal 0.

Finally, we need to specify the I/O appropriately. [0,1] is [2,1] times 0; [0,2] is [2,1] times 1; [0,3] is [2,1] times 2; and so on. So we need to take an input (storing it arbitrarily in, say, [2,2]; any unused cell outside column 0 would work), then read out the value at [0,+[2,2]].

Test if the input is composite

>[1, 3+[0,2]];
[2, 3+[0,1]] = [1, 2+[2,0]];
@1: [0,1] = 0;
[0, +[1,0]] = [1,1];
@1: +[0, +[1,0]] = [0, 2+[1,0]].

In many languages, testing to see if the input is a composite number would be significantly more complex than multiplying two numbers. In Tableaux, though, the two are almost identical (and in fact, testing for compositeness has simpler I/O). We start by moving the entire data storage down a further line, giving us a new line 0 to work with; then we need to see if we can multiply 2+[0,1] and 2+[0,2] to produce the input. Previously we used [2,1] and [2,2] as arbitrary choices to store the numbers we were multiplying; here, we can just use 2+[0,1] and 2+[0,2] directly. Note that this means that we need to pull [0, 2+[1,0]] = [1, +[2,1]] out of the scope of the first @1 because it's now referring to a value in row 0, meaning that we need to increase the y values by hand, but that isn't a huge issue.

Note that there's no need to store the input in a temporary at all; we can just input into [1, 3+[0,2]] directly.

Test if the input is prime

>[3,1];
[0, [1, 3+[0,0]]] = 1; [0, [3,1]] = 0; [0,1] = 1;
@1: [0,1] = 0;
[0, +[1,0]] = [1,1]; [0, 2+[1,0]] = [1, 3+[0,0]];
@1: +[0, +[1,0]] = [0, 2+[1,0]].

Now, what about inverting that, and testing to see if a number is prime? Just like the compositeness test program, we start with the multiplication program moved down a line. However, this time, instead of multiplying 2+[0,1] and 2+[0,2] (i.e. existentially quantified variables), we're multiplying 2+[0,0] and 2+[1,0] (i.e. universally quantified variables). This means that for each possible composite number, [1, 3+[0,0]] will take on that value in some tableau. Note that this means that we can now move the multiplication back into its original form, as [1,0] is in fact (just about) visible even with an @1: modifier.

Now, we can use a trick to require the input to not match any value of [1, 3+[0,0]]: we can store a 1 in [0, [1, 3+[0,0]]], and a 0 in [0, input] (here, we use [3,1] as a temporary to store the input). Because [0, [3,1]] is locked to equal zero, the program will fail if the input has a value such that it can be produced by multiplying 2+[0,0] and 2+[1,0]. So this program will fail on composite numbers, and succeed on prime numbers.

We're not quite finished: 0 and 1 are neither composite nor prime. The program correctly fails on input 0, because that would require [0,0] to be 0, a requirement which clearly can't hold for all possible values of [0,0]. However, it would succeed on input 1 unless we add another requirement. As such, we finish off the program by unconditionally requiring [0,1] to equal 1, meaning that an input of 1 will be rejected too.

Computational class

The tests for composite and prime numbers can be generalised in a fairly straightforward way to see if an input is a possible value of an arbitrary multivariate polynomial with integer coefficients and nonnegative integer variables. Setting the input to 0 here, we find that Tableaux can solve Diophantine equations, both ways (i.e. we can succeed if and only if they're solvable, or succeed if and only if they're not solvable). This is sufficient power to solve the halting problem for Turing machines, and thus the language is, despite its very simple rules, actually uncomputable.

Implementing Tableaux

In practice, a Tableaux interpreter would have to work by attempting to find a proof that some particular tableaux succeeds, or else that no tableaux can. (Note that because a tableaux is an infinite structure, and there are an infinite number of constraints on it, it's not sufficient to simply give an example; you'd need a proof checker to confirm that the example obeys all the requirements.) At least if running the interpreter on a computable system, it's clear that not all programs can be evaluated as far as success or failure, but many useful programs could be without needing too ridiculous an AI. (In particular, backwards induction seems like a useful technique for determining what value specific cells of the tableaux must have, so the hard step would be collapsing an infinite sequence into closed form; in many cases, though, the sequence will be something very simple like an arithmetic progression.) As such, it seems likely that an interpreter could be written which could handle a sufficiently large set of programs to make the language useful for practically programming in.

Note that one issue with writing an interpreter is that despite being a tarpit, the language is actually capable of some very high-level operations; for example, it can quantify over (countably) infinite sequences. Something like "find a counterexample to the Erdős discrepancy problem" is fairly easy to translate into Tableaux, but almost impossible to express imperatively in terms of low-level constructs.