Time hierarchy theorem

DefinitionDeciding within a time bound#✓fully proved

A code \(c\) decides a decision problem \(L\) within the time bound \(t : \mathbb{N} \to \mathbb{N}\) when, on every bit list \(x\), the machine of \(c\) started on the input word of \(x\) halts within \(t(|x|)\) steps, and its tape from the head rightwards, without trailing blanks, is the single symbol of the answer \(L(x)\): \(2\) for true and \(1\) for false.

def Code.DecidesWithin (c : Code) (L : DecisionProblem) (t : ℕ → ℕ) : Prop :=
  ∀ x, c.evalSteps x (t x.length) = some [bitSym (L x)]
Uses 4 · Used by 7
Statement usesCodes for single-tape machines · The clocked evaluator · Symbol of an input bit · Decision problems
Used byTime classes on codes · Some step is needed · Monotonicity of time classes on codes · The constant-false code decides the empty language · Time classes are not empty once the bound exceeds the input length · The diagonal argument · Deciding within a larger time bound

DefinitionTime classes on codes#✓fully proved

For \(t : \mathbb{N} \to \mathbb{N}\), \(\mathrm{CodeTime}(t)\) is the class of decision problems \(L\) such that some code decides \(L\) within \(t(|x|)\) steps on every input \(x\).

def CodeTime (t : ℕ → ℕ) : DecisionComplexityClass :=
  {L | ∃ c : Code, c.DecidesWithin L t}
Uses 4 · Used by 7
Statement usesCodes for single-tape machines · Deciding within a time bound · Complexity classes · Decision problems
Used bySome step is needed · Monotonicity of time classes on codes · A hierarchy within codes, given an upper bound · Time classes are not empty once the bound exceeds the input length · The diagonal argument · Diagonalization across models · Polynomial time is not contained in code time \(n^2 + 1\)

TheoremDeciding within a larger time bound#✓fully proved

