Halticopter

Halticopter

Paradigm(s)	Declarative
Designed by	Hakerh400
Appeared in	2020
Computational class	Unknown
Major implementations	Unimplemented
File extension(s)	.txt

Halticopter is an esoteric programming language.

Overview

Source code consists of a single Turing machine (we call it $X$). Input is also a Turing machine (we call it $Y$). Output is a single bit.

Halticopter assumes that $X$ does not halt. From that assumption only, it tries to determine whether $Y$ halts. If the program can conclude that $Y$ halts, the program outputs $1$ and halts. If the program can conclude that $Y$ does not halt, the program outputs $0$ and halts. If the program cannot determine whether $Y$ halts or not, the program does not halt. If $X$ halts, the result is undefined (the program may either output $0$ or $1$, or may not halt).

Syntax

Both source code and input represent Turing machines. The syntax of the Turing machine is the following: it is an array of states separated by new lines and each state is represented either as the "HALT" string (for halting states), or as two groups of 3 space-separated decimal non-negative integers enclosed in parentheses (for non-halting states) - the first group is for the current pointed bit being 0 and the second is for 1. In each group, the first number is 0 or 1 (0 - do not invert the memory bit, 1 - invert the memory bit), the second one is 0 or 1 (0 - go left, 1 - go right), and the third one is the next state (0-indexed). The initial state is the state with index 0. Invalid syntax (either in the source code, or in the input) triggers a syntax error.

Examples

Example 1

Source code:

HALT

Input: (anything)

Output: undefined (because $X$ halts)

Example 2

Source code:

(0 0 0) (0 0 0)

Input: (anything)

Output: If the input is literally the same as the source code, the output is $0$. For any other input, the output depends on the inference rules used to determine whether $Y$ halts or not (see the "Further research" section).

Example 3

Source code: (a Turing machine that halts iff ZF is inconcistent)

Input: (a Turing machine that tries to prove a ZF statement starting from the ZF axioms)

Output: If ZF is consistent: if the statement is provable, then the output is $1$, otherwise the output is either $0$, or the program does not halt. If ZF is inconsistent, the result is undefined.

Further research

The language does not seem to be precisely defined. The statement "assuming that $X$ does not halt, we conclude that..." is pretty vague. The language specification can be improved by defining some formal computable inference rules for deducing whether $Y$ halts based on the assumption that $X$ does not halt (if such rules even exist), but without assuming anything else (such as the consistency of ZF or any other formal mathematical system). The author did not come up with any such rules so far.