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

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

global g;

The operations available on globals include assignment and lookup. For example, we can increment a global value:

g = g + 1;

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;.

NQL requires a main procedure, and the main procedure must return. Therefore the shortest legal NQL program is:

proc main() {
    return;
}

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.