Clocked universal Turing machine

DefinitionThe cell of a number#✓fully proved

The cell of a natural number \(n\) is the list of bits consisting of \(n\) copies of the bit true (units) followed by one bit false (a marker).

def cell (n : ℕ) : List Bool := cnt true n ++ [false]

Uses 1 · Used by 25

Statement 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 · The diagonal answer read from the encoded output · The diagonal language through the universal machine · The reformatting function in bits · Code stacks are recognized · Code stacks, entry by entry · The layout function · Layout after checking gives the universal machine's input · The code stack determines the table lookups · Reading a unary length prefix reads one cell · The checking run · The layout run · The tape update · The cells of a list of numbers · Input encoding of the clocked universal machine · The clocked loop · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case · Correctness and running time of the clocked universal machine · The step bound of the clocked universal machine is quadratic

DefinitionThe cells of a list of numbers#✓fully proved

The cells of a list \((n_1, \ldots, n_m)\) of natural numbers are the concatenation of the cells of \(n_1, \ldots, n_m\) in this order, so that the cell of \(n_1\) comes first (on top of a stack).

def cells (l : List ℕ) : List Bool := l.flatMap cell

Uses 1 · Used by 25

Statement usesThe cell of a number

Used byThe cell-by-cell check recognizes code stacks · The cell-by-cell check agrees with code-stack decoding · Decoding inverts the code stack · The diagonal answer read from the encoded output · The diagonal language through the universal machine · The reformatting function in bits · Code stacks are recognized · Code stacks, entry by entry · The layout function · Layout after checking gives the universal machine's input · The code stack determines the table lookups · The layout run · The tape update · The code stack · Input encoding of the clocked universal machine · Output encoding of the clocked universal machine · The clocked loop · Writing the output · Reading the input · Cost of reading the input · One simulated step, halting case · One simulated step, running case · The stacks of a simulated configuration · Correctness and running time of the clocked universal machine · The step bound of the clocked universal machine is quadratic

InductiveStacks of the clocked universal machine#✓fully proved

The clocked universal machine has fifteen stacks: the state \(Q\), the next state \(N\), the action \(A\) and the head cell \(H\) (these four hold counters of units), the cells left (\(L\)) and right (\(R\)) of the head, the code \(C\), the scan buffer \(B\), the scratch counters \(T\), \(U\), \(V\), the clock \(\mathrm{Ck}\), and the parsing stacks: the encoded input \(X\), the parse buffer \(P\) and the output \(O\).

inductive K | Q | N | A | H | L | R | C | B | T | U | V | Ck | X | P | O
  deriving DecidableEq

Used by 15

Used byThe tape update · The clocked universal machine on stacks · The clocked loop · Moving a marker onto the scan buffer · The clocked universal function is polynomial-time computable · Writing the output · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case · The stacks of a simulated configuration · Writing a timeout · The clocked universal machine as a host component · Correctness and running time of the clocked universal machine · Stack alphabet of the clocked universal machine

InductiveLabels of the clocked universal machine#✓fully proved

The labels of the program of the clocked universal machine: the tape update (act0–act3, wr0, wr1, mvL0–mvL3, mvR0–mvR3) and the clock tick fin; the scan, which starts at sc0 and has labels for the state (rq0–rq2; cqA o and cqB o for each comparison outcome o; sq0 m and sq1 m for each bit m), for the head cell (ra0–ra2; caA o, caB o; sa0 m, sa1 m), for skipping the rest of an entry (sk3a, sk3b, sk2a, sk2b, sk1a, sk1b) and for reading a match (rd0–rd7); the restores rs and nf; the exits hlt and tmo; the parse of the encoded input (pc0, pc1, px0–px6, pk0); and the output phase (o1–o6, done).

inductive Lab
  | act0 | act1 | act2 | act3 | wr0 | wr1 | mvL0 | mvL1 | mvL2 | mvL3 | mvR0 | mvR1 | mvR2 | mvR3
  | fin
  | sc0 | rq0 | rq1 | rq2 | cqA (o : Ordering) | cqB (o : Ordering)
  | sq0 (m : Bool) | sq1 (m : Bool)
  | ra0 | ra1 | ra2 | caA (o : Ordering) | caB (o : Ordering) | sa0 (m : Bool) | sa1 (m : Bool)
  | sk3a | sk3b | sk2a | sk2b | sk1a | sk1b
  | rd0 | rd1 | rd2 | rd3 | rd4 | rd5 | rd6 | rd7
  | rs | nf | hlt | tmo
  | pc0 | pc1 | px0 | px1 | px2 | px3 | px4 | px5 | px6 | pk0
  | o1 | o2 | o3 | o4 | o5 | o6 | done
  deriving DecidableEq

Used by 13

Used byThe tape update · The clocked universal machine on stacks · The clocked loop · Moving a marker onto the scan buffer · The clocked universal function is polynomial-time computable · Writing the output · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case · Writing a timeout · The clocked universal machine as a host component · Correctness and running time of the clocked universal machine

AbbreviationStack alphabet of the clocked universal machine#✓fully proved

Every stack \(k\) of the clocked universal machine holds bits: its alphabet is \(\Gamma(k) = \mathrm{Bool}\).

abbrev Γ : K → Type := fun _ => Bool

Uses 1 · Used by 14

Statement usesStacks of the clocked universal machine

Used byThe tape update · The clocked universal machine on stacks · The clocked loop · Moving a marker onto the scan buffer · The clocked universal function is polynomial-time computable · Writing the output · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case · The stacks of a simulated configuration · Writing a timeout · The clocked universal machine as a host component · Correctness and running time of the clocked universal machine

DefinitionDecoding units#✓fully proved

The unit decoder sends the bit true (a unit) to the bit true, and sends the bit false (a marker) to no bit, which ends a block.

def dU (b : Bool) : Option Bool := if b then some true else none

Used by 7

Used byProgram of the checking machine · The checking run · The tape update · Reading the input · The clocked universal program · One simulated step, halting case · One simulated step, running case

DefinitionMoving a marker onto the scan buffer#✓fully proved

For a label \(\ell\), this instruction pops the top symbol of the code stack \(C\) and discards it (doing nothing if \(C\) is empty), pushes a marker (the bit false) onto the scan buffer \(B\), and goes to \(\ell\); the state bit is unchanged.

