Onoz

From Esolang

The title of this article is incorrect because of technical limitations. The correct title is 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.

[edit] 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. Three cases exist:

• The loop terminates. In this case, the actual execution finishes first; we abort the proof search 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.

This article is a stub, which means that it is not detailed enough and needs to be expanded. Please help us by adding some more information.