If a code \(c\) decides a decision problem \(L\) within a time bound \(t : \mathbb{N} \to \mathbb{N}\), and \(t' : \mathbb{N} \to \mathbb{N}\) satisfies \(t(n) \le t'(n)\) for every \(n\), then \(c\) decides \(L\) within \(t'\).

theorem Code.DecidesWithin.mono {c : Code} {L : DecisionProblem} {t t' : ℕ → ℕ}
    (h : c.DecidesWithin L t) (ht : t ≤ t') : c.DecidesWithin L t'
Uses 5 · Used by 2
Statement usesCodes for single-tape machines · Deciding within a time bound · Decision problems
Proof usesMonotonicity of the single-tape clocked evaluator · Symbol of an input bit
Used byMonotonicity of time classes on codes · Time classes are not empty once the bound exceeds the input length

TheoremMonotonicity of time classes on codes#✓fully proved

Let \(t, t' : \mathbb{N} \to \mathbb{N}\) with \(t(n) \le t'(n)\) for every \(n\). Then every decision problem that some code decides within \(t(|x|)\) steps on every input \(x\) is decided by some code within \(t'(|x|)\) steps on every input \(x\): \(\mathrm{CodeTime}(t) \subseteq \mathrm{CodeTime}(t')\).

theorem codeTime_mono {t t' : ℕ → ℕ} (ht : t ≤ t') : CodeTime t ⊆ CodeTime t'
Uses 6 · Used by 1
Statement usesTime classes on codes · Complexity classes · Decision problems
Proof usesCodes for single-tape machines · Deciding within a time bound · Deciding within a larger time bound
Used byA hierarchy within codes, given an upper bound

DefinitionThe constant-false code#✓fully proved

The code whose table has a single row, for state \(0\): on the blank \(0\) it writes the symbol \(1\), the symbol of the bit false, and enters state \(1\); on the input symbols \(1\) and \(2\) it moves right and stays in state \(0\); on every other symbol it halts. State \(1\) has no row, so the machine halts there. This code answers false on every input.

def Code.constFalse : Code := ⟨[[some (1, 3), some (0, 1), some (0, 1)]]⟩
Uses 1 · Used by 2
Statement usesCodes for single-tape machines
Used byThe constant-false code decides the empty language · Time classes are not empty once the bound exceeds the input length

TheoremThe constant-false code decides the empty language#✓fully proved

Let \(c\) be the code whose table has one row, for state \(0\): on the input symbols \(1\) and \(2\) it moves right and stays in state \(0\), and on the blank \(0\) it writes \(1\), the symbol of the bit \(\mathrm{false}\), and enters state \(1\), which has no row, so that \(c\) halts. Then \(c\) decides the empty language within \(n + 1\) steps on every input of length \(n\).

theorem Code.constFalse_decidesWithin : Code.constFalse.DecidesWithin (fun _ ↦ false) (· + 1)
Uses 13 · Used by 1
Statement usesDeciding within a time bound · The constant-false code
Proof usesCodes for single-tape machines · Explicit configurations · Output of a configuration · Clocked configuration of a code · The clocked evaluator · Characterization of clocked results · Initial configuration of the code simulation · One step of a code · One step of a code, or stay when halted · Symbol of an input bit · Input word of a list of bits
Used byTime classes are not empty once the bound exceeds the input length

TheoremTime classes are not empty once the bound exceeds the input length#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(n + 1 \le f(n)\) for every \(n\). Then the empty language, the decision problem that answers false on every bit list, belongs to the time class of \(f\): some code decides it within \(f(|x|)\) steps on every input \(x\), where \(|x|\) is the length of \(x\).

theorem const_false_mem_codeTime {f : ℕ → ℕ} (hf : ∀ n, n + 1 ≤ f n) :
    (fun _ ↦ false) ∈ CodeTime f
Uses 8
Statement usesTime classes on codes · Complexity classes · Decision problems
Proof usesCodes for single-tape machines · Deciding within a time bound · Deciding within a larger time bound · The constant-false code · The constant-false code decides the empty language

TheoremSome step is needed#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\) with \(f(0) = 0\). Then no decision problem is decided by a code within \(f(|x|)\) steps on every input \(x\): the time class \(\mathrm{CodeTime}(f)\) is empty. With no step on the empty input, the tape stays blank and holds no answer bit.

theorem codeTime_eq_empty {f : ℕ → ℕ} (hf : f 0 = 0) : CodeTime f = ∅
Uses 12
Statement usesTime classes on codes · Complexity classes · Decision problems
Proof usesCodes for single-tape machines · Explicit configurations · Output of a configuration · Deciding within a time bound · Clocked configuration of a code · The clocked evaluator · Characterization of clocked results · One step of a code · Symbol of an input bit

TheoremThe code stack determines the table lookups#✓fully proved

If two codes \(c\) and \(c'\) have the same code stack, then for every state \(q\) and every symbol \(a\), the table entry of \(c\) at \((q, a)\) equals the table entry of \(c'\) at \((q, a)\).

theorem Code.lookup_eq_of_codeCells_eq {c c' : Code} (h : codeCells c = codeCells c') :
    c.lookup = c'.lookup
Uses 10 · Used by 1
Statement usesThe code stack · Codes for single-tape machines · Table lookup of a code
Proof usesThe cell of a number · The cells of a list of numbers · Entries of a code · Numbers of a list of entries · Looking up a key in a list of entries · Scanning the entries finds the table entry · Unary counter
Used byThe code stack determines the clocked semantics

TheoremThe code stack determines the clocked semantics#✓fully proved

Codes with the same code stack have the same clocked evaluator.

theorem Code.evalSteps_eq_of_codeCells_eq {c c' : Code} (h : codeCells c = codeCells c') :
    c.evalSteps = c'.evalSteps
Uses 12 · Used by 1
Statement usesThe code stack · Codes for single-tape machines · The clocked evaluator
Proof usesExplicit configurations · Acting on a configuration · Output of a configuration · Clocked configuration of a code · Initial configuration of the code simulation · Table lookup of a code · The code stack determines the table lookups · One step of a code · One step of a code, or stay when halted
Used byThe diagonal language on a code stack

TheoremReading a unary length prefix reads one cell#✓fully proved

For bit lists \(x\) and \(r\) and a natural number \(n\), reading a unary length prefix of \(x\) returns \(n\) together with the rest \(r\) if and only if \(x\) is the cell of \(n\) (that is, \(n\) copies of \(\mathrm{true}\) followed by \(\mathrm{false}\)) followed by \(r\).

theorem readUnaryLength_eq_some_iff_cell {x r : List Bool} {n : ℕ} :
    readUnaryLength x = some (n, r) ↔ x = cell n ++ r
Uses 3 · Used by 7
Statement usesReading a unary length prefix · The cell of a number
Proof usesUnary counter
Used byDecoding a list of cells · Cell-by-cell check of a code stack · The cell-by-cell check recognizes code stacks · Decoding inverts the code stack · Code stacks are recognized · Code stacks, entry by entry · The checking run

DefinitionDecoding a list of cells#✓fully proved

For a bit list \(x\), the list of natural numbers \(l\) whose cells are \(x\), if there is one, and nothing otherwise. Here the cells of \(l\) are its numbers written in order, each number \(n\) as \(n\) copies of \(\mathrm{true}\) followed by one \(\mathrm{false}\); distinct lists have distinct cells. The decoder reads one cell at a time with the unary length reader.

def cellsDecode (x : List Bool) : Option (List ℕ) :=
  match x with
  | [] => some []
  | b :: x' =>
    match h : readUnaryLength (b :: x') with
    | none => none
    | some (n, r) =>
      have : r.length < (b :: x').length := by
        rw [readUnaryLength_eq_some_iff_cell.1 h]
        simp [cell]
        omega
      (cellsDecode r).map (n :: ·)
termination_by x.length
Uses 4 · Used by 4
Statement usesReading a unary length prefix · The cell of a number · Reading a unary length prefix reads one cell · Unary counter
Used byDecoding inverts the code stack · Decoding a code stack · Code stacks are recognized · Code stacks, entry by entry

DefinitionReading entries from numbers#✓fully proved

A list of natural numbers is read as a list of entries \((q, a, q', s)\), four consecutive numbers per entry, if possible: the empty list gives no entries; a list that starts with \(q, a, q', s\) and continues with \(l\) gives the entry \((q, a, q', s)\) followed by the entries read from \(l\), if that succeeds; and the reading fails when the length of the list is not a multiple of \(4\).

def entriesOfNums : List ℕ → Option (List (ℕ × ℕ × ℕ × ℕ))
  | [] => some []
  | q :: a :: q' :: s :: l => (entriesOfNums l).map ((q, a, q', s) :: ·)
  | _ => none
Used by 4
Used byDecoding inverts the code stack · Decoding a code stack · Code stacks are recognized · Code stacks, entry by entry

DefinitionAscending keys of a list of entries#✓fully proved

For natural numbers \(p_q\), \(p_a\) and a list of entries \((q, a, q', s) \in \mathbb{N}^4\), this Boolean test is true exactly when the keys \((q, a)\) of the entries strictly increase in lexicographic order and the first key, if there is one, is at least \((p_q, p_a)\) in that order.

def keysAscendFrom (pq pa : ℕ) : List (ℕ × ℕ × ℕ × ℕ) → Bool
  | [] => true
  | e :: es => decide (pq < e.1 ∨ pq = e.1 ∧ pa ≤ e.2.1) && keysAscendFrom e.1 (e.2.1 + 1) es
Used by 6
Used byThe cell-by-cell check recognizes code stacks · The cell-by-cell check agrees with code-stack decoding · Decoding inverts the code stack · Decoding a code stack · Code stacks are recognized · Code stacks, entry by entry

DefinitionThe code of a list of entries#✓fully proved

Let \(E\) be a list of entries \((q, a, q', s)\) of natural numbers, and let \(Q\) and \(M\) be the sums, over the entries of \(E\) counted with multiplicity, of \(q + 1\) and of \(a + 1\) respectively. The code of \(E\) has a table with \(Q\) rows and \(M\) columns, and for \(q < Q\) and \(a < M\) its position \((q, a)\) holds \((q', s)\) for the first entry \((q, a, q', s)\) of \(E\) with key \((q, a)\), and is empty (halting) if \(E\) has no entry with that key.

def codeOfEntries (es : List (ℕ × ℕ × ℕ × ℕ)) : Code :=
  ⟨(List.range (es.map fun e ↦ e.1 + 1).sum).map fun q ↦
    (List.range (es.map fun e ↦ e.2.1 + 1).sum).map fun a ↦ findEntry q a es⟩
Uses 2 · Used by 4
Statement usesLooking up a key in a list of entries · Codes for single-tape machines
Used byDecoding inverts the code stack · Decoding a code stack · Code stacks are recognized · Code stacks, entry by entry

DefinitionDecoding a code stack#✓fully proved

For a bit list \(x\), the decoding of \(x\) as a code is defined as follows. Write the cell of a number \(n\) for the \(n\) bits true followed by one bit false, and the cells of a list of numbers for the cells of its numbers in order. If \(x\) is the cells of a list \(l\) of natural numbers (such an \(l\) is unique), the length of \(l\) is a multiple of \(4\), and the keys \((q, a)\) of the entries \((q, a, q', s)\) formed by the consecutive groups of four numbers of \(l\) strictly increase in lexicographic order, then the decoding of \(x\) is the code of these entries. Otherwise the decoding returns no code.

The code stack of a code is the cells of the numbers \(q, a, q', s\) of its entries \((q, a, q', s)\), listed by increasing key \((q, a)\); codes with the same code stack have the same clocked evaluator.

def decodeCodeCells (x : List Bool) : Option Code :=
  ((cellsDecode x).bind entriesOfNums).bind fun es ↦
    if keysAscendFrom 0 0 es then some (codeOfEntries es) else none
Uses 5 · Used by 12
Statement usesCodes for single-tape machines · Decoding a list of cells · The code of a list of entries · Reading entries from numbers · Ascending keys of a list of entries
Used byThe cell-by-cell check agrees with code-stack decoding · Decoding inverts the code stack · Code stacks decode to codes with the same code stack · The diagonal language · The universal machine's argument for the diagonal language · The diagonal language on a code stack · The diagonal language through the clocked evaluator · Bit lists that encode no code are outside the diagonal language · The reformatting function in bits · Code stacks are recognized · Code stacks, entry by entry · Layout after checking gives the universal machine's input

DefinitionThe diagonal language#✓fully proved

For \(f : \mathbb{N} \to \mathbb{N}\), the diagonal language of \(f\) holds at a bit list \(x\) iff \(x\) encodes a code \(c\) and the clocked evaluator, running \(c\) on \(x\) for at most \(f(|x|)\) steps, does not return the output \([2]\), the symbol of the answer true: either \(c\) does not halt on \(x\) within \(f(|x|)\) steps, or it halts with another output. Bit lists that encode no code are not in the language. This is the diagonal language of the proof of Sipser's Theorem 9.10.

def diag (f : ℕ → ℕ) : DecisionProblem := fun x ↦
  match decodeCodeCells x with
  | none => false
  | some c => decide (c.evalSteps x (f x.length) ≠ some [bitSym true])
Uses 5 · Used by 11
Statement usesCodes for single-tape machines · The clocked evaluator · Symbol of an input bit · Decoding a code stack · Decision problems
Used byA hierarchy within codes, given an upper bound · The diagonal language on a code stack · The diagonal language through the universal machine · The diagonal language through the clocked evaluator · Bit lists that encode no code are outside the diagonal language · The diagonal argument · The quadratic diagonal language is in P · Diagonalization across models · The diagonal language in polynomial time, given the reformatting machine · Deciding the diagonal language on raw bits in polynomial time · Polynomial time is not contained in code time \(n^2 + 1\)

TheoremDecoding inverts the code stack#✓fully proved

For every bit list \(x\) and every code \(c\), if \(x\) decodes to \(c\), then the code stack of \(c\) is \(x\).

theorem codeCells_of_decodeCodeCells_eq_some {x : List Bool} {c : Code}
    (h : decodeCodeCells x = some c) :
    codeCells c = x
Uses 17 · Used by 4
Statement usesThe code stack · Codes for single-tape machines · Decoding a code stack
Proof usesReading a unary length prefix · The cell of a number · The cells of a list of numbers · Entries of a code · Numbers of a list of entries · Looking up a key in a list of entries · Scanning the entries finds the table entry · Table lookup of a code · Decoding a list of cells · The code of a list of entries · Reading entries from numbers · Ascending keys of a list of entries · Reading a unary length prefix reads one cell · Unary counter
Used byCode stacks decode to codes with the same code stack · Bit lists that encode no code are outside the diagonal language · The reformatting function in bits · Code stacks are recognized

TheoremCode stacks are recognized#✓fully proved

For every bit list \(x\), the decoding of \(x\) as a code succeeds iff \(x\) is the code stack of some code.

theorem isSome_decodeCodeCells_iff (x : List Bool) :
    (decodeCodeCells x).isSome ↔ ∃ c : Code, codeCells c = x
Uses 16 · Used by 1
Statement usesThe code stack · Codes for single-tape machines · Decoding a code stack
Proof usesReading a unary length prefix · The cell of a number · The cells of a list of numbers · Entries of a code · Numbers of a list of entries · Table lookup of a code · Decoding a list of cells · The code of a list of entries · Reading entries from numbers · Ascending keys of a list of entries · Reading a unary length prefix reads one cell · Decoding inverts the code stack · Unary counter
Used byCode stacks decode to codes with the same code stack

TheoremCode stacks, entry by entry#✓fully proved

A bit list \(x\) encodes a code (its decoding succeeds) iff there is a list of entries \((q, a, q', s)\) of natural numbers whose keys \((q, a)\) strictly increase in lexicographic order, such that \(x\) is the list of cells of the numbers of these entries, four numbers per entry.

theorem isSome_decodeCodeCells_iff_entries (x : List Bool) : (decodeCodeCells x).isSome ↔
    ∃ es, x = cells (entryNums es) ∧ keysAscendFrom 0 0 es = true
Uses 12 · Used by 1
Statement usesThe cells of a list of numbers · Numbers of a list of entries · Codes for single-tape machines · Ascending keys of a list of entries · Decoding a code stack
Proof usesReading a unary length prefix · The cell of a number · Decoding a list of cells · The code of a list of entries · Reading entries from numbers · Reading a unary length prefix reads one cell · Unary counter
Used byThe cell-by-cell check agrees with code-stack decoding

TheoremCode stacks decode to codes with the same code stack#✓fully proved

For every code \(c\), decoding the code stack of \(c\) succeeds and returns a code \(c'\) whose code stack equals the code stack of \(c\).

theorem decodeCodeCells_codeCells (c : Code) :
    ∃ c', decodeCodeCells (codeCells c) = some c' ∧ codeCells c' = codeCells c
Uses 5 · Used by 1
Statement usesThe code stack · Codes for single-tape machines · Decoding a code stack
Proof usesDecoding inverts the code stack · Code stacks are recognized
Used byThe diagonal language on a code stack

TheoremThe diagonal language on a code stack#✓fully proved

For every time bound \(f : \mathbb{N} \to \mathbb{N}\) and every code \(c\) with code stack \(x\), the bit list \(x\) belongs to the diagonal language for \(f\) iff it is not the case that \(c\), run on \(x\), halts within \(f(|x|)\) steps with output the single symbol \(2\) of the bit true.

theorem diag_codeCells (f : ℕ → ℕ) (c : Code) :
    diag f (codeCells c) =
      decide (c.evalSteps (codeCells c) (f (codeCells c).length) ≠ some [bitSym true])
Uses 8 · Used by 2
Statement usesThe code stack · Codes for single-tape machines · The clocked evaluator · Symbol of an input bit · The diagonal language
Proof usesThe code stack determines the clocked semantics · Decoding a code stack · Code stacks decode to codes with the same code stack
Used byThe diagonal language through the universal machine · The diagonal argument

TheoremBit lists that encode no code are outside the diagonal language#✓fully proved

For every \(f : \mathbb{N} \to \mathbb{N}\) and every bit list \(x\) that is the code stack of no code, \(x\) is not in the diagonal language of \(f\).

theorem diag_eq_false {f : ℕ → ℕ} {x : List Bool} (hx : ∀ c : Code, codeCells c ≠ x) :
    diag f x = false
Uses 7
Statement usesThe code stack · Codes for single-tape machines · The diagonal language
Proof usesThe clocked evaluator · Symbol of an input bit · Decoding inverts the code stack · Decoding a code stack

TheoremThe diagonal language through the universal machine#✓fully proved

For every time bound \(f : \mathbb{N} \to \mathbb{N}\) and every code \(c\) with code stack \(x\), the bit list \(x\) belongs to the diagonal language for \(f\) iff the output encoding of the result of running \(c\) on \(x\) for at most \(f(|x|)\) steps differs from the output encoding of the result whose output is the single symbol \(2\) of the bit true.

The clocked universal machine reads the input encoding of a code, an input and a clock \(T\) and writes the output encoding of the result of running the code on the input for at most \(T\) steps, so the condition is read from its output on \(c\), \(x\) and \(f(|x|)\).

theorem diag_codeCells_eq_encOut (f : ℕ → ℕ) (c : Code) :
    diag f (codeCells c) = decide
      (encOut (c.evalSteps (codeCells c) (f (codeCells c).length)) ≠
        encOut (some [bitSym true]))
Uses 10
Statement usesThe code stack · Output encoding of the clocked universal machine · Codes for single-tape machines · The clocked evaluator · Symbol of an input bit · The diagonal language
Proof usesThe cell of a number · The cells of a list of numbers · The diagonal language on a code stack · Unary counter

TheoremThe diagonal argument#✓fully proved

For every \(f : \mathbb{N} \to \mathbb{N}\), the diagonal language of \(f\) is not in the time class of \(f\) on codes: no code decides it on every input \(x\) within \(f(|x|)\) steps. This is the argument from the proof of Sipser's Theorem 9.10: a code \(c\) deciding it would, on its own code stack, answer the opposite of the diagonal language of \(f\).

theorem diag_not_mem_codeTime (f : ℕ → ℕ) : diag f ∉ CodeTime f
Uses 10 · Used by 3
Statement usesTime classes on codes · The diagonal language · Complexity classes · Decision problems
Proof usesThe code stack · Codes for single-tape machines · Deciding within a time bound · The clocked evaluator · Symbol of an input bit · The diagonal language on a code stack
Used byA hierarchy within codes, given an upper bound · Diagonalization across models · Polynomial time is not contained in code time \(n^2 + 1\)

TheoremA hierarchy within codes, given an upper bound#✓fully proved

Let \(f, g : \mathbb{N} \to \mathbb{N}\) with \(f(n) \le g(n)\) for every \(n\), and for a time bound \(t\) let \(\mathrm{CodeTime}(t)\) be the class of decision problems that some code decides within \(t(|x|)\) steps on every input \(x\). If the diagonal language \(\mathrm{diag}(f)\) belongs to \(\mathrm{CodeTime}(g)\), then \(\mathrm{CodeTime}(f)\) is a proper subclass of \(\mathrm{CodeTime}(g)\).

theorem codeTime_ssubset_of_diag_mem {f g : ℕ → ℕ} (hfg : f ≤ g) (h : diag f ∈ CodeTime g) :
    CodeTime f ⊂ CodeTime g
Uses 6
Statement usesTime classes on codes · The diagonal language · Complexity classes · Decision problems
Proof usesMonotonicity of time classes on codes · The diagonal argument

DefinitionThe universal machine's argument for the diagonal language#✓fully proved

For a time bound \(f : \mathbb{N} \to \mathbb{N}\) and a bit list \(x\), the argument is a triple of a code, an input and a clock. If \(x\) decodes to a code \(c\), it is \((c, x, f(|x|))\). Otherwise it is the code with the empty table, the input consisting of the single bit true, and the clock \(0\); that code halts at once with the answer true, so that the diagonal answer is false there.

def diagArg (f : ℕ → ℕ) (x : List Bool) : Code × List Bool × ℕ :=
  match decodeCodeCells x with
  | some c => (c, x, f x.length)
  | none => (⟨[]⟩, [true], 0)
Uses 2 · Used by 5
Statement usesCodes for single-tape machines · Decoding a code stack
Used byThe diagonal language through the clocked evaluator · The reformatting function in bits · Layout after checking gives the universal machine's input · The diagonal language in polynomial time, given the reformatting machine · The reformatting machine for \(n \mapsto n^2 + 1\)

TheoremThe reformatting function in bits#✓fully proved

For \(f : \mathbb{N} \to \mathbb{N}\) and a bit list \(x\), the input bits of the clocked universal machine on its argument for the diagonal language of \(f\) on \(x\) are, when \(x\) encodes a code, the cell of \(f(|x|)\), then the cells of the input symbols of \(x\), then the bit false, then \(x\) reversed; when \(x\) encodes no code, they are the fixed list \([\mathrm{false}, \mathrm{true}, \mathrm{true}, \mathrm{false}, \mathrm{false}]\).

theorem encIn_diagArg (f : ℕ → ℕ) (x : List Bool) :
    encIn (diagArg f x).1 (diagArg f x).2.1 (diagArg f x).2.2 =
      if (decodeCodeCells x).isSome then
        cell (f x.length) ++ (cells (input x) ++ (false :: x.reverse))
      else [false, true, true, false, false]
Uses 9 · Used by 1
Statement usesThe cell of a number · The cells of a list of numbers · Input encoding of the clocked universal machine · Codes for single-tape machines · Decoding a code stack · The universal machine's argument for the diagonal language · Input word of a list of bits
Proof usesThe code stack · Decoding inverts the code stack
Used byLayout after checking gives the universal machine's input

DefinitionThe diagonal answer#✓fully proved

For a clocked result \(o\), either a timeout or the output of a halted run, the diagonal answer of \(o\) is false if \(o\) is the output consisting of the single symbol \(2\), the symbol of the bit true, and true otherwise, including on a timeout.

def diagAnswer (o : Option (List ℕ)) : Bool := decide (o ≠ some [bitSym true])
Uses 1 · Used by 4
Statement usesSymbol of an input bit
Used byThe diagonal answer read from the encoded output · The diagonal language through the clocked evaluator · The diagonal language in polynomial time, given the reformatting machine · The readout in polynomial time

TheoremThe diagonal answer read from the encoded output#✓fully proved

For every clocked result \(o\), either a timeout or the output of a halted run, the diagonal answer of \(o\) is true exactly when the output encoding of \(o\) differs from the output encoding of the result whose output is the single symbol \(2\) of the bit true, which is the bit list true, true, true, false.

theorem diagAnswer_eq_decide_encOut (o : Option (List ℕ)) :
    diagAnswer o = decide (encOut o ≠ encOut (some [bitSym true]))
Uses 6 · Used by 1
Statement usesOutput encoding of the clocked universal machine · Symbol of an input bit · The diagonal answer
Proof usesThe cell of a number · The cells of a list of numbers · Unary counter
Used byThe readout in polynomial time

TheoremThe diagonal language through the clocked evaluator#✓fully proved

For every \(f : \mathbb{N} \to \mathbb{N}\) and every bit list \(x\), let \((c, y, T)\) be the universal machine's argument for the diagonal language of \(f\) on \(x\). Then the diagonal language of \(f\) holds at \(x\) iff the clocked evaluator, running \(c\) on \(y\) for at most \(T\) steps, does not return the output \([2]\), the symbol of the answer true.

theorem diag_eq_comp (f : ℕ → ℕ) :
    diag f = diagAnswer ∘ (fun a : Code × List Bool × ℕ ↦ a.1.evalSteps a.2.1 a.2.2) ∘
      diagArg f
Uses 8 · Used by 1
Statement usesCodes for single-tape machines · The clocked evaluator · The diagonal language · The diagonal answer · The universal machine's argument for the diagonal language · Decision problems
Proof usesSymbol of an input bit · Decoding a code stack
Used byThe diagonal language in polynomial time, given the reformatting machine

InductiveStacks of the readout machine#✓fully proved

The readout machine, which reads the answer of the diagonal language off the output of the clocked universal machine, has exactly two stacks: the input stack \(X\) and the output stack \(O\).

inductive K | X | O
  deriving DecidableEq
Used by 6
Used byThe readout on raw bits in polynomial time · The readout machine as a host component · Expecting a bit in the readout machine · Program of the readout machine · The readout run · Stack alphabet of the readout machine

InductiveLabels of the readout machine#✓fully proved

The readout machine has eight labels: \(r_0\), \(r_1\), \(r_2\) and \(r_3\) read in turn the bits \(\mathrm{true}, \mathrm{true}, \mathrm{true}, \mathrm{false}\), which encode, at the output of the clocked universal machine, a halt whose output is the single symbol of the bit \(\mathrm{true}\); \(r_4\) checks that no bit follows; \(\mathrm{hit}\) and \(\mathrm{miss}\) write the answer; and \(\mathrm{done}\) stops.

inductive Lab | r0 | r1 | r2 | r3 | r4 | hit | miss | done
  deriving DecidableEq
Used by 5
Used byThe readout on raw bits in polynomial time · The readout machine as a host component · Expecting a bit in the readout machine · Program of the readout machine · The readout run

AbbreviationStack alphabet of the readout machine#✓fully proved

Every stack of the readout machine, namely the input stack \(X\) and the output stack \(O\), has the alphabet of bits.

abbrev Γ : K → Type := fun _ => Bool
Uses 1 · Used by 5
Statement usesStacks of the readout machine
Used byThe readout on raw bits in polynomial time · The readout machine as a host component · Expecting a bit in the readout machine · Program of the readout machine · The readout run

DefinitionExpecting a bit in the readout machine#✓fully proved

For a bit \(b\) and a label \(\ell\), the statement that pops the top of the input stack \(X\) and goes to \(\ell\) if the popped symbol is \(b\), and to the label miss otherwise, including when \(X\) is empty.

def expect (b : Bool) (next : Lab) : TM2.Stmt Γ Lab Bool :=
  .pop .X (fun _ o ↦ o == some b) (.branch id (.goto fun _ ↦ next) (.goto fun _ ↦ .miss))
Uses 3 · Used by 1
Statement usesStacks of the readout machine · Labels of the readout machine · Stack alphabet of the readout machine
Used byProgram of the readout machine

DefinitionProgram of the readout machine#✓fully proved

The readout machine pops the bits of its input stack \(X\) one at a time and compares them with \(\mathrm{true}, \mathrm{true}, \mathrm{true}, \mathrm{false}\), which encode, at the output of the clocked universal machine, a halt whose output is the single symbol of the bit \(\mathrm{true}\). If the input is exactly this list, it pushes \(\mathrm{false}\) onto its output stack \(O\); otherwise (at the first bit that differs, when the input ends early, or when a fifth bit follows) it pushes \(\mathrm{true}\). Then it halts.

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .r0 => expect true .r1
  | .r1 => expect true .r2
  | .r2 => expect true .r3
  | .r3 => expect false .r4
  | .r4 => .pop .X (fun _ o ↦ o.isNone) (.branch id (.goto fun _ ↦ .hit) (.goto fun _ ↦ .miss))
  | .hit => .push .O (fun _ ↦ false) (.goto fun _ ↦ .done)
  | .miss => .push .O (fun _ ↦ true) (.goto fun _ ↦ .done)
  | .done => .halt
Uses 4 · Used by 3
Statement usesStacks of the readout machine · Labels of the readout machine · Expecting a bit in the readout machine · Stack alphabet of the readout machine
Used byThe readout on raw bits in polynomial time · The readout machine as a host component · The readout run

AbbreviationThe readout machine as a host component#✓fully proved

The component machine whose stacks are the input \(X\) and the output \(O\), each over the alphabet of bits, whose labels and program are those of the readout machine, which checks whether \(X\) holds exactly \((\mathrm{true}, \mathrm{true}, \mathrm{true}, \mathrm{false})\) and pushes \(\mathrm{false}\) on \(O\) if so and \(\mathrm{true}\) otherwise, and whose list of stacks is \((X, O)\).

abbrev comp : Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ := fun _ ↦ inferInstanceAs (Fintype Bool)
  L := Lab
  prog := prog
  ks := [.X, .O]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide
Uses 5 · Used by 1
Statement usesComponent machine · Stacks of the readout machine · Labels of the readout machine · Program of the readout machine · Stack alphabet of the readout machine
Used byThe readout on raw bits in polynomial time

TheoremThe readout run#✓fully proved

Let \(l\) be a bit list, and start the readout machine at the label \(r_0\) with its internal Boolean variable set to \(\mathrm{false}\), \(l\) on the input stack \(X\) and the output stack \(O\) empty. Then the machine reaches the label \(\mathrm{done}\) within \(6\) steps, and \(O\) then holds exactly one bit, which is \(\mathrm{true}\) if and only if \(l \ne [\mathrm{true}, \mathrm{true}, \mathrm{true}, \mathrm{false}]\), the list that encodes, at the output of the clocked universal machine, a halt whose output is the single symbol of the bit \(\mathrm{true}\).

theorem run (l : List Bool) :
    ∃ v S', RunLe prog 6 ⟨some .r0, false, update (fun _ ↦ []) .X l⟩ ⟨some .done, v, S'⟩ ∧
      S' .O = [decide (l ≠ encOut (some [bitSym true]))]
Uses 8 · Used by 1
Statement usesOutput encoding of the clocked universal machine · Stacks of the readout machine · Labels of the readout machine · Program of the readout machine · Stack alphabet of the readout machine · Symbol of an input bit · Runs within a step budget
Proof usesExact-length runs of a TM2 machine
Used byThe readout on raw bits in polynomial time

DefinitionThe readout on raw bits in polynomial time#✓fully proved

A finite multi-stack Turing machine, whose input and output alphabets are identified with the bits, together with a polynomial time bound, such that for every bit list \(l\), given \(l\) as its input, it halts within the bound, evaluated at \(|l|\), with output the one-bit list \([b]\), where \(b\) is true if and only if \(l\) differs from the output encoding of the result whose output is the single symbol \(2\) of the bit true, that is, from the list true, true, true, false.

noncomputable def bitsPolyTime :
    TM2ComputableInPolyTime (fun l : List Bool ↦ l) (fun l : List Bool ↦ l)
      (fun l ↦ [decide (l ≠ encOut (some [bitSym true]))]) :=
  Complexity.Host.reduction (c := comp) (cX := .X) (cO := .O) (gX := id) (start := .r0)
    (done := .done) (Equiv.refl Bool) _ (Polynomial.C 6) rfl fun l ↦ by
      obtain ⟨v, S', hr, hO⟩ := run l
      exact ⟨v, S', by simpa using hr, by simpa using hO⟩
Uses 11 · Used by 1
Statement usesComponent machine · Reduction host · Output encoding of the clocked universal machine · Stacks of the readout machine · Labels of the readout machine · The readout machine as a host component · Program of the readout machine · The readout run · Stack alphabet of the readout machine · Symbol of an input bit · Runs within a step budget
Used byThe readout in polynomial time

DefinitionThe readout in polynomial time#✓fully proved

A finite multi-stack Turing machine, given the output encoding \(\mathrm{encOut}(o)\) of a result \(o\) of the clocked universal function (a list of symbols, or a timeout), outputs the one-bit list \([\mathrm{diagAnswer}(o)]\) within a number of steps polynomial in the length of \(\mathrm{encOut}(o)\). Here \(\mathrm{diagAnswer}(o)\) is \(\mathrm{true}\) unless \(o\) is a halt whose output is the single symbol of the bit \(\mathrm{true}\).

noncomputable def polyTime : TM2ComputableInPolyTime encOut (fun b : Bool ↦ [b]) diagAnswer where
  toTM2ComputableAux := bitsPolyTime.toTM2ComputableAux
  time := bitsPolyTime.time
  outputsFun o := by
    have h := bitsPolyTime.outputsFun (encOut o)
    rwa [← diagAnswer_eq_decide_encOut] at h
Uses 5 · Used by 1
Statement usesOutput encoding of the clocked universal machine · The readout on raw bits in polynomial time · Symbol of an input bit · The diagonal answer · The diagonal answer read from the encoded output
Used byThe diagonal language in polynomial time, given the reformatting machine

TheoremThe diagonal language in polynomial time, given the reformatting machine#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\). Suppose that a finite multi-stack Turing machine, the reformatting machine, computes in polynomial time, from a bit list \(x\) given as itself, the input \(\mathrm{encIn}(c, y, T)\) of the clocked universal machine, where \((c, y, T) = \mathrm{diagArg}_f(x)\) is the argument of the clocked universal function for the diagonal language \(\mathrm{diag}_f\) on \(x\). Then a finite multi-stack Turing machine computes \(\mathrm{diag}_f\) in polynomial time: on every bit list \(x\), given as itself, it outputs the one-bit list \([\mathrm{diag}_f(x)]\).

The machine runs the reformatting machine, then the clocked universal machine, then the readout machine.

theorem nonempty_diag_polyTime {f : ℕ → ℕ}
    (hR : TM2ComputableInPolyTime (fun x : List Bool ↦ x)
      (fun a : Code × List Bool × ℕ ↦ encIn a.1 a.2.1 a.2.2) (diagArg f)) :
    Nonempty (TM2ComputableInPolyTime (fun x : List Bool ↦ x) (fun b : Bool ↦ [b]) (diag f))
Uses 12 · Used by 1
Statement usesInput encoding of the clocked universal machine · Codes for single-tape machines · The diagonal language · The universal machine's argument for the diagonal language
Proof usesOutput encoding of the clocked universal machine · The clocked universal function is polynomial-time computable · The clocked evaluator · The readout in polynomial time · The diagonal answer · The diagonal language through the clocked evaluator · Decision problems · The composite polynomial-time TM2 computation
Used byDeciding the diagonal language on raw bits in polynomial time

DefinitionCell-by-cell check of a code stack#✓fully proved

The check of a bit list \(x\) from a key \((p_q, p_a)\) of natural numbers is defined as follows. The empty list passes. Otherwise, calling the cell of a number \(n\) the \(n\) bits \(\mathrm{true}\) followed by one bit \(\mathrm{false}\), read four cells off the front of \(x\), those of \(q\), \(a\), \(q'\) and \(s\) in this order, leaving the rest \(r\). The check fails if one of these cells cannot be read because what remains contains no bit \(\mathrm{false}\), or if the key \((q, a)\) is lexicographically below \((p_q, p_a)\), that is, unless \(p_q < q\), or \(p_q = q\) and \(p_a \le a\). Otherwise its result is the check of \(r\) from the key \((q, a + 1)\).

The reformatting machine checks its input this way.

Cslib.Turing.Universal.Diag.chkFrom · 28 lines 
def chkFrom (pq pa : ℕ) (x : List Bool) : Bool :=
  match x with
  | [] => true
  | b :: x' =>
    match _h1 : readUnaryLength (b :: x') with
    | none => false
    | some (q, x1) =>
      match _h2 : readUnaryLength x1 with
      | none => false
      | some (a, x2) =>
        if pq < q ∨ pq = q ∧ pa ≤ a then
          match _h3 : readUnaryLength x2 with
          | none => false
          | some (_, x3) =>
            match h4 : readUnaryLength x3 with
            | none => false
            | some (_, x4) => chkFrom q (a + 1) x4
        else false
termination_by x.length
decreasing_by
  have e1 := congrArg List.length (readUnaryLength_eq_some_iff_cell.1 _h1)
  have e2 := congrArg List.length (readUnaryLength_eq_some_iff_cell.1 _h2)
  have e3 := congrArg List.length (readUnaryLength_eq_some_iff_cell.1 _h3)
  have e4 := congrArg List.length (readUnaryLength_eq_some_iff_cell.1 h4)
  simp only [cell, List.length_append, List.length_replicate, List.length_cons,
    List.length_nil] at e1 e2 e3 e4
  simp only [List.length_cons]
  omega
Uses 4 · Used by 5
Statement usesReading a unary length prefix · The cell of a number · Reading a unary length prefix reads one cell · Unary counter
Used byAnswer of the checking machine · The cell-by-cell check recognizes code stacks · The cell-by-cell check agrees with code-stack decoding · Layout after checking gives the universal machine's input · The checking run

TheoremThe cell-by-cell check recognizes code stacks#✓fully proved

For all natural numbers \(p_q, p_a\) and every bit list \(x\), the cell-by-cell check of \(x\) from the key \((p_q, p_a)\) succeeds if and only if there is a list of \(m \ge 0\) entries \((q_1, a_1, q'_1, s_1), \dots, (q_m, a_m, q'_m, s_m)\) of natural numbers such that \(x\) is the concatenation of the cells of \(q_1, a_1, q'_1, s_1, \dots, q_m, a_m, q'_m, s_m\), in this order, and the keys \((q_i, a_i)\) strictly increase in lexicographic order, starting at \((p_q, p_a)\) or above. Here the cell of a number \(n\) is \(n\) bits \(\mathrm{true}\) followed by one bit \(\mathrm{false}\).

theorem chkFrom_iff (pq pa : ℕ) (x : List Bool) :
    chkFrom pq pa x = true ↔ ∃ es, x = cells (entryNums es) ∧ keysAscendFrom pq pa es = true
Uses 8 · Used by 1
Statement usesThe cells of a list of numbers · Numbers of a list of entries · Cell-by-cell check of a code stack · Ascending keys of a list of entries
Proof usesReading a unary length prefix · The cell of a number · Reading a unary length prefix reads one cell · Unary counter
Used byThe cell-by-cell check agrees with code-stack decoding

InductiveStacks of the checking machine#✓fully proved

The checking machine has twelve stacks, named \(X, Y, W, V, Q, A, P_Q, P_A, T_1, T_2, J, O\).

inductive K | X | Y | W | V | Q | A | PQ | PA | T1 | T2 | J | O
  deriving DecidableEq
Used by 5
Used byThe checking machine as a host component · The checking machine in polynomial time · Program of the checking machine · The checking run · Stack alphabet of the layout machine

InductiveLabels of the checking machine#✓fully proved

The labels of the checking machine: 23 labels without arguments and four families of labels indexed by the outcome of a comparison (\(<\), \(=\) or \(>\)), 35 distinct labels in all.

inductive Lab
  | dupP | dupQ | cpy | lp | rq0 | rq1 | ra0 | ra1
  | cq | cqR (o : Ordering) | cqRB (o : Ordering) | ca | caR (o : Ordering) | caRB (o : Ordering)
  | sk0 | sk1 | sk2 | sk3 | dr0 | dr1 | mv0 | mv1 | inc | okO | okT | bad | done
  deriving DecidableEq
Used by 6
Used byThe checking machine as a host component · Branch after comparing symbols · Branch after comparing states · The checking machine in polynomial time · Program of the checking machine · The checking run

AbbreviationStack alphabet of the layout machine#✓fully proved

Every stack of the layout machine holds bits: the alphabet of each stack is the type of Booleans.

abbrev Γ : K → Type := fun _ => Bool
Uses 1 · Used by 4
Statement usesStacks of the checking machine
Used byThe checking machine as a host component · The checking machine in polynomial time · Program of the checking machine · The checking run

DefinitionBranch after comparing states#✓fully proved

The label the checking machine goes to after comparing the bound \(p\) for the state (the state of the previous key, or \(0\) at the first entry) with the state \(q\) of the current key: if \(p < q\), the label \(\mathsf{sk0}\), where it starts skipping the rest of the entry; if \(p = q\), the label \(\mathsf{ca}\), where it compares the symbols; if \(p > q\), the label \(\mathsf{bad}\), where it rejects.

def outQ : Ordering → Lab
  | .lt => .sk0
  | .eq => .ca
  | .gt => .bad
Uses 1 · Used by 2
Statement usesLabels of the checking machine
Used byProgram of the checking machine · The checking run

DefinitionBranch after comparing symbols#✓fully proved

The label the checking machine goes to after comparing the bound \(p\) for the symbol with the symbol \(a\) of the current key: if \(p > a\), the label \(\mathsf{bad}\), where it rejects; if \(p < a\) or \(p = a\), the label \(\mathsf{sk0}\), where it starts skipping the rest of the entry.

def outA : Ordering → Lab
  | .gt => .bad
  | _ => .sk0
Uses 1 · Used by 2
Statement usesLabels of the checking machine
Used byProgram of the checking machine · The checking run

DefinitionProgram of the checking machine#✓fully proved

Writing \(1\) for true and \(0\) for false, this is the program of a multi-stack machine whose stacks \(X, Y, W, V, Q, A, P_Q, P_A, T_1, T_2, J, O\) all hold bits. To read a cell from \(V\) onto a stack \(S\) means to pop the leading \(1\)s of \(V\), pushing a \(1\) on \(S\) for each, and then to pop the \(0\) that follows; if \(V\) is empty at that point, the machine rejects. From its first label the program pops the bits of \(X\) one at a time, pushing each onto both \(Y\) and \(W\), and then pops the bits of \(W\) one at a time onto \(V\). Then it loops. If \(V\) is empty, it pops the bits of \(Y\) one at a time onto \(O\), pushes a \(1\) on \(O\) and halts. Otherwise it reads a cell from \(V\) onto \(Q\) and then one onto \(A\). With \(p_Q\), \(q\), \(p_A\), \(a\) the numbers of bits on \(P_Q\), \(Q\), \(P_A\), \(A\), it compares \(p_Q\) with \(q\) and, if they are equal, \(p_A\) with \(a\), afterwards pushing back as many \(1\)s as it popped from each. If \(p_Q > q\), or \(p_Q = q\) and \(p_A > a\), it rejects; otherwise it reads two more cells from \(V\) onto \(J\), empties \(P_Q\) and \(P_A\), moves \(Q\) onto \(P_Q\) and \(A\) onto \(P_A\) (pushing a \(1\) for each bit popped), pushes one more \(1\) on \(P_A\) and loops again. Rejecting pushes a single \(0\) on \(O\) and halts.

Cslib.Turing.Universal.Diag.Check.prog · 30 lines 
def prog : Lab → TM2.Stmt Γ Lab Bool
  | .dupP => .peek .X (fun _ o ↦ o.isSome) (.branch id (.goto fun _ ↦ .dupQ) (.goto fun _ ↦ .cpy))
  | .dupQ => .pop .X (fun _ o ↦ o.getD false) (.branch id
      (.push .Y (fun _ ↦ true) (.push .W (fun _ ↦ true) (.goto fun _ ↦ .dupP)))
      (.push .Y (fun _ ↦ false) (.push .W (fun _ ↦ false) (.goto fun _ ↦ .dupP))))
  | .cpy => moveB .W .V some id .cpy .lp
  | .lp => .peek .V (fun _ o ↦ o.isSome) (.branch id (.goto fun _ ↦ .rq0) (.goto fun _ ↦ .okO))
  | .rq0 => moveB .V .Q dU (fun _ ↦ true) .rq0 .rq1
  | .rq1 => decr .V .bad .ra0
  | .ra0 => moveB .V .A dU (fun _ ↦ true) .ra0 .ra1
  | .ra1 => decr .V .bad .cq
  | .cq => cmpStep .PQ .Q .T1 .T2 true true .cq (.cqR .lt) (.cqR .eq) (.cqR .gt)
  | .cqR o => xfer .T1 [⟨.PQ, true⟩] (.cqR o) (.cqRB o)
  | .cqRB o => xfer .T2 [⟨.Q, true⟩] (.cqRB o) (outQ o)
  | .ca => cmpStep .PA .A .T1 .T2 true true .ca (.caR .lt) (.caR .eq) (.caR .gt)
  | .caR o => xfer .T1 [⟨.PA, true⟩] (.caR o) (.caRB o)
  | .caRB o => xfer .T2 [⟨.A, true⟩] (.caRB o) (outA o)
  | .sk0 => moveB .V .J dU (fun _ ↦ true) .sk0 .sk1
  | .sk1 => decr .V .bad .sk2
  | .sk2 => moveB .V .J dU (fun _ ↦ true) .sk2 .sk3
  | .sk3 => decr .V .bad .dr0
  | .dr0 => xfer .PQ [] .dr0 .dr1
  | .dr1 => xfer .PA [] .dr1 .mv0
  | .mv0 => xfer .Q [⟨.PQ, true⟩] .mv0 .mv1
  | .mv1 => xfer .A [⟨.PA, true⟩] .mv1 .inc
  | .inc => incr .PA true .lp
  | .okO => moveB .Y .O some id .okO .okT
  | .okT => incr .O true .done
  | .bad => emit .O [false] .done
  | .done => .halt
Uses 13 · Used by 3
Statement usesDecoding units · Stacks of the checking machine · Labels of the checking machine · Branch after comparing symbols · Branch after comparing states · Stack alphabet of the layout machine · Flag bit of a machine state · One round of counter comparison · Decrement · Pushing a constant list · Counter increment · Bit-moving loop · Counter transfer loop
Used byThe checking machine as a host component · The checking machine in polynomial time · The checking run

DefinitionAnswer of the checking machine#✓fully proved

For a bit list \(x\), the answer is the list \(x\) with the bit \(\mathrm{true}\) put in front if the cell-by-cell check of \(x\) from the key \((0, 0)\) succeeds, and the one-bit list \([\mathrm{false}]\) otherwise.

def answer (x : List Bool) : List Bool := if chkFrom 0 0 x then true :: x else [false]
Uses 1 · Used by 4
Statement usesCell-by-cell check of a code stack
Used byLayout after checking gives the universal machine's input · The checking machine in polynomial time · The reformatting machine for \(n \mapsto n^2 + 1\) · The checking run

TheoremThe checking run#✓fully proved

For every bit list \(x\), the checking machine, started at the label \(\mathsf{dupP}\) with internal state false, with \(x\) on its input stack \(X\) and every other stack empty, reaches the label \(\mathsf{done}\) within \(33(|x| + 1)^2\) steps, with some internal state and stacks in which the output stack \(O\) holds the answer of the checking machine on \(x\).

theorem run (x : List Bool) :
    ∃ v S', RunLe prog (33 * (x.length + 1) ^ 2)
      ⟨some .dupP, false, update (fun _ ↦ []) .X x⟩ ⟨some .done, v, S'⟩ ∧ S' .O = answer x
Uses 27 · Used by 1
Statement usesStacks of the checking machine · Labels of the checking machine · Answer of the checking machine · Program of the checking machine · Stack alphabet of the layout machine · Runs within a step budget
Proof usesReading a unary length prefix · The cell of a number · Decoding units · Branch after comparing symbols · Branch after comparing states · Cell-by-cell check of a code stack · Reading a unary length prefix reads one cell · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Non-destructive comparison of two counters · Unary counter · Decrement · Pushing a constant list · Counter increment · Bit-moving loop · Running the bit-moving loop · Pushing a list of symbols onto one stack · Running a counter transfer
Used byThe checking machine in polynomial time

AbbreviationThe checking machine as a host component#✓fully proved

The component machine with the twelve stacks \(X, Y, W, V, Q, A, P_Q, P_A, T_1, T_2, J, O\) of the checking machine, each holding bits, with the labels and the program of the checking machine, and with its stacks listed in the order \(X, Y, W, V, Q, A, P_Q, P_A, T_1, T_2, J, O\).

abbrev comp : Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ := fun _ ↦ inferInstanceAs (Fintype Bool)
  L := Lab
  prog := prog
  ks := [.X, .Y, .W, .V, .Q, .A, .PQ, .PA, .T1, .T2, .J, .O]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide
Uses 5 · Used by 1
Statement usesComponent machine · Stacks of the checking machine · Labels of the checking machine · Program of the checking machine · Stack alphabet of the layout machine
Used byThe checking machine in polynomial time

DefinitionThe checking machine in polynomial time#✓fully proved

A finite multi-stack Turing machine with a polynomial time bound that computes the checking answer: given a bit list \(x\) as its input, it halts within the bound, evaluated at \(|x|\), with the checking answer on \(x\) as its output.

noncomputable def polyTime :
    TM2ComputableInPolyTime (fun l : List Bool ↦ l) (fun l : List Bool ↦ l) answer :=
  Complexity.Host.reduction (c := comp) (cX := .X) (cO := .O) (gX := id) (start := .dupP)
    (done := .done) (Equiv.refl Bool) _ (Polynomial.C 33 * (Polynomial.X + 1) ^ 2) rfl
    fun x ↦ by
      obtain ⟨v, S', hr, hO⟩ := run x
      exact ⟨v, S', by simpa [Polynomial.eval_mul, Polynomial.eval_pow] using hr,
        by simpa using hO⟩
Uses 10 · Used by 1
Statement usesComponent machine · Reduction host · Stacks of the checking machine · Labels of the checking machine · Answer of the checking machine · The checking machine as a host component · Program of the checking machine · The checking run · Stack alphabet of the layout machine · Runs within a step budget
Used byThe reformatting machine for \(n \mapsto n^2 + 1\)

InductiveStacks of the layout machine#✓fully proved

The layout machine has twelve stacks, named \(X, Z, P, P_2, U, N, A_2, B_2, D, C, T, O\).

inductive K | X | Z | P | P2 | U | N | A2 | B2 | D | C | T | O
  deriving DecidableEq
Used by 5
Used byThe layout machine as a host component · The layout in polynomial time · Program of the layout machine · The layout run · Stack symbols of the layout machine

InductiveLabels of the layout machine#✓fully proved

The layout machine has 17 labels, named \(\mathsf{s0}\), \(\mathsf{mvZ}\), \(\mathsf{cp0}\), \(\mathsf{cp1}\), \(\mathsf{lo0}\), \(\mathsf{lo1}\), \(\mathsf{lo2}\), \(\mathsf{lo3}\), \(\mathsf{lo4}\), \(\mathsf{mh}\), \(\mathsf{mb}\), \(\mathsf{mk}\), \(\mathsf{mr}\), \(\mathsf{lo5}\), \(\mathsf{lo6}\), \(\mathsf{bad}\) and \(\mathsf{done}\).

inductive Lab
  | s0 | mvZ | cp0 | cp1 | lo0 | lo1 | lo2 | lo3 | lo4 | mh | mb | mk | mr | lo5 | lo6 | bad | done
  deriving DecidableEq
Used by 4
Used byThe layout machine as a host component · The layout in polynomial time · Program of the layout machine · The layout run

AbbreviationStack symbols of the layout machine#✓fully proved

Every stack of the layout machine holds bits: the alphabet of each of its stacks is the type of Booleans.

abbrev Γ : K → Type := fun _ => Bool
Uses 1 · Used by 4
Statement usesStacks of the layout machine
Used byThe layout machine as a host component · The layout in polynomial time · Program of the layout machine · The layout run

DefinitionProgram of the layout machine#✓fully proved

Writing \(1\) for true and \(0\) for false, this is the program of a multi-stack machine whose stacks \(X, Z, P, P_2, U, N, A_2, B_2, D, C, T, O\) all hold bits. To move a stack \(S\) onto a stack \(S'\) means to pop the bits of \(S\) one at a time, pushing each onto \(S'\), until \(S\) is empty; to transfer \(S\) to some stacks means to pop \(S\) until it is empty, pushing a \(1\) on each of these stacks for every bit popped. From the label \(\mathsf{s0}\) the program pops \(X\). If \(X\) was empty or the popped bit is \(0\), it pushes \(0, 0, 1, 1, 0\) on \(O\) in this order and halts. Otherwise it moves \(X\) onto \(Z\), and then, as long as \(Z\) is nonempty, it pops a bit \(b\) from \(Z\), pushes \(b\) on \(U\) and a \(1\) on \(N\), and pushes \(0, 1, 1\) on \(P\) in this order if \(b = 1\) and \(0, 1\) if \(b = 0\). Then it moves \(U\) onto \(O\), pushes a \(0\) on \(O\), moves \(P\) onto \(P_2\) and then \(P_2\) onto \(O\), and transfers \(N\) to \(A_2\) and \(B_2\). Then it loops: it pops \(A_2\); if a bit was popped, it pushes a \(1\) on \(D\), transfers \(B_2\) to \(C\) and \(T\), transfers \(T\) to \(B_2\) and loops again; if \(A_2\) was empty, it transfers \(D\) to \(A_2\). Finally it pushes \(0, 1\) on \(O\) in this order, transfers \(C\) to \(O\) and halts.

Cslib.Turing.Universal.Diag.Layout.prog · 23 lines 
def prog : Lab → TM2.Stmt Γ Lab Bool
  | .s0 => .pop .X (fun _ o ↦ o == some true)
      (.branch id (.goto fun _ ↦ .mvZ) (.goto fun _ ↦ .bad))
  | .mvZ => moveB .X .Z some id .mvZ .cp0
  | .cp0 => .peek .Z (fun _ o ↦ o.isSome) (.branch id (.goto fun _ ↦ .cp1) (.goto fun _ ↦ .lo0))
  | .cp1 => .pop .Z (fun _ o ↦ o.getD false) (.branch id
      (.push .U (fun _ ↦ true) (.push .N (fun _ ↦ true) (.push .P (fun _ ↦ false)
        (.push .P (fun _ ↦ true) (.push .P (fun _ ↦ true) (.goto fun _ ↦ .cp0))))))
      (.push .U (fun _ ↦ false) (.push .N (fun _ ↦ true) (.push .P (fun _ ↦ false)
        (.push .P (fun _ ↦ true) (.goto fun _ ↦ .cp0))))))
  | .lo0 => moveB .U .O some id .lo0 .lo1
  | .lo1 => incr .O false .lo2
  | .lo2 => moveB .P .P2 some id .lo2 .lo3
  | .lo3 => moveB .P2 .O some id .lo3 .lo4
  | .lo4 => xfer .N [⟨.A2, true⟩, ⟨.B2, true⟩] .lo4 .mh
  | .mh => forHead .A2 .D true .mb .mr
  | .mb => xfer .B2 [⟨.C, true⟩, ⟨.T, true⟩] .mb .mk
  | .mk => xfer .T [⟨.B2, true⟩] .mk .mh
  | .mr => xfer .D [⟨.A2, true⟩] .mr .lo5
  | .lo5 => emitR .O [true, false] .lo6
  | .lo6 => xfer .C [⟨.O, true⟩] .lo6 .done
  | .bad => emitR .O [false, true, true, false, false] .done
  | .done => .halt
Uses 9 · Used by 3
Statement usesStacks of the layout machine · Labels of the layout machine · Stack symbols of the layout machine · Flag bit of a machine state · Prepending a constant list · Loop head of a for loop over a counter · Counter increment · Bit-moving loop · Counter transfer loop
Used byThe layout machine as a host component · The layout in polynomial time · The layout run

DefinitionThe layout function#✓fully proved

Write \(\mathrm{cell}(n)\) for the bit list of \(n\) bits \(\mathrm{true}\) followed by one bit \(\mathrm{false}\). On a bit list \(\mathrm{true} :: x\), the layout function returns \(\mathrm{cell}(|x|^2 + 1)\), then the cells \(\mathrm{cell}(s)\) of the symbols \(s\) of the input word of \(x\) (the symbol \(2\) for each bit \(\mathrm{true}\) and \(1\) for each bit \(\mathrm{false}\)), then the bit \(\mathrm{false}\), then the reverse of \(x\). On every other bit list, that is, the empty list or a list starting with \(\mathrm{false}\), it returns the list \([\mathrm{false}, \mathrm{true}, \mathrm{true}, \mathrm{false}, \mathrm{false}]\).

def layout : List Bool → List Bool
  | true :: x => cell (x.length ^ 2 + 1) ++ (cells (input x) ++ (false :: x.reverse))
  | _ => [false, true, true, false, false]
Uses 3 · Used by 4
Statement usesThe cell of a number · The cells of a list of numbers · Input word of a list of bits
Used byLayout after checking gives the universal machine's input · The layout in polynomial time · The reformatting machine for \(n \mapsto n^2 + 1\) · The layout run

TheoremThe layout run#✓fully proved

For every bit list \(y\), the layout machine, started at the label \(\mathsf{s0}\) with internal state false, with \(y\) on its input stack \(X\) and every other stack empty, reaches the label \(\mathsf{done}\) within \(18(|y| + 1)^2\) steps, with some internal state and stacks in which the output stack \(O\) holds the layout of \(y\).

theorem run (y : List Bool) :
    ∃ v S', RunLe prog (18 * (y.length + 1) ^ 2)
      ⟨some .s0, false, update (fun _ ↦ []) .X y⟩ ⟨some .done, v, S'⟩ ∧ S' .O = layout y
Uses 22 · Used by 1
Statement usesStacks of the layout machine · Labels of the layout machine · The layout function · Program of the layout machine · Stack symbols of the layout machine · Runs within a step budget
Proof usesThe cell of a number · The cells of a list of numbers · Symbol of an input bit · Input word of a list of bits · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Unary counter · Pushing a constant list · Prepending a constant list · Counter increment · Running the bit-moving loop · Multiplying unary counters · Pushing a list of symbols onto one stack · Running a counter transfer
Used byThe layout in polynomial time

TheoremThe cell-by-cell check agrees with code-stack decoding#✓fully proved

For every bit list \(x\), the cell-by-cell check of \(x\) from the key \((0, 0)\) succeeds if and only if the decoding of \(x\) as a code stack returns a code.

theorem chkFrom_zero (x : List Bool) : chkFrom 0 0 x = (decodeCodeCells x).isSome
Uses 8 · Used by 1
Statement usesCodes for single-tape machines · Cell-by-cell check of a code stack · Decoding a code stack
Proof usesThe cells of a list of numbers · Numbers of a list of entries · The cell-by-cell check recognizes code stacks · Ascending keys of a list of entries · Code stacks, entry by entry
Used byLayout after checking gives the universal machine's input

AbbreviationThe layout machine as a host component#✓fully proved

The component machine with the twelve stacks \(X, Z, P, P_2, U, N, A_2, B_2, D, C, T, O\) of the layout machine, each holding bits, with the labels and the program of the layout machine, and with its stacks listed in the order \(X, Z, P, P_2, U, N, A_2, B_2, D, C, T, O\).

abbrev comp : Complexity.Host.Comp where
  K := K
  Γ := Γ
  finΓ := fun _ ↦ inferInstanceAs (Fintype Bool)
  L := Lab
  prog := prog
  ks := [.X, .Z, .P, .P2, .U, .N, .A2, .B2, .D, .C, .T, .O]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide
Uses 5 · Used by 1
Statement usesComponent machine · Stacks of the layout machine · Labels of the layout machine · Program of the layout machine · Stack symbols of the layout machine
Used byThe layout in polynomial time

DefinitionThe layout in polynomial time#✓fully proved

A finite multi-stack Turing machine, whose input and output alphabets are identified with the bits, together with a polynomial time bound, that computes the layout function: given a bit list \(y\) as its input, it halts within the bound, evaluated at \(|y|\), with the layout of \(y\) as its output.

noncomputable def polyTime :
    TM2ComputableInPolyTime (fun l : List Bool ↦ l) (fun l : List Bool ↦ l) layout :=
  Complexity.Host.reduction (c := comp) (cX := .X) (cO := .O) (gX := id) (start := .s0)
    (done := .done) (Equiv.refl Bool) _ (Polynomial.C 18 * (Polynomial.X + 1) ^ 2) rfl
    fun y ↦ by
      obtain ⟨v, S', hr, hO⟩ := run y
      exact ⟨v, S', by simpa [Polynomial.eval_mul, Polynomial.eval_pow] using hr,
        by simpa using hO⟩
Uses 10 · Used by 1
Statement usesComponent machine · Reduction host · Stacks of the layout machine · Labels of the layout machine · The layout machine as a host component · The layout function · Program of the layout machine · The layout run · Stack symbols of the layout machine · Runs within a step budget
Used byThe reformatting machine for \(n \mapsto n^2 + 1\)

TheoremLayout after checking gives the universal machine's input#✓fully proved

For every bit list \(x\), let \((c, y, T)\) be the universal machine's argument for the diagonal language of \(f(n) = n^2 + 1\) on \(x\). Then the layout function applied to the checking machine's answer on \(x\) equals the input bit list of the clocked universal machine for the code \(c\), the input \(y\) and the clock \(T\).

theorem layout_answer (x : List Bool) :
    Layout.layout (Check.answer x) =
      encIn (diagArg (fun n ↦ n ^ 2 + 1) x).1 (diagArg (fun n ↦ n ^ 2 + 1) x).2.1
        (diagArg (fun n ↦ n ^ 2 + 1) x).2.2
Uses 12 · Used by 1
Statement usesInput encoding of the clocked universal machine · Codes for single-tape machines · Answer of the checking machine · The layout function · The universal machine's argument for the diagonal language
Proof usesThe cell of a number · The cells of a list of numbers · Cell-by-cell check of a code stack · The cell-by-cell check agrees with code-stack decoding · Decoding a code stack · The reformatting function in bits · Input word of a list of bits
Used byThe reformatting machine for \(n \mapsto n^2 + 1\)

DefinitionThe reformatting machine for \(n \mapsto n^2 + 1\)#✓fully proved

Let \(f(n) = n^2 + 1\). This is a finite multi-stack Turing machine whose input and output alphabets are identified with the bits, together with a polynomial \(p\), such that for every bit list \(x\), started with \(x\) on its input stack it halts within \(p(|x|)\) steps with output the clocked universal machine's input bits for the universal machine's argument \((c, w, T)\) for the diagonal language of \(f\) at \(x\): the clock \(T\) as a cell, the cells of the input symbols of \(w\), a blank cell and the code stack of \(c\) reversed. It runs the checking machine and then the layout machine.

noncomputable def reformat :
    TM2ComputableInPolyTime (fun x : List Bool ↦ x)
      (fun a : Code × List Bool × ℕ ↦ encIn a.1 a.2.1 a.2.2) (diagArg (fun n ↦ n ^ 2 + 1)) :=
  let H := MetaMathlibExt.TM2Composition.compComputable Check.polyTime Layout.polyTime
  { toTM2ComputableAux := H.toTM2ComputableAux
    time := H.time
    outputsFun := fun x ↦ by
      have h := H.outputsFun x
      simp only [Function.comp_apply, layout_answer] at h
      exact h }
Uses 9 · Used by 1
Statement usesInput encoding of the clocked universal machine · Codes for single-tape machines · Answer of the checking machine · The checking machine in polynomial time · The layout function · The layout in polynomial time · Layout after checking gives the universal machine's input · The universal machine's argument for the diagonal language · The composite polynomial-time TM2 computation
Used byDeciding the diagonal language on raw bits in polynomial time

TheoremDeciding the diagonal language on raw bits in polynomial time#✓fully proved

Let \(D\) be the diagonal language for the time bound \(f(n) = n^2 + 1\). There is a finite multi-stack Turing machine that, given a bit list \(x\) as its input, halts within a number of steps polynomial in \(|x|\) with the single bit \(D(x)\) as its output.

theorem nonempty_diag_sq_add_one_polyTime :
    Nonempty (TM2ComputableInPolyTime (fun x : List Bool ↦ x) (fun b : Bool ↦ [b])
      (diag (fun n ↦ n ^ 2 + 1)))
Uses 3 · Used by 1
Statement usesThe diagonal language
Proof usesThe reformatting machine for \(n \mapsto n^2 + 1\) · The diagonal language in polynomial time, given the reformatting machine
Used byThe quadratic diagonal language is in P

TheoremThe quadratic diagonal language is in P#✓fully proved

The diagonal language for the time bound \(f(n) = n^2 + 1\), the set of bit lists \(x\) that encode a code which does not halt on \(x\) within \(|x|^2 + 1\) steps with the answer \(\mathrm{true}\), is in the class P of decision problems decidable in polynomial time.

The decider decodes the canonical encoding of bit lists and then runs a polynomial-time decider on the raw bits.

theorem diag_sq_add_one_mem_P : diag (fun n ↦ n ^ 2 + 1) ∈ P
Uses 15 · Used by 2
Statement usesThe diagonal language · Complexity classes · Decision problems · The complexity class P
Proof usesPolynomial-time decoder of the canonical bit-list encoding · Deciding the diagonal language on raw bits in polynomial time · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time TM2-computable functions are closed under composition
Used byDiagonalization across models · Polynomial time is not contained in code time \(n^2 + 1\)

TheoremDiagonalization across models#✓fully proved

There is a decision problem in the class P that no code decides within \(n^2 + 1\) steps: no code halts on every input \(x\) within \(|x|^2 + 1\) steps with the answer for \(x\) as its output.

The diagonal language for the time bound \(n \mapsto n^2 + 1\) is such a problem. The class of problems that codes decide within \(n^2 + 1\) steps is not empty: it contains the problem whose answer is always \(\mathrm{false}\).

theorem exists_mem_P_not_mem_codeTime_sq_add_one :
    ∃ L ∈ P, L ∉ CodeTime (fun n ↦ n ^ 2 + 1)
Uses 7
Statement usesTime classes on codes · Complexity classes · Decision problems · The complexity class P
Proof usesThe diagonal language · The diagonal argument · The quadratic diagonal language is in P

TheoremPolynomial time is not contained in code time \(n^2 + 1\)#✓fully proved

Some decision problem in \(\mathsf{P}\) is decided by no code within \(n^2 + 1\) steps on every input of length \(n\); that is, \(\mathsf{P}\) is not a subset of the class \(\mathrm{CodeTime}(n \mapsto n^2 + 1)\).

theorem not_P_subset_codeTime_sq_add_one : ¬ P ⊆ CodeTime (fun n ↦ n ^ 2 + 1)
Uses 7
Statement usesTime classes on codes · Complexity classes · Decision problems · The complexity class P
Proof usesThe diagonal language · The diagonal argument · The quadratic diagonal language is in P

TheoremThere is an EXP language outside P (time-hierarchy separation)#●ready to prove

There is a decision problem that belongs to the class EXP but not to the complexity class P.

Only this separation is stated; the containment of P in EXP is not part of the statement.

public theorem_wanted p_ne_exp :
    ∃ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ EXP ∧ L ∉ MetaMathlibExt.ComplexityTheory.P
Sources
  • J. Hartmanis and R. E. Stearns, "On the computational complexity of algorithms", Transactions of the American Mathematical Society 117 (1965), 285-306; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Corollary 3.5.
Uses 4
Statement usesThe class EXP · Complexity classes · Decision problems · The complexity class P

TheoremDeterministic time hierarchy: quadratic versus linear time#●ready to prove

There is a language \(L\) of bitstrings that lies in the multi-tape deterministic time class \(\mathrm{DTIME}(n^2)\) but not in \(\mathrm{DTIME}(n)\).

public theorem_wanted time_hierarchy :
    ∃ L : Set (List Bool), L ∈ Cslib.Turing.MultiTapeTM.DTIME (fun n => n ^ 2) ∧
      L ∉ Cslib.Turing.MultiTapeTM.DTIME (fun n => n)
Sources
  • J. Hartmanis and R. E. Stearns, "On the computational complexity of algorithms", Transactions of the American Mathematical Society 117 (1965), 285-306.
Uses 1
Statement usesDeterministic time classes on multi-tape machines
68 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.