def mark (next : Lab) : TM2.Stmt Γ Lab Bool :=
  .pop .C (fun v _ ↦ v) (.push .B (fun _ ↦ false) (.goto fun _ ↦ next))

Uses 3 · Used by 3

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Stack alphabet of the clocked universal machine

Used byThe clocked universal program · One simulated step, halting case · One simulated step, running case

DefinitionThe clocked universal program#✓fully proved

The program of the clocked universal machine gives an instruction for every label. Numbers sit on stacks as counters of units (the bit true), and a cell is a counter followed by a marker (the bit false).

Tape update. \(\mathsf{act0}\) empties \(Q\) and \(\mathsf{act1}\) moves the counter \(N\) onto \(Q\). \(\mathsf{act2}\) pops \(A\) and goes to \(\mathsf{mvL0}\) if \(A\) was empty, else to \(\mathsf{act3}\), which pops \(A\) and goes to \(\mathsf{mvR0}\) if \(A\) was empty, else to \(\mathsf{wr0}\); so the action \(0\) moves left, \(1\) moves right and \(a + 2\) writes \(a\). \(\mathsf{wr0}\) empties \(H\) and \(\mathsf{wr1}\) moves the counter \(A\) onto \(H\). A left move (\(\mathsf{mvL0}\) to \(\mathsf{mvL3}\)) pushes a marker on \(R\), moves the units of \(H\) onto \(R\), moves the units on top of \(L\) onto \(H\) and pops one more symbol of \(L\); a right move (\(\mathsf{mvR0}\) to \(\mathsf{mvR3}\)) does the same with \(L\) and \(R\) exchanged. Writes and moves end at \(\mathsf{fin}\), which pops the clock \(Ck\) and goes to \(\mathsf{tmo}\) if it was empty, else to \(\mathsf{sc0}\).

Scan. \(\mathsf{sc0}\) goes to \(\mathsf{nf}\) if \(C\) is empty, else to \(\mathsf{rq0}\). Then \(\mathsf{rq0}\), \(\mathsf{rq1}\) move the units on top of \(C\) onto \(T\) and pop the next symbol of \(C\); \(\mathsf{rq2}\) compares \(T\) with \(Q\) unit by unit, parking the popped units on \(U\) and \(V\); \(\mathsf{cqA}\), \(\mathsf{cqB}\) move \(U\) back onto \(T\) and \(V\) back onto \(Q\); \(\mathsf{sq0}\), \(\mathsf{sq1}\) move \(T\) onto \(B\), push a marker on \(B\), and go to \(\mathsf{ra0}\) if the two counters were equal, else to \(\mathsf{sk3a}\). The labels \(\mathsf{ra0}\) to \(\mathsf{sa1}\) do the same with \(H\) in place of \(Q\), and go to \(\mathsf{rd0}\) on equality, else to \(\mathsf{sk2a}\). From \(\mathsf{sk3a}\), \(\mathsf{sk2a}\) or \(\mathsf{sk1a}\) the program moves three, two or one further cells of \(C\) onto \(B\) (the units, then the next symbol replaced by a marker) and returns to \(\mathsf{sc0}\). The labels \(\mathsf{rd0}\) to \(\mathsf{rd3}\) move the units on top of \(C\) onto both \(N\) and \(B\), pop the next symbol of \(C\) and push a marker on \(B\); \(\mathsf{rd4}\) to \(\mathsf{rd7}\) do the same with \(A\) in place of \(N\) and go to \(\mathsf{rs}\). Finally \(\mathsf{rs}\) and \(\mathsf{nf}\) move all of \(B\) back onto \(C\), one symbol at a time, and go to \(\mathsf{act0}\) and \(\mathsf{hlt}\) respectively.

Parse. \(\mathsf{pc0}\), \(\mathsf{pc1}\) move the units on top of \(X\) onto \(Ck\) and pop the next symbol of \(X\). Then, while the top of \(X\) is a unit, \(\mathsf{px0}\) to \(\mathsf{px2}\) move the units on top of \(X\) onto \(P\), pop the next symbol of \(X\) and push a marker on \(P\); otherwise \(\mathsf{px3}\) pops \(X\), \(\mathsf{px4}\) moves all of \(P\) onto \(R\), \(\mathsf{px5}\), \(\mathsf{px6}\) move the units on top of \(R\) onto \(H\) and pop the next symbol of \(R\), and \(\mathsf{pk0}\) moves all of \(X\) onto \(C\) and goes to \(\mathsf{sc0}\).

Exits. \(\mathsf{tmo}\) pushes a marker on \(O\) and goes to \(\mathsf{done}\). \(\mathsf{hlt}\) pushes a marker on \(R\), \(\mathsf{o1}\) moves the units of \(H\) onto \(R\), \(\mathsf{o2}\) moves all of \(R\) onto \(P\), \(\mathsf{o3}\) pops the markers on top of \(P\), \(\mathsf{o4}\) pushes one marker on \(P\) unless \(P\) is empty, \(\mathsf{o5}\) moves all of \(P\) onto \(O\), and \(\mathsf{o6}\) pushes a unit on \(O\) and goes to \(\mathsf{done}\), where the program halts.

