181 Complexity — Halting

181.1 Overview

This module establishes the uncomputability of the halting problem [AB09, §1.5.1, Theorem 1.11]. It defines the halting function on the universal machine’s paired input format and proves, by history’s first reduction, that a Turing machine deciding it would make the diagonal function \(\mathrm{UC}\) computable, contradicting the diagonalization theorem [AB09, Theorem 1.10].

181.2 Declarations

Definition 181.1 The halting function

✓

Fix a coding scheme \(c\) that assigns to every bit string \(\alpha \) a Turing machine (the machine that \(\alpha \) denotes under \(c\)). The halting function \(\mathrm{HALT}_c\) maps a bit string \(s\) to a Boolean: \(\mathrm{HALT}_c(s)\) is true precisely when \(s\) is the pairing encoding \(\langle \alpha , x \rangle \) of two bit strings — the universal machine’s input format, code first — and the machine denoted by \(\alpha \) halts on input \(x\), i.e. completes some output within some finite number of steps. Strings not of this form (the pairing encoding is not surjective) are mapped to false.

Theorem 181.2 Unfolding of the halting function

✓

Let \(c\) be a coding scheme for Turing machines and let \(s\) be a bit string. Then \(\mathrm{HALT}_c(s)\) is true if and only if there exist bit strings \(\alpha \) and \(x\) such that \(s\) is the pairing encoding \(\langle \alpha , x \rangle \) and the machine that \(\alpha \) denotes under \(c\) produces some output on input \(x\) within some finite number of steps.

Theorem 181.3 The halting function on a genuine pair

✓

Let \(c\) be a coding scheme for Turing machines and let \(\alpha \) and \(x\) be bit strings. Then \(\mathrm{HALT}_c\), evaluated on the pairing encoding \(\langle \alpha , x \rangle \), is true if and only if the machine that \(\alpha \) denotes under \(c\) halts on input \(x\), completing some output within some finite number of steps.

Theorem 181.4 Reduction from the diagonal function to halting

✓

Let \(c\) be an effective coding scheme for Turing machines, i.e. one admitting a universal evaluator machine. Write \(\mathrm{HALT}_c\) for the halting function of \(c\): it is true on a bit string \(s\) exactly when \(s\) is the pairing encoding \(\langle \alpha , x \rangle \) of two bit strings and the machine denoted by \(\alpha \) under \(c\) halts on input \(x\), and false otherwise. Write \(\mathrm{UC}_c\) for the diagonal function that maps a bit string \(\alpha \) to false when the machine denoted by \(\alpha \) under \(c\) outputs the single bit true on input \(\alpha \) within some finite number of steps, and to true otherwise. If the function mapping \(s\) to the one-bit string carrying \(\mathrm{HALT}_c(s)\) is computable by a Turing machine, then so is the function mapping \(\alpha \) to the one-bit string carrying \(\mathrm{UC}_c(\alpha )\) [AB09, proof of Theorem 1.11].

Theorem 181.5 Uncomputability of the halting problem

✓

Let \(c\) be an effective coding scheme for Turing machines, i.e. one admitting a universal evaluator machine, and let \(\mathrm{HALT}_c\) be its halting function: true on a bit string \(s\) exactly when \(s\) is the pairing encoding \(\langle \alpha , x \rangle \) of two bit strings and the machine denoted by \(\alpha \) under \(c\) produces some output on input \(x\) within some finite number of steps, and false otherwise. Then no Turing machine computes the function mapping \(s\) to the one-bit string carrying \(\mathrm{HALT}_c(s)\) [AB09, Theorem 1.11].