HaltingFuck is a language very much like Brainfuck, with one key difference: instead of loops stopping when the value in the current cell is zero, they stop when the value in the current cell is the Gödel number of a HaltingFuck program that halts. The specific Gödel encoding is not specified since it doesn't affect any interesting properties of the language.
It is consistent with the definition of Haltingfuck to claim that all Haltingfuck programs halt. However, this is not the only consistent interpretation - the specification is incomplete. When determining whether a Haltingfuck program halts, there are three possible cases to consider:
- A program with no loops in it. This definitely halts.
- A program containing only loops that start on a cell containing the number of programs of type 1 or 2. This halts too, since by induction none of its loops will run.
- A program containing a loop that starts on a cell containing the number of a program of type 3. These can be divided into two subtypes - those where if you follow the list of programs whose halting behaviour you need to determine in order to determine the behaviour of the first program you eventually come back around to the start, and those where the list continues forever without repetition. For instance, in an encoding where 0 encodes
is of type 3a: in order to determine whether
halts, you must determine whether
halts. On the other hand in an encoding where a number n encodes n+1
+s followed by
is of type 3b: in order to determine whether
halts, you must determine whether + halts, and in order to that you must determine whether
++halts, and so on.
The specified semantics tell us nothing about whether programs of type 3 halt. We can specify that they do, but we can also self-consistently specify that some or all of them don't. If there is any Haltingfuck program that doesn't halt, then that version of Haltingfuck is uncomputable by the same argument as applies to Unhaltingfuck.
HaltingFuck implies a sister language, Unhaltingfuck, whose loops stop when the value in the current cell is the Gödel number of an Unhaltingfuck program that doesn't halt. This language is uncomputable - ie. its specification is complete but inconsistent.