Cslib.Turing.Universal.Clocked.prog · 68 lines

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .act0 => xfer .Q [] .act0 .act1
  | .act1 => xfer .N [⟨.Q, true⟩] .act1 .act2
  | .act2 => decr .A .mvL0 .act3
  | .act3 => decr .A .mvR0 .wr0
  | .wr0 => xfer .H [] .wr0 .wr1
  | .wr1 => xfer .A [⟨.H, true⟩] .wr1 .fin
  | .mvL0 => incr .R false .mvL1
  | .mvL1 => xfer .H [⟨.R, true⟩] .mvL1 .mvL2
  | .mvL2 => moveB .L .H dU (fun _ => true) .mvL2 .mvL3
  | .mvL3 => decr .L .fin .fin
  | .mvR0 => incr .L false .mvR1
  | .mvR1 => xfer .H [⟨.L, true⟩] .mvR1 .mvR2
  | .mvR2 => moveB .R .H dU (fun _ => true) .mvR2 .mvR3
  | .mvR3 => decr .R .fin .fin
  | .fin => decr .Ck .tmo .sc0
  | .sc0 => .peek .C (fun _ o ↦ o.isSome) (.branch id (.goto fun _ ↦ .rq0) (.goto fun _ ↦ .nf))
  | .rq0 => moveB .C .T dU (fun _ ↦ true) .rq0 .rq1
  | .rq1 => decr .C .rq2 .rq2
  | .rq2 => cmpStep .T .Q .U .V true true .rq2 (.cqA .lt) (.cqA .eq) (.cqA .gt)
  | .cqA o => xfer .U [⟨.T, true⟩] (.cqA o) (.cqB o)
  | .cqB o => xfer .V [⟨.Q, true⟩] (.cqB o) (.sq0 (decide (o = .eq)))
  | .sq0 m => xfer .T [⟨.B, true⟩] (.sq0 m) (.sq1 m)
  | .sq1 m => incr .B false (if m then .ra0 else .sk3a)
  | .ra0 => moveB .C .T dU (fun _ ↦ true) .ra0 .ra1
  | .ra1 => decr .C .ra2 .ra2
  | .ra2 => cmpStep .T .H .U .V true true .ra2 (.caA .lt) (.caA .eq) (.caA .gt)
  | .caA o => xfer .U [⟨.T, true⟩] (.caA o) (.caB o)
  | .caB o => xfer .V [⟨.H, true⟩] (.caB o) (.sa0 (decide (o = .eq)))
  | .sa0 m => xfer .T [⟨.B, true⟩] (.sa0 m) (.sa1 m)
  | .sa1 m => incr .B false (if m then .rd0 else .sk2a)
  | .sk3a => moveB .C .B dU (fun _ ↦ true) .sk3a .sk3b
  | .sk3b => mark .sk2a
  | .sk2a => moveB .C .B dU (fun _ ↦ true) .sk2a .sk2b
  | .sk2b => mark .sk1a
  | .sk1a => moveB .C .B dU (fun _ ↦ true) .sk1a .sk1b
  | .sk1b => mark .sc0
  | .rd0 => moveB .C .T dU (fun _ ↦ true) .rd0 .rd1
  | .rd1 => decr .C .rd2 .rd2
  | .rd2 => xfer .T [⟨.N, true⟩, ⟨.B, true⟩] .rd2 .rd3
  | .rd3 => incr .B false .rd4
  | .rd4 => moveB .C .T dU (fun _ ↦ true) .rd4 .rd5
  | .rd5 => decr .C .rd6 .rd6
  | .rd6 => xfer .T [⟨.A, true⟩, ⟨.B, true⟩] .rd6 .rd7
  | .rd7 => incr .B false .rs
  | .rs => moveB .B .C some id .rs .act0
  | .nf => moveB .B .C some id .nf .hlt
  | .hlt => incr .R false .o1
  | .tmo => incr .O false .done
  | .pc0 => moveB .X .Ck dU (fun _ ↦ true) .pc0 .pc1
  | .pc1 => decr .X .px0 .px0
  | .px0 => .peek .X (fun _ o ↦ isBit dU o) (.branch id (.goto fun _ ↦ .px1) (.goto fun _ ↦ .px3))
  | .px1 => moveB .X .P dU (fun _ ↦ true) .px1 .px2
  | .px2 => .pop .X (fun v _ ↦ v) (.push .P (fun _ ↦ false) (.goto fun _ ↦ .px0))
  | .px3 => decr .X .px4 .px4
  | .px4 => moveB .P .R some id .px4 .px5
  | .px5 => moveB .R .H dU (fun _ ↦ true) .px5 .px6
  | .px6 => decr .R .pk0 .pk0
  | .pk0 => moveB .X .C some id .pk0 .sc0
  | .o1 => xfer .H [⟨.R, true⟩] .o1 .o2
  | .o2 => moveB .R .P some id .o2 .o3
  | .o3 => .peek .P (fun _ o ↦ o == some false)
      (.branch id (.pop .P (fun v _ ↦ v) (.goto fun _ ↦ .o3)) (.goto fun _ ↦ .o4))
  | .o4 => .peek .P (fun _ o ↦ o.isSome)
      (.branch id (.push .P (fun _ ↦ false) (.goto fun _ ↦ .o5)) (.goto fun _ ↦ .o5))
  | .o5 => moveB .P .O some id .o5 .o6
  | .o6 => incr .O true .done
  | .done => .halt

Uses 12 · Used by 11

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Decoding units · Moving a marker onto the scan buffer · Stack alphabet of the clocked universal machine · Flag bit of a machine state · One round of counter comparison · Decrement · Counter increment · Bit test for the top of a stack · Bit-moving loop · Counter transfer loop

Used byThe tape update · The clocked universal machine on stacks · The clocked loop · The clocked universal function is polynomial-time computable · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case · Writing a timeout · The clocked universal machine as a host component · Correctness and running time of the clocked universal machine

DefinitionEntries of a code#✓fully proved

For a code \(c\), the list of quadruples \((q, a, q', s)\), one for each state \(q\) and symbol \(a\) inside the table of \(c\) whose table entry is a transition \((q', s)\) (enter the state \(q'\) and do the action coded by \(s\)); halting positions are skipped. The quadruples are listed row by row, by increasing \(q\), and within a row by increasing \(a\).

def entries (c : Code) : List (ℕ × ℕ × ℕ × ℕ) :=
  (List.range c.table.length).flatMap fun q ↦
    (List.range (c.table.getD q []).length).filterMap fun a ↦
      (c.lookup q a).map fun e ↦ (q, a, e.1, e.2)

Uses 2 · Used by 9

Statement usesCodes for single-tape machines · Table lookup of a code

Used byDecoding inverts the code stack · Code stacks are recognized · The code stack determines the table lookups · The code stack · Scanning the entries finds the table entry · The clocked loop · One simulated step, halting case · One simulated step, running case · Correctness and running time of the clocked universal machine

DefinitionLooking up a key in a list of entries#✓fully proved

For natural numbers \(q\) and \(a\) and a list of quadruples \((q_i, a_i, q'_i, s_i)\) of natural numbers, the result is the pair \((q'_i, s_i)\) of the first quadruple in the list with \(q_i = q\) and \(a_i = a\), and no result if no quadruple has the key \((q, a)\). This is the order in which the machine scans the code stack.

def findEntry (q a : ℕ) : List (ℕ × ℕ × ℕ × ℕ) → Option (ℕ × ℕ)
  | [] => none
  | e :: es => if e.1 = q ∧ e.2.1 = a then some (e.2.2.1, e.2.2.2) else findEntry q a es

Used by 6

Used byDecoding inverts the code stack · The code of a list of entries · The code stack determines the table lookups · Scanning the entries finds the table entry · One simulated step, halting case · One simulated step, running case

TheoremScanning the entries finds the table entry#✓fully proved

For every code \(c\) and all natural numbers \(q\) and \(a\), looking up the key \((q, a)\) in the entries of \(c\) gives the entry of the table of \(c\) at state \(q\) and symbol \(a\): the pair \((q', s)\) if that position holds the transition \((q', s)\), and no result if it halts, including every position outside the table.

theorem findEntry_entries (c : Code) (q a : ℕ) : findEntry q a (entries c) = c.lookup q a

Uses 4 · Used by 4

Statement usesEntries of a code · Looking up a key in a list of entries · Codes for single-tape machines · Table lookup of a code

Used byDecoding inverts the code stack · The code stack determines the table lookups · One simulated step, halting case · One simulated step, running case

DefinitionNumbers of a list of entries#✓fully proved

For a list of quadruples of natural numbers, the list of natural numbers obtained by replacing each quadruple \((q, a, q', s)\) by the four numbers \(q, a, q', s\) in this order, keeping the order of the quadruples.

def entryNums (es : List (ℕ × ℕ × ℕ × ℕ)) : List ℕ :=
  es.flatMap fun e ↦ [e.1, e.2.1, e.2.2.1, e.2.2.2]

Used by 11

Used byThe cell-by-cell check recognizes code stacks · The cell-by-cell check agrees with code-stack decoding · Decoding inverts the code stack · Code stacks are recognized · Code stacks, entry by entry · The code stack determines the table lookups · The code stack · The clocked loop · One simulated step, halting case · One simulated step, running case · Correctness and running time of the clocked universal machine

DefinitionThe code stack#✓fully proved

The code stack of a code \(c\) is the list of bits formed by the cells of the numbers \(q, a, q', s\) of every entry \((q, a, q', s)\) of \(c\) (a table position \((q, a)\) holding the transition \((q', s)\)), with the entries ordered by \(q\) and then by \(a\), and the four numbers of an entry in the order \(q, a, q', s\).

def codeCells (c : Code) : List Bool := cells (entryNums (entries c))

Uses 4 · Used by 25

Statement usesThe cells of a list of numbers · Entries of a code · Numbers of a list of entries · Codes for single-tape machines

Used byDecoding inverts the code stack · Code stacks decode to codes with the same code stack · The diagonal language on a code stack · The diagonal language through the universal machine · Bit lists that encode no code are outside the diagonal language · The diagonal argument · The reformatting function in bits · The code stack determines the clocked semantics · Code stacks are recognized · The code stack determines the table lookups · The tape update · Step bound of the clocked simulation · The clocked universal machine on stacks · Input encoding of the clocked universal machine · The clocked loop · Step bound of the clocked loop · Reading the input · Cost of reading the input · One simulated step, halting case · One simulated step, running case · Step bound of one simulated step · The stacks of a simulated configuration · Correctness and running time of the clocked universal machine · Step bound of the clocked universal machine · The step bound of the clocked universal machine is quadratic

DefinitionThe stacks of a simulated configuration#✓fully proved

For a code \(c\), a natural number \(t\) (the clock), a configuration \(k\) and natural numbers \(q'\) and \(s\), the stacks of \(c\), \(t\) and \(k\) with next state \(q'\) and action \(s\) hold, as counters of units (the bit true): the state of \(k\) on \(Q\), \(q'\) on \(N\), \(s\) on \(A\), the head symbol of \(k\) on \(H\) and \(t\) on \(Ck\). The stacks \(L\) and \(R\) hold the cells of the symbols left and right of the head, nearest first, \(C\) holds the code stack of \(c\), and every other stack is empty.

def stk (c : Code) (t : ℕ) (k : Code.Cfg) (q' s : ℕ) : ∀ j, List (Γ j)
  | .Q => cnt true k.q
  | .N => cnt true q'
  | .A => cnt true s
  | .H => cnt true k.head
  | .L => cells k.left
  | .R => cells k.right
  | .C => codeCells c
  | .Ck => cnt true t
  | _ => []

Uses 7 · Used by 9

Statement usesStacks of the clocked universal machine · The cells of a list of numbers · The code stack · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · Unary counter

Used byThe tape update · The clocked universal machine on stacks · The clocked loop · Writing the output · Reading the input · One simulated step, halting case · One simulated step, running case · Writing a timeout · Correctness and running time of the clocked universal machine

DefinitionStep bound of the tape update#✓fully proved

For a configuration \(k\) with state \(q\), head cell \(h\), cells \(\ell\) left of the head and cells \(r\) right of the head (nearest first), a next state \(q'\) and an action \(s\), the step bound of the tape update is \(q + q' + s + h + \ell_0 + r_0 + 8\), where \(\ell_0\) and \(r_0\) are the first entries of \(\ell\) and \(r\), taken to be \(0\) for an empty list.

def actTime (k : Code.Cfg) (q' s : ℕ) : ℕ :=
  k.q + q' + s + k.head + k.left.headI + k.right.headI + 8

Uses 1 · Used by 2

Statement usesExplicit configurations

Used byThe tape update · One simulated step, running case

TheoremThe tape update#✓fully proved

Let \(c\) be a code, \(k\) a configuration and \(t\), \(q'\), \(s\) natural numbers. Started at the label \(\mathsf{act0}\), with any value of its internal variable, on the stacks holding the code \(c\), the clock \(t\) and the configuration \(k\), with \(q'\) on the next-state stack, \(s\) on the action stack and all other stacks empty, the program of the clocked universal machine reaches the label \(\mathsf{fin}\), with some value of its internal variable, on the stacks holding \(c\), \(t\) and the configuration obtained from \(k\) by entering the state \(q'\) and doing the action coded by \(s\), with the next-state, action and all other stacks empty. It does so in at most as many steps as the step bound of the tape update for \(k\), \(q'\) and \(s\).

theorem act_run (c : Code) (t : ℕ) (k : Code.Cfg) (q' s : ℕ) (v : Bool) :
    ∃ v', RunLe prog (actTime k q' s) ⟨some .act0, v, stk c t k q' s⟩
      ⟨some .fin, v', stk c t (k.act q' s) 0 0⟩

Uses 25 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Step bound of the tape update · The clocked universal program · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · Acting on a configuration · Runs within a step budget

Proof usesThe cell of a number · The cells of a list of numbers · The code stack · Decoding units · End of a bit block · 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 · Unary counter · Decrement · Counter increment · Running the bit-moving loop · Running a counter transfer

Used byOne simulated step, running case

DefinitionCost of scanning past one entry#✓fully proved

The step budget for scanning past an entry \((q, a, q', s)\) of the code stack is \(5q + 5a + 2q' + 2s + 30\).

def entryCost (e : ℕ × ℕ × ℕ × ℕ) : ℕ := 5 * e.1 + 5 * e.2.1 + 2 * e.2.2.1 + 2 * e.2.2.2 + 30

Used by 2

Used byOne simulated step, halting case · One simulated step, running case

DefinitionStep bound of one simulated step#✓fully proved

For a code \(c\) and a configuration \(k\) with state \(q\), head cell \(h\), nearest left cell \(l\) and nearest right cell \(r\) (each read as the blank \(0\) when there is no such cell), let \(|C|\) be the length of the code stack of \(c\). The step bound of \(c\) at \(k\) is \(10|C| + q + h + l + r + 10\).

def stepTime (c : Code) (k : Code.Cfg) : ℕ :=
  10 * (codeCells c).length + k.q + k.head + k.left.headI + k.right.headI + 10

Uses 3 · Used by 3

Statement usesThe code stack · Codes for single-tape machines · Explicit configurations

Used byThe clocked loop · One simulated step, halting case · One simulated step, running case

TheoremOne simulated step, running case#✓fully proved

Let \(c\) be a code, \(k\) and \(k'\) configurations such that one step of \(c\) from \(k\) gives \(k'\), \(t\) a natural number, \(v\) a bit, and \(b\) the step bound of \(c\) at \(k\). Started at the label \(\mathsf{sc0}\) with state bit \(v\) and the stacks of the code \(c\), the clock \(t\) and the configuration \(k\) with next state and action \(0\), the clocked universal program reaches the label \(\mathsf{fin}\) within \(b\) steps, with some state bit and the stacks of \(c\), \(t\) and \(k'\) with next state and action \(0\).

theorem step_run_of_step_eq_some {c : Code} {k k' : Code.Cfg} (h : c.step k = some k') (t : ℕ)
    (v : Bool) :
    ∃ v', RunLe prog (stepTime c k) ⟨some .sc0, v, stk c t k 0 0⟩
      ⟨some .fin, v', stk c t k' 0 0⟩

Uses 37 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · The clocked universal program · Step bound of one simulated step · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · One step of a code · Runs within a step budget

Proof usesStep bound of the tape update · The tape update · The cell of a number · The cells of a list of numbers · The code stack · Decoding units · Entries of a code · Cost of scanning past one entry · Numbers of a list of entries · Looking up a key in a list of entries · Scanning the entries finds the table entry · Moving a marker onto the scan buffer · Acting on a configuration · Table lookup of a code · 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 · Counter increment · Bit-moving loop · Running the bit-moving loop · Counter transfer loop · Running a counter transfer

Used byThe clocked loop

TheoremOne simulated step, halting case#✓fully proved

Let \(c\) be a code, \(k\) a configuration at which \(c\) halts (one step of \(c\) from \(k\) gives nothing), \(t\) a natural number, \(v\) a bit, and \(b\) the step bound of \(c\) at \(k\). Started at the label \(\mathsf{sc0}\) with state bit \(v\) and the stacks of the code \(c\), the clock \(t\) and the configuration \(k\) with next state and action \(0\), the clocked universal program reaches the label \(\mathsf{hlt}\) within \(b\) steps, with some state bit and the same stacks.

theorem step_run_of_step_eq_none {c : Code} {k : Code.Cfg} (h : c.step k = none) (t : ℕ)
    (v : Bool) :
    ∃ v', RunLe prog (stepTime c k) ⟨some .sc0, v, stk c t k 0 0⟩
      ⟨some .hlt, v', stk c t k 0 0⟩

Uses 35 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · The clocked universal program · Step bound of one simulated step · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · One step of a code · Runs within a step budget

Proof usesThe cell of a number · The cells of a list of numbers · The code stack · Decoding units · Entries of a code · Cost of scanning past one entry · Numbers of a list of entries · Looking up a key in a list of entries · Scanning the entries finds the table entry · Moving a marker onto the scan buffer · Acting on a configuration · Table lookup of a code · 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 · Counter increment · Bit-moving loop · Running the bit-moving loop · Counter transfer loop · Running a counter transfer

Used byThe clocked loop

DefinitionConfigurations bounded by \(M\)#✓fully proved

A configuration \(k\) is bounded by a natural number \(M\) when its state, its head cell and every cell left and right of the head are at most \(M\).

def Bounded (M : ℕ) (k : Code.Cfg) : Prop :=
  k.q ≤ M ∧ k.head ≤ M ∧ (∀ a ∈ k.left, a ≤ M) ∧ ∀ a ∈ k.right, a ≤ M

Uses 1 · Used by 3

Statement usesExplicit configurations

Used byThe clocked universal machine on stacks · The clocked loop · Correctness and running time of the clocked universal machine

DefinitionStep bound of the clocked loop#✓fully proved

For a code \(c\) and a number \(M\), the loop step time is \(10\ell + 4M + 11\), where \(\ell\) is the length of the code stack of \(c\). It serves as the cost bound of one round of the loop (a simulated step and a clock tick) on configurations whose numbers are at most \(M\).

def loopStepTime (c : Code) (M : ℕ) : ℕ := 10 * (codeCells c).length + 4 * M + 11

Uses 2 · Used by 3

Statement usesThe code stack · Codes for single-tape machines

Used byStep bound of the clocked simulation · The clocked universal machine on stacks · The clocked loop

TheoremThe clocked loop#✓fully proved

Let \(c\) be a code, let \(M\) be at least the length of the code stack of \(c\), let \(k\) be a configuration whose state and cells are all at most \(M\), let \(t\) be a natural number and \(v\) a bit, and let \(k_t\) be the result of \(t\) steps of \(c\) from \(k\), where a halted configuration stays put. Start the program of the clocked universal machine at label sc0 with variable \(v\) and the stacks of \(c\), the clock \(t\) and \(k\) (next state and action \(0\)). If \(k_t\) has halted, then within \((t + 1) \cdot L(c, M)\) steps, where \(L(c, M)\) is the loop step time, the program reaches label hlt with some variable and the stacks of \(c\), some clock \(t'\) and \(k_t\) (next state and action \(0\)). If instead \(c\) steps \(k_t\) to \(k''\), then within the same number of steps it reaches label tmo with some variable and the stacks of \(c\), the clock \(0\) and \(k''\) (next state and action \(0\)).

theorem loop_run {c : Code} {M : ℕ} (hM : (codeCells c).length ≤ M) :
    ∀ (t : ℕ) (k : Code.Cfg), Bounded M k → ∀ v : Bool,
      (c.step (c.stepOrStay^[t] k) = none →
        ∃ v' t', RunLe prog ((t + 1) * loopStepTime c M) ⟨some .sc0, v, stk c t k 0 0⟩
          ⟨some .hlt, v', stk c t' (c.stepOrStay^[t] k) 0 0⟩) ∧
      ∀ k'', c.step (c.stepOrStay^[t] k) = some k'' →
        ∃ v', RunLe prog ((t + 1) * loopStepTime c M) ⟨some .sc0, v, stk c t k 0 0⟩
          ⟨some .tmo, v', stk c 0 k'' 0 0⟩

Uses 27 · Used by 1

Statement usesConfigurations bounded by \(M\) · Stacks of the clocked universal machine · Labels of the clocked universal machine · The code stack · Step bound of the clocked loop · The clocked universal program · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · One step of a code · One step of a code, or stay when halted · Runs within a step budget

Proof usesThe cell of a number · The cells of a list of numbers · Entries of a code · Numbers of a list of entries · Step bound of one simulated step · One simulated step, halting case · One simulated step, running case · Acting on a configuration · Table lookup of a code · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter · Decrement

Used byThe clocked universal machine on stacks

DefinitionStep bound of the clocked simulation#✓fully proved

For a code \(c\) and a clock \(T\), let \(|C|\) be the length of the code stack of \(c\). The step bound of the clocked simulation on the clock \(T\) is \(T + 1\) times the cost of one round of the loop on configurations whose numbers are at most \(|C| + 2\), that is, \((T + 1)(14|C| + 19)\).

def clockTime (c : Code) (T : ℕ) : ℕ := (T + 1) * loopStepTime c ((codeCells c).length + 2)

Uses 3 · Used by 4

Statement usesThe code stack · Step bound of the clocked loop · Codes for single-tape machines

Used byThe clocked universal machine on stacks · Correctness and running time of the clocked universal machine · Step bound of the clocked universal machine · The step bound of the clocked universal machine is quadratic

TheoremThe clocked universal machine on stacks#✓fully proved

Let \(c\) be a code, \(x\) a list of bits and \(T\) a natural number, and let \(|C|\) be the length of the code stack of \(c\). Start the program of the clocked universal machine at the label \(\mathsf{sc0}\), with any value of its internal variable, on the stacks holding the code \(c\), the clock \(T\) and the initial configuration on \(x\), all other stacks empty. If the clocked evaluation of \(c\) on \(x\) for \(T\) steps is defined, the machine reaches the label \(\mathsf{hlt}\) on the stacks holding \(c\), some clock \(t'\) and the configuration of \(c\) after \(T\) steps on \(x\); otherwise it reaches the label \(\mathsf{tmo}\) on the stacks holding \(c\), the clock \(0\) and some configuration. In both cases the internal variable ends with some value, all other stacks are empty, and the run takes at most \((T + 1)(14|C| + 19)\) steps, the step bound of the clocked machine on the clock \(T\).

When the clocked evaluation is defined, its value is the output of the configuration of \(c\) after \(T\) steps on \(x\).

theorem clocked_run (c : Code) (x : List Bool) (T : ℕ) (v : Bool) :
    ((c.evalSteps x T).isSome → ∃ v' t', RunLe prog (clockTime c T)
      ⟨some .sc0, v, stk c T (Code.init x) 0 0⟩ ⟨some .hlt, v', stk c t' (c.cfgAfter x T) 0 0⟩) ∧
    (c.evalSteps x T = none → ∃ v' k'', RunLe prog (clockTime c T)
      ⟨some .sc0, v, stk c T (Code.init x) 0 0⟩ ⟨some .tmo, v', stk c 0 k'' 0 0⟩)

Uses 21 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Step bound of the clocked simulation · The clocked universal program · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · Clocked configuration of a code · The clocked evaluator · Initial configuration of the code simulation · Runs within a step budget

Proof usesConfigurations bounded by \(M\) · The code stack · Step bound of the clocked loop · The clocked loop · Definedness of the clocked evaluator · 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 byCorrectness and running time of the clocked universal machine

DefinitionInput encoding of the clocked universal machine#✓fully proved

For a code \(c\), a list of bits \(x\) and a clock \(T\), the input of the clocked universal machine is the list of bits formed by the cell of \(T\), then the cells of the input word of \(x\), then the cell of \(0\) (a blank cell, the single bit false), then the code stack of \(c\) in reverse order.

def encIn (c : Code) (x : List Bool) (T : ℕ) : List Bool :=
  cell T ++ (cells (input x) ++ (false :: (codeCells c).reverse))

Uses 5 · Used by 8

Statement usesThe cell of a number · The cells of a list of numbers · The code stack · Codes for single-tape machines · Input word of a list of bits

Used byThe 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\) · The clocked universal function is polynomial-time computable · Reading the input · Correctness and running time of the clocked universal machine · The step bound of the clocked universal machine is quadratic

DefinitionCost of reading the input#✓fully proved

For a code \(c\), a list of bits \(x\) and a natural number \(T\), let \(w_1, \dots, w_n\) be the input word of \(x\) (false as the symbol \(1\), true as \(2\)), with \(w_1\) read as \(0\) when \(x\) is empty, let \(S_j = \sum_{i=1}^{n} (w_i + j)\), and let \(m\) be the length of the code stack of \(c\). The cost of reading the input is \(T + 2 + (S_3 + 2) + (S_1 + 1) + (w_1 + 2) + (m + 1)\).

def parseTime (c : Code) (x : List Bool) (T : ℕ) : ℕ :=
  T + 2 + (((input x).map (· + 3)).sum + 2) + ((cells (input x)).length + 1) +
    ((input x).headI + 2) + ((codeCells c).length + 1)

Uses 4 · Used by 4

Statement usesThe cells of a list of numbers · The code stack · Codes for single-tape machines · Input word of a list of bits

Used byReading the input · Correctness and running time of the clocked universal machine · Step bound of the clocked universal machine · The step bound of the clocked universal machine is quadratic

TheoremReading the input#✓fully proved

Let \(c\) be a code, \(x\) a list of bits and \(T\) a natural number, and let \(p\) be the cost of reading the input of \(c\), \(x\) and \(T\). Started at the label \(\mathsf{pc0}\) with state bit false, the input encoding of \(c\), \(x\) and \(T\) on the stack \(X\) and every other stack empty, the clocked universal program reaches the label \(\mathsf{sc0}\) in exactly \(p\) steps, with some state bit and the stacks of the code \(c\), the clock \(T\) and the initial configuration on \(x\), with next state and action \(0\).

theorem parse_run (c : Code) (x : List Bool) (T : ℕ) :
    ∃ v', Run prog (parseTime c x T) ⟨some .pc0, false, update (fun _ ↦ []) .X (encIn c x T)⟩
      ⟨some .sc0, v', stk c T (Code.init x) 0 0⟩

Uses 23 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Input encoding of the clocked universal machine · Cost of reading the input · The clocked universal program · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Initial configuration of the code simulation · Exact-length runs of a TM2 machine

Proof usesThe cell of a number · The cells of a list of numbers · The code stack · Decoding units · Symbol of an input bit · Input word of a list of bits · Flag bit of a machine state · Bit blocks · A single step executes the statement at the current label · Unary counter · Decrement · Bit-moving loop · Running the bit-moving loop

Used byCorrectness and running time of the clocked universal machine

DefinitionOutput encoding of the clocked universal machine#✓fully proved

The output bits of an optional list of numbers: no result (a timeout) is encoded as the single bit false, and a result \(l\) is encoded as the bit true followed by the cells of \(l\), where a number \(n\) is written as \(n\) bits true followed by one bit false.

def encOut : Option (List ℕ) → List Bool
  | none => [false]
  | some l => true :: cells l

Uses 1 · Used by 10

Statement usesThe cells of a list of numbers

Used byThe readout on raw bits in polynomial time · The diagonal answer read from the encoded output · The diagonal language through the universal machine · The diagonal language in polynomial time, given the reformatting machine · The readout in polynomial time · The readout run · The clocked universal function is polynomial-time computable · Writing the output · Writing a timeout · Correctness and running time of the clocked universal machine

TheoremWriting the output#✓fully proved

Let \(c\) be a code, \(t\) a natural number, \(k\) a configuration and \(v\) a bit, and let \(N\) be the length of the cells of the head symbol of \(k\) followed by the symbols to its right (a symbol \(a\) takes \(a + 1\) bits). Started at the label \(\mathsf{hlt}\) with state bit \(v\) and the stacks of the code \(c\), the clock \(t\) and the configuration \(k\) with next state and action \(0\), the clocked universal program reaches the label \(\mathsf{done}\) within \(4N + 8\) steps, with some state bit and stacks in which the output stack \(O\) holds the encoding of the output of \(k\): the bit true followed by the cells of the output of \(k\).

theorem out_run (c : Code) (t : ℕ) (k : Code.Cfg) (v : Bool) :
    ∃ v' S', RunLe prog (4 * (cells (k.head :: k.right)).length + 8) ⟨some .hlt, v, stk c t k 0 0⟩
      ⟨some .done, v', S'⟩ ∧ S' .O = encOut (some k.output)

Uses 21 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · The cells of a list of numbers · Output encoding of the clocked universal machine · The clocked universal program · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · Output of a configuration · Runs within a step budget

Proof usesThe cell of a number · 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 · Counter increment · Bit-moving loop · Running the bit-moving loop · Running a counter transfer

Used byCorrectness and running time of the clocked universal machine

TheoremWriting a timeout#✓fully proved

Let \(c\) be a code, \(t\) a natural number, \(k\) a configuration and \(v\) a bit. Started at the label \(\mathsf{tmo}\) with state bit \(v\) and the stacks of the code \(c\), the clock \(t\) and the configuration \(k\) with next state and action \(0\), the clocked universal program reaches the label \(\mathsf{done}\) in exactly one step, with the same state bit and the same stacks except that the output stack \(O\) holds the timeout encoding, the single bit false.

theorem tmo_run (c : Code) (t : ℕ) (k : Code.Cfg) (v : Bool) :
    Run prog 1 ⟨some .tmo, v, stk c t k 0 0⟩
      ⟨some .done, v, update (stk c t k 0 0) .O (encOut none)⟩

Uses 11 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Output encoding of the clocked universal machine · The clocked universal program · The stacks of a simulated configuration · Stack alphabet of the clocked universal machine · Codes for single-tape machines · Explicit configurations · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label · Counter increment

Used byCorrectness and running time of the clocked universal machine

DefinitionStep bound of the clocked universal machine#✓fully proved

For a code \(c\), a list of bits \(x\) and a natural number \(T\), the step bound of the whole machine on \((c, x, T)\) is the sum of three terms: the cost of reading the input on \((c, x, T)\), the step bound of the clocked simulation on the clock \(T\), and the output bound \(4\,(|x| + T + 1)\,(|C| + 3) + 8\), where \(|x|\) is the length of \(x\) and \(|C|\) is the length of the code stack of \(c\).

def univTime (c : Code) (x : List Bool) (T : ℕ) : ℕ :=
  parseTime c x T + clockTime c T + (4 * ((x.length + T + 1) * ((codeCells c).length + 3)) + 8)

Uses 4 · Used by 3

Statement usesStep bound of the clocked simulation · The code stack · Cost of reading the input · Codes for single-tape machines

Used byThe clocked universal function is polynomial-time computable · Correctness and running time of the clocked universal machine · The step bound of the clocked universal machine is quadratic

TheoremCorrectness and running time of the clocked universal machine#✓fully proved

Let \(c\) be a code, \(x\) a list of bits and \(T\) a natural number. Start the clocked universal stack program at the label \(\mathrm{pc0}\) with internal bit \(\mathrm{false}\), with every stack empty except \(X\), which holds the input encoding of \((c, x, T)\): the cell of \(T\), the cells of the input symbols of \(x\) (the symbol \(1\) for \(\mathrm{false}\) and \(2\) for \(\mathrm{true}\)), the bit \(\mathrm{false}\), and the code stack of \(c\) reversed, where the cell of a number \(n\) is \(n\) bits \(\mathrm{true}\) followed by the bit \(\mathrm{false}\). Then within at most \(N(c, x, T)\) steps, where \(N\) is the step bound of the whole machine, the program reaches the label \(\mathrm{done}\) (with some internal bit and some stack contents) with the output encoding of the clocked evaluation of \(c\) on \(x\) with clock \(T\) on the stack \(O\): the single bit \(\mathrm{false}\) if the coded machine does not halt within \(T\) steps, and otherwise the bit \(\mathrm{true}\) followed by the cells of its output, the tape from the head rightwards without trailing blanks.

theorem univ_run (c : Code) (x : List Bool) (T : ℕ) :
    ∃ v' S', RunLe prog (univTime c x T) ⟨some .pc0, false, update (fun _ ↦ []) .X (encIn c x T)⟩
      ⟨some .done, v', S'⟩ ∧ S' .O = encOut (c.evalSteps x T)

Uses 36 · Used by 1

Statement usesStacks of the clocked universal machine · Labels of the clocked universal machine · Input encoding of the clocked universal machine · Output encoding of the clocked universal machine · The clocked universal program · Step bound of the clocked universal machine · Stack alphabet of the clocked universal machine · Codes for single-tape machines · The clocked evaluator · Runs within a step budget

Proof usesConfigurations bounded by \(M\) · The cell of a number · The cells of a list of numbers · Step bound of the clocked simulation · The clocked universal machine on stacks · The code stack · Entries of a code · Numbers of a list of entries · Writing the output · Cost of reading the input · Reading the input · The stacks of a simulated configuration · Writing a timeout · Explicit configurations · Acting on a configuration · Output of a configuration · Clocked configuration of a code · Characterization of clocked results · Initial configuration of the code simulation · Table lookup of a code · 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 · Exact-length runs of a TM2 machine · Unary counter

Used byThe clocked universal function is polynomial-time computable

AbbreviationThe clocked universal machine as a host component#✓fully proved

The component machine whose stacks are the fifteen stacks of the clocked universal machine, each holding bits, whose labels and program are those of the clocked universal machine, and whose list of stacks is, in order: the state \(Q\), the next state \(N\), the action \(A\), the head cell \(H\), the cells left (\(L\)) and right (\(R\)) of the head, the code \(C\), the scan buffer \(B\), the scratch counters \(T\), \(U\), \(V\), the clock \(\mathit{Ck}\), the encoded input \(X\), the parse buffer \(P\) and the output \(O\).

abbrev univComp : Comp where
  K := K
  Γ := Γ
  finΓ := fun _ ↦ inferInstanceAs (Fintype Bool)
  L := Lab
  prog := prog
  ks := [.Q, .N, .A, .H, .L, .R, .C, .B, .T, .U, .V, .Ck, .X, .P, .O]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 5 · Used by 1

Statement usesComponent machine · Stacks of the clocked universal machine · Labels of the clocked universal machine · The clocked universal program · Stack alphabet of the clocked universal machine

Used byThe clocked universal function is polynomial-time computable

TheoremThe step bound of the clocked universal machine is quadratic#✓fully proved

For every code \(c\), list of bits \(x\) and clock \(T \in \mathbb{N}\), the step bound of the whole clocked universal machine on \((c, x, T)\) is at most \(18 (n + 1)^2\), where \(n\) is the length of the input encoding of \((c, x, T)\).

theorem univTime_le (c : Code) (x : List Bool) (T : ℕ) :
    univTime c x T ≤ 18 * ((encIn c x T).length + 1) ^ 2

Uses 11 · Used by 1

Statement usesInput encoding of the clocked universal machine · Step bound of the clocked universal machine · Codes for single-tape machines

Proof usesThe cell of a number · The cells of a list of numbers · Step bound of the clocked simulation · The code stack · Cost of reading the input · Symbol of an input bit · Input word of a list of bits · Unary counter

Used byThe clocked universal function is polynomial-time computable

DefinitionStep bound polynomial of the clocked universal machine#✓fully proved

The polynomial \(18 (X + 1)^2\) with natural-number coefficients, used as the step bound of the clocked universal machine as a host component.

noncomputable def univPoly : Polynomial ℕ := Polynomial.C 18 * (Polynomial.X + 1) ^ 2

Used by 1

Used byThe clocked universal function is polynomial-time computable

TheoremThe clocked universal function is polynomial-time computable#✓fully proved

There are a multi-stack Turing machine with finitely many stacks, labels and internal states, whose input and output alphabets are in bijection with the bits, and a polynomial \(p\) with natural-number coefficients, such that for every code \(c\), list of bits \(x\) and clock \(T \in \mathbb{N}\) the following holds. Let \(n\) be the length of the input encoding of \((c, x, T)\). Started at its main label in its initial internal state, with the input encoding of \((c, x, T)\) on its input stack and every other stack empty, the machine halts within \(p(n)\) steps, with its internal state again the initial one, the output encoding of the result of the clocked evaluator on \(c\), \(x\) and \(T\) on its output stack, and every other stack empty; both encodings are translated letter by letter through the inverses of the bijections.

In the proof, \(p\) has degree \(2\): the clocked universal machine itself takes at most \(18 (n + 1)^2\) steps, and running it as a component of the reduction host keeps the degree.

theorem nonempty_univPolyTime :
    Nonempty (TM2ComputableInPolyTime (fun a : Code × List Bool × ℕ ↦ encIn a.1 a.2.1 a.2.2)
      encOut (fun a ↦ a.1.evalSteps a.2.1 a.2.2))

Uses 26 · Used by 1

Statement usesInput encoding of the clocked universal machine · Output encoding of the clocked universal machine · Codes for single-tape machines · The clocked evaluator

Proof usesComponent machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Phase-0 labels of the generic host · Halting configuration of a finite multi-stack machine · Initial configuration of a finite multi-stack machine · Reduction host program · The reduction host's run on one input · Step bound of the reduction host · Reduction host machine · Stacks of the clocked universal machine · Labels of the clocked universal machine · The clocked universal program · The clocked universal machine as a host component · Step bound polynomial of the clocked universal machine · Step bound of the clocked universal machine · The step bound of the clocked universal machine is quadratic · Correctness and running time of the clocked universal machine · Stack alphabet of the clocked universal machine · Exact-length runs of a TM2 machine · Runs within a step budget

Used byThe diagonal language in polynomial time, given the reformatting machine

37 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.