onoz

onoz is an esolang by Ihope127 where all infinite loops are undetectable. It is a cross between brainfuck and a variant of Brainhype proposed by Ørjan. All instructions except [] work as in brainfuck. When [] is encountered, everything in it is looped as in brainfuck, unless doing so would provably result in an infinite loop, in which case it is simply skipped. Like in Brainhype, no I/O is allowed inside brackets.

Computability

Contrary to initial impressions, onoz is computable. To execute an onoz program, proceed as with brainfuck but, when [ is encountered, save the current tape and initiate a search for nontermination proofs, concurrently continuing to execute the program. Three cases exist:

• The loop terminates. We detect this because execution led us to the end of the loop. In this case, we abort the proof search (which we now know to be fruitless) and continue execution.

• The loop provably does not terminate. Since the set of proofs in standard logical formulations such as first-order logic with the Zermelo-Fraenkel axiom schema is recursively enumerable, if such a proof exists it will be found in finite time, at which point we continue after restoring the saved tape.

• The loop does not terminate, but this fact cannot be proven. Neither the execution nor the proof search will terminate, so the algorithm does not terminate; but this is consistent with the specified behavior of not skipping the loop (since it does not provably result in an infinite loop). This case must be reachable if the chosen logic is expressive enough to satisfy the preconditions of Gödel's second incompleteness theorem.

Example

To demonstrate how one would implement an infinite process in onoz, here is an (incomplete and untested) implementation of a truth machine (for a nonwrapping implementation):

,[>+>+<<-]++++++[>>--------<<-]>>>+<[->>+<<[>>-<<[>>>+<<<-]]>>>[<<<+>>>-]<[>>+>+<[<<<<<<.>>>>>>>S+<]]>-<[>>+<<-]]>>[<<+>>-]<[<<.[>]]

This example, of course, leaves out the largest portion of the code, which is the subprogram S. S is a program which takes the current tape value n and checks whether n is a valid Gödel number of a proof of a contradiction (true=false) in ZF, and then cleans up the tape, returning it to its previous state except that it decrements the cell 1 to the left of its starting position if it found a contradiction. This subprogram will be very long, and implementing it is left as an exercise to the reader. Since ZF is consistent, the decrementation of the cell to the left will never occur, and since this is the sentinel for the loop, the loop will be infinite, as required. And since ZF contains no proof of its consistency, we will not skip the loop.

Note: Although the spec requires that no I/O happen inside brackets, it is impossible to write a Truth-machine with this restriction, so this example depends on an implementation allowing I/O to happen from the simulated loop before it has decided whether to skip the loop or not. If an implementation does this, it means that it will behave unexpectedly on programs that depend on loop-skipping behavior in order to avoid outputting some things. Thus, a more useful implementation of onoz could go ahead and output characters when simulating brackets, but delete them from the output buffer upon deciding to skip the loop.