A decidable problem outside P #

The clocked diagonal Cslib.Complexity.clockedDiagonal J reads a description of a machine framed at the start of its input x (Turing.MultiTapeTM.Universal.decodeDesc), runs the described machine on the whole of x, symbol by symbol under the fixed coding false ↦ 0, true ↦ 1, for J x.length steps with the universal function, and negates the verdict: it returns false exactly when the described machine has halted with output [true] by then. The diagonal function Cslib.Complexity.diagonal is the clocked diagonal with clock 2 ^ n; other clocks give the time hierarchy theorem in CslibFrontier.Computability.Complexity.Classes.Hierarchy.Time.

The diagonal is itself computed, by one fixed machine, within time O(2 ^ (4 * n)) and space O(2 ^ (2 * n)) on inputs of length n (Cslib.Complexity.computableInO_diagonal). The bound charges decoding, converting the input to symbols through the universal input-coding API, writing the clock 2 ^ n in binary, the universal run and the final test. The universal run dominates, within time polynomial in n times 2 ^ (3 * n) and space polynomial in n times 2 ^ n, and one more factor 2 ^ n absorbs the polynomials. The exponents are deliberately loose.

No machine computing a Boolean function in polynomial time decides the diagonal problem, by the diagonal argument of the time hierarchy theorem Arora and Barak, Theorem 3.1. Its description, padded to a length where the machine halts within the exponential clock, is an input on which the diagonal returns the negation of the machine's answer (Cslib.Complexity.diagonal_notMem_P). The argument uses only that the machine halts with its answer within a polynomial time bound, so it applies to plain, not necessarily tidy, machines as well (Cslib.Complexity.not_computableInTimeAndSpace_diagonal). Together, the problem decided by an explicit exponential-time computation is not in P. No time-bounded classes are defined here.

Main definitions #

Cslib.Complexity.clockedDiagonal: the diagonal with a clock.
Cslib.Complexity.diagonal: the diagonal function, with clock 2 ^ n.

Main results #

Cslib.Complexity.computableInO_diagonal: the diagonal in exponential time and space.
Cslib.Complexity.diagonal_notMem_P: the diagonal problem is not in P.
Cslib.Complexity.not_computableInTimeAndSpace_diagonal: no plain machine computes the diagonal within a polynomial time bound.
Cslib.Complexity.clockedDiagonal_desc, Cslib.Complexity.diagonal_desc, Cslib.Complexity.not_forall_halted_diagonal: the reusable diagonal core: the negated answer on a padded description, and the diagonal argument itself.

References #

S. Arora, B. Barak, Computational Complexity: A Modern Approach

The padded diagonal argument follows the original Complexitylib's Classes/Hierarchy and UTM/Diagonal (Samuel Schlesinger), here on the native universal interpreter of Christian Reitwiessner.

source

def Cslib.Complexity.Diagonal.verdict (r : List ℕ × Bool) :

Bool

The output test of the diagonal on a result of the universal function: false exactly when the simulated machine has halted with output [true], under the coding Turing.MultiTapeTM.Universal.eBit.

Instances For

source

def Cslib.Complexity.clockedDiagonal (J : ℕ → ℕ) (x : List Bool) :

Bool

The diagonal with clock J. Run the machine described at the start of x on x, under the coding Turing.MultiTapeTM.Universal.eBit of bits by 0 and 1, for J x.length steps, and return false exactly when it has halted with output [true].

Instances For

source

def Cslib.Complexity.diagonal :

List Bool → Bool

The diagonal function, the clocked diagonal with clock 2 ^ n: run the machine described at the start of x on x for 2 ^ x.length steps, and return false exactly when it has halted with output [true].

Instances For

source

theorem Cslib.Complexity.clockedDiagonal_two_pow :

(clockedDiagonal fun (x : ℕ) => 2 ^ x) = diagonal

The diagonal is the clocked diagonal with clock 2 ^ n.

source

clockedDiagonal J (Turing.MultiTapeTM.frame (Turing.MultiTapeTM.Universal.eDesc (Turing.MultiTapeTM.Universal.desc eS Turing.MultiTapeTM.Universal.eBit tm)) ++ pad) = !b

On its padded description, the clocked diagonal negates the answer of a machine that halts within the clock.

source

diagonal (Turing.MultiTapeTM.frame (Turing.MultiTapeTM.Universal.eDesc (Turing.MultiTapeTM.Universal.desc eS Turing.MultiTapeTM.Universal.eBit tm)) ++ pad) = !b

On its padded description, the diagonal negates the answer of a machine that halts within the exponential clock.

source

theorem Cslib.Complexity.not_forall_halted_diagonal {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) {t : List Bool → ℕ} (ht : Turing.MultiTapeTM.PolyBounded List.length t) (h : ∀ (x : List Bool), (Turing.MultiTapeTM.runFrom (tm.initCfg x) (t x)).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg x) (t x)).output = [diagonal x]) :

False

The diagonal argument. No finite binary machine halts within a polynomially bounded time t x with output [diagonal x] on every input x: on its own description, padded beyond the polynomial, it would answer the negation of its answer.

source

theorem Cslib.Complexity.diagonal_notMem_P :

{x : List Bool | diagonal x = true } ∉ P Turing.MultiTapeTM.encBits

The diagonal problem is not in P, by the diagonal argument of the time hierarchy theorem Arora and Barak, Theorem 3.1.

source

theorem Cslib.Complexity.not_computableInTimeAndSpace_diagonal {t s : List Bool → ℕ} (ht : Turing.MultiTapeTM.PolyBounded List.length t) :

¬Turing.MultiTapeTM.ComputableInTimeAndSpace diagonal Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool t s

No plain machine computes the diagonal in polynomial time: the separation does not depend on tidy normal forms.

The resources of the diagonal #

source

theorem Cslib.Complexity.Diagonal.computableInO_verdict :

Turing.MultiTapeTM.ComputableInO verdict Turing.MultiTapeTM.Universal.eOut Turing.MultiTapeTM.encBool (fun (r : List ℕ × Bool) => ((Turing.MultiTapeTM.Universal.eOut r).length + 1) ^ 2) fun (r : List ℕ × Bool) => (Turing.MultiTapeTM.Universal.eOut r).length

The test is within time quadratic and space linear in the encoded result.

source

theorem Cslib.Complexity.computableInO_diagonal :

Turing.MultiTapeTM.ComputableInO diagonal Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool (fun (x : List Bool) => 2 ^ (4 * x.length)) fun (x : List Bool) => 2 ^ (2 * x.length)

The diagonal is decidable in exponential time, within time O(2 ^ (4 * n)) and space O(2 ^ (2 * n)) on inputs of length n, charging decoding, the symbols, the clock, the universal run and the test.