Not-Quite-Laconic

Not-Quite-Laconic

Designed by	Stefan O'Rear
Appeared in	2016
Computational class	Turing-complete
Major implementations	[1]
Influenced by	Laconic
File extension(s)	.nql

Not-Quite-Laconic, or NQL, is a slight modification of Laconic with a different compilation strategy. The design goal of NQL is to provide a similar experience to Laconic but with much smaller compiled programs. It was introduced in 2016 following the original announcement of Laconic.

NQL behaves like a register machine over natural numbers. Instead of compiling to Minsky machines, it is intended to compile to Turing machines.

Overview

A NQL program consists of two sorts of top-level declarations, globals and procedures. Globals declare storage and procedures declare actions.

Globals

A global name is a location which stores a natural number. Globals are introduced with the global keyword.

global g;

Procedures

A procedure is a unit of code. Procedures are used both to organize the overall control-flow of the program and to factor out common code to reduce program size.

Procedure arguments are passed by reference. That is, when calling a procedure with a global, the global's name/location is passed instead of its value. For example, the following procedure sets a global to zero:

proc zero(x) { x = 0; }

In addition to assignments, there are if-statements and while-statements. For example, the following procedure computes x % y = z:

proc modulus(x, y, z) {
    z = x;
    while (z >= y) { z = z - y; }
}

There is only one non-local control statement, return;. There is also a single dispatch statement, switch with fallthrough. The break; keyword ends a switch but is not legal for leaving a while-loop early.

NQL requires a main procedure. The main procedure will be executed repeatedly forever, but if it returns then the machine will halt. Therefore the shortest legal halting NQL program is:

proc main() { return; }

While the overall shortest legal program does not halt:

proc main() {}

Arithmetic

A statement assigns the result of an arithmetic expression to a global. Available arithmetic includes literal natural numbers, looking up the current value of a global, addition, monus (truncated subtraction), multiplication, and division. For example, a global can be incremented:

g = g + 1;

Comparisons

An if- or while-statement is conditional upon the result of a Boolean expression which compares globals to other globals or literal natural numbers. The total-ordering operators are supported (less-than, greater-than, equal) and standard Boolean operators (AND, OR, NOT). Unlike languages like Python, comparisons cannot be chained; for example, to require that three globals are ordered with x <= y <= z two clauses must be conjoined:

if (x <= y && y <= z) { ordered(); }

Complexity class

NQL is Turing-complete. In particular:

Theorem (Halting). It is not decidable whether an NQL program will halt.

The general insight is that NQL can easily encode a Diophantine equation over natural numbers and search for elements of a corresponding Diophantine set. It can also encode a search for statements in a proof system with some property. Such programs roughly look like:

global x;
global hasProperty;
proc main() {
    x = 0;
    while (true) {
        checkForProperty(x, hasProperty);
        if (hasProperty == 1) { return; }
        x = x + 1;
    }
}

From there, it is possible to search for answers to open problems in mathematics by writing NQL programs. The size of the NQL program can be used to analyze the busy-beaver problem by forcing an arithmetic theory to search for its own contradictions. Concretely, the set theory ZFC cannot construct every busy beaver number.

Construction. There is a 748-state 2-symbol Turing machine which halts if and only if ZFC proves ~Con(ZFC). (O'Rear, 2016)

If ZFC is consistent then ZFC does not prove that O'Rear's machine does not halt. Also, if ZFC is consistent then O'Rear's machine does not halt. Finally, if ZFC is consistent then ZFC does not prove that O'Rear's machine halts after some finite number of steps. In summary, if ZFC is consistent then whether O'Rear's machine halts is independent of ZFC; it's not a question that ZFC can answer! This leads to an immediate limitation on what ZFC can prove about the busy-beaver function.

Corollary (BB(748) is independent of ZFC). If ZFC is consistent then no theorem of ZFC implies that the busy-beaver function BB(k) = n for any finite n and any finite k ≥ 748.