Skip to content

Simulating component machines in a host machine

StructureComponent machine#✓fully proved

A component machine consists of a finite type \(K\) of stacks with decidable equality, a finite alphabet \(\Gamma_k\) for each stack \(k\), a finite type \(L\) of labels with decidable equality, a multi-stack Turing machine program assigning to each label in \(L\) a statement over the alphabets \(\Gamma\) and the labels \(L\) with Boolean internal state, and a list of the stacks in which every stack occurs exactly once, so that a host can empty all of them.

Cslib.Complexity.Host.Comp · 25 lines 
structure Comp where
  /-- Stack indices. -/
  K : Type
  /-- Decidable equality of stack indices. -/
  [decK : DecidableEq K]
  /-- Finitely many stacks. -/
  [finK : Fintype K]
  /-- Stack alphabets. -/
  Γ : K → Type
  /-- Finite alphabets. -/
  [finΓ : ∀ k, Fintype (Γ k)]
  /-- Labels. -/
  L : Type
  /-- Decidable equality of labels. -/
  [decL : DecidableEq L]
  /-- Finitely many labels. -/
  [finL : Fintype L]
  /-- The program. -/
  prog : L → TM2.Stmt Γ L Bool
  /-- The stacks, listed. -/
  ks : List K
  /-- No stack is listed twice. -/
  ks_nodup : ks.Nodup
  /-- Every stack is listed. -/
  mem_ks : ∀ k, k ∈ ks
Used by 74
Used byThe reversal component · Reversing and dropping the first bit is polynomial-time · Running the reversal component · The readout on raw bits in polynomial time · The checking machine as a host component · The layout machine as a host component · The readout machine as a host component · The checking machine in polynomial time · The layout in polynomial time · List-of-naturals canonicalizer as a host component · Payload normalizer as a host component · Payload normalization is polynomial-time · Pair-list projector as a host component · Frame counter for lists of naturals as a host component · Four-output pair-list decoder as a host component · Number-pair projector as a host component · Raw pair-frame splitter as a host component · Unary-to-binary converter as a host component · The 3-COLOR verifier as a host component · 3-COLOR is in NP · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · The CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier as a host component · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier · PARTITION doubling machine as a host component · Raw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION padding machine as a host component · Raw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · SUBSET-SUM to PARTITION map is polynomial-time · PARTITION to SUBSET-SUM map is polynomial-time · PARTITION doubling pass is polynomial-time · The VERTEX-COVER to SUBSET-SUM machine as a host component · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time · The SUBSET-SUM verifier machine as a host component · SUBSET-SUM is in NP · HAMPATH is in NP · The HAMPATH verifier as a host component · The tokenize-then-emit machine as a host component · Emitter reductions out of SAT are polynomial-time · The marking algorithm is polynomial-time · The marking machine as a host component · Agreement with the embedded component · The list of host stacks · Cleanup stacks of the generic host · Cleanup in a host · The component's stacks inside a host · The reduction host embeds the component · The verifier host embeds the component · Labels of the generic host as a sum type · Alphabets of the generic host · Stacks of the generic host · Labels of the generic host · Decider host · Reduction host, canonical form · Verifier host, canonical form · Membership in the cleanup stacks of the generic host · Component labels in the reduction host · Reduction host · Reduction host program · The reduction host's run · The reduction host's run on one input · Step bound of the reduction host · Reduction host machine · Stack lengths when only one stack is filled · Relabelling in the verifier host · Verifier host · Verifier host program · The verifier host's run · Step bound of the verifier host · The verifier host machine · The clocked universal function is polynomial-time computable · The clocked universal machine as a host component
37 fully proved

Host stacks, alphabets and labels

InductiveStacks of the generic host#✓fully proved

For a component machine \(c\) with stack indices \(K\), the host stacks are an input stack, an output stack, two buffers \(X_1\) and \(W_1\) used in phase 0 (which moves the input onto the component's stacks), and one copy of each component stack \(k \in K\).

inductive HK (c : Comp)
  | inp | out | X1 | W1
  | comp (k : c.K)
  deriving DecidableEq
Uses 1 · Used by 20
Statement usesComponent machine
Used byAgreement with the embedded component · The list of host stacks · Cleanup stacks of the generic host · Cleanup in a host · The component's stacks inside a host · The reduction host embeds the component · The verifier host embeds the component · Alphabets of the generic host · Membership in the cleanup stacks of the generic host · Reduction host · Reduction host program · The reduction host's run · The reduction host's run on one input · Reduction host machine · Stack lengths when only one stack is filled · Verifier host · Verifier host program · The verifier host's run · The verifier host machine · The clocked universal function is polynomial-time computable

DefinitionThe list of host stacks#✓fully proved

For a component machine \(c\), the host stacks are listed as the input stack, the output stack, the two buffer stacks \(X_1\) and \(W_1\), and then the host's copies of the stacks of \(c\), in the order of the list of stacks that \(c\) carries.

def allKs (c : Comp) : List (HK c) := .inp :: .out :: .X1 :: .W1 :: c.ks.map .comp
Uses 2 · Used by 5
Statement usesComponent machine · Stacks of the generic host
Used byCleanup stacks of the generic host · Cleanup in a host · Membership in the cleanup stacks of the generic host · Reduction host machine · The verifier host machine

DefinitionAlphabets of the generic host#✓fully proved

For a component machine \(c\) with stack alphabets \((\Gamma_k)_k\) and a type \(\alpha\), the alphabet of a host stack is \(\alpha\) on the input stack, \(\Gamma_k\) on the host copy of the component's stack \(k\), and the booleans on the output stack and on the two phase-0 buffers.

@[reducible] def HΓ (c : Comp) (α : Type) : HK c → Type
  | .inp => α
  | .comp k => c.Γ k
  | _ => Bool
Uses 2 · Used by 16
Statement usesComponent machine · Stacks of the generic host
Used byAgreement with the embedded component · Cleanup in a host · The component's stacks inside a host · The reduction host embeds the component · The verifier host embeds the component · Reduction host · Reduction host program · The reduction host's run · The reduction host's run on one input · Reduction host machine · Stack lengths when only one stack is filled · Verifier host · Verifier host program · The verifier host's run · The verifier host machine · The clocked universal function is polynomial-time computable

InductivePhase-0 labels of the generic host#✓fully proved

The six labels of a host's phase 0, which moves the input onto the component's stacks: two for the two passes that move the first block \(x\), one that drops the separator, two for the two passes that move the second block \(w\), and one that resets the state and starts the component.

inductive P0 | m1 | m2 | sep | m3 | m4 | go
  deriving DecidableEq
Used by 12
Used byLabels of the generic host as a sum type · Labels of the generic host · Reduction host · Reduction host program · The reduction host's run · The reduction host's run on one input · Reduction host machine · Verifier host · Verifier host program · The verifier host's run · The verifier host machine · The clocked universal function is polynomial-time computable

InductiveLabels of the generic host#✓fully proved

For a component machine \(c\) with labels \(L\), and with \(P_0\) the set of phase-0 labels, the host labels are one label for each \(p \in P_0\), one copy of each component label \(l \in L\), and, for each boolean answer \(a\), a cleanup label and an output label carrying \(a\).

inductive HLab (c : Comp)
  | ph (p : P0)
  | comp (l : c.L)
  | clean (ans : Bool)
  | fin (ans : Bool)
  deriving DecidableEq
Uses 2 · Used by 16
Statement usesComponent machine · Phase-0 labels of the generic host
Used byCleanup in a host · The reduction host embeds the component · The verifier host embeds the component · Labels of the generic host as a sum type · Component labels in the reduction host · Reduction host · Reduction host program · The reduction host's run · The reduction host's run on one input · Reduction host machine · Relabelling in the verifier host · Verifier host · Verifier host program · The verifier host's run · The verifier host machine · The clocked universal function is polynomial-time computable

DefinitionLabels of the generic host as a sum type#✓fully proved

For a component machine \(c\) with labels \(L\), let \(P_0\) be the set of phase-0 labels and \(B = \{\mathrm{false}, \mathrm{true}\}\). The host labels of \(c\) are in bijection with the disjoint union \(P_0 \sqcup L \sqcup B \sqcup B\): the phase-0 label \(p\) corresponds to \(p\), the host copy of the component label \(l\) to \(l\), the cleanup label with answer \(a\) to \(a\) in the first copy of \(B\), and the output label with answer \(a\) to \(a\) in the second copy of \(B\).

The bijection shows that there are finitely many host labels.

def HLab.equiv (c : Comp) : HLab c ≃ P0 ⊕ c.L ⊕ Bool ⊕ Bool where
  toFun
    | .ph p => .inl p | .comp l => .inr (.inl l) | .clean a => .inr (.inr (.inl a))
    | .fin a => .inr (.inr (.inr a))
  invFun
    | .inl p => .ph p | .inr (.inl l) => .comp l | .inr (.inr (.inl a)) => .clean a
    | .inr (.inr (.inr a)) => .fin a
  left_inv x := by cases x <;> rfl
  right_inv x := by rcases x with p | l | a | a <;> rfl
Uses 3 · Used by 2
Statement usesComponent machine · Labels of the generic host · Phase-0 labels of the generic host
Used byReduction host machine · The verifier host machine

DefinitionThe component's stacks inside a host#✓fully proved

For a component machine \(c\) and an input alphabet \(\alpha\), the stack embedding of \(c\) into the host over \(\alpha\) sends each stack \(k\) of \(c\) to the host's copy of \(k\), whose alphabet is the alphabet \(\Gamma_k\) of \(k\), and identifies the two alphabets by the identity. Distinct stacks have distinct copies, so the embedding is injective.

def emb (c : Comp) (α : Type) : SEmb c.Γ (HΓ c α) where
  e := .comp
  inj _ _ h := HK.comp.inj h
  ι _ := Equiv.refl _
Uses 4 · Used by 7
Statement usesComponent machine · Stacks of the generic host · Alphabets of the generic host · Stack embedding
Used byAgreement with the embedded component · The reduction host embeds the component · The verifier host embeds the component · Reduction host program · The reduction host's run on one input · Verifier host program · The verifier host's run

TheoremAgreement with the embedded component#✓fully proved

Let \(c\) be a component machine and \(\alpha\) an input alphabet. For stack contents \(S\) of \(c\) and stack contents \(T\) of the host over \(\alpha\), \(T\) agrees with \(S\) under the embedding of the component's stacks into the host if and only if, for every stack \(k\) of \(c\), the host's copy of \(k\) holds exactly \(S(k)\).

theorem agree_emb {c : Comp} {α : Type} {S : ∀ k, List (c.Γ k)} {T : ∀ k, List (HΓ c α k)} :
    Agree (emb c α) S T ↔ ∀ k, T (.comp k) = S k
Uses 6 · Used by 2
Statement usesComponent machine · Stacks of the generic host · Alphabets of the generic host · The component's stacks inside a host · Agreement of host and sub-machine stacks
Proof usesStack embedding
Used byThe reduction host's run on one input · The verifier host's run

Generic pieces of a host run

TheoremMoving a bit block through a buffer#✓fully proved

Let \(a\), \(t\), \(b\) be pairwise distinct stacks of a program \(M\) with Boolean state, and let \(l_1\), \(l_2\), \(l_3\) be labels such that \(M\) runs at \(l_1\) the bit-moving loop from \(a\) to \(t\) with decoder \(d\) and encoder \(g_t\), looping at \(l_1\) and exiting to \(l_2\), and at \(l_2\) the bit-moving loop from \(t\) to \(b\) with decoder \(d_t\) and encoder \(g\), looping at \(l_2\) and exiting to \(l_3\), where \(d_t\) decodes \(g_t(y)\) to \(y\) for every bit \(y\). Let \(x = x_1 \cdots x_n\) be a bit list and \(S\) stack contents in which \(a\) holds a bit block for \(x\) under \(d\) followed by a rest \(A\) that ends a bit block under \(d\), and \(t\) is empty. Then for every state \(v\) there are a state \(v'\) and stack contents \(S'\) such that \(M\) runs in exactly \(2n + 2\) steps from label \(l_1\), state \(v\) and stacks \(S\) to label \(l_3\), state \(v'\) and stacks \(S'\), where \(S'(a) = A\), \(S'(t)\) is empty, \(S'(b)\) is \(g(x_1), \dots, g(x_n)\) (top first) followed by \(S(b)\), and \(S'(k) = S(k)\) for every other stack \(k\).

theorem move2_run {K Λ : Type} [DecidableEq K] {Γ : K → Type} {M : Λ → TM2.Stmt Γ Λ Bool}
    {a t b : K} {d : Γ a → Option Bool} {gt : Bool → Γ t} {dt : Γ t → Option Bool}
    {g : Bool → Γ b} {l₁ l₂ l₃ : Λ} (h₁ : M l₁ = moveB a t d gt l₁ l₂)
    (h₂ : M l₂ = moveB t b dt g l₂ l₃) (hat : a ≠ t) (htb : t ≠ b) (hab : a ≠ b)
    (hdt : ∀ y, dt (gt y) = some y) (x : List Bool) (xs A : List (Γ a)) (v : Bool)
    (S : ∀ k, List (Γ k)) (hS : S a = xs ++ A) (hxs : IsBitBlock d xs x)
    (hA : EndsBitBlock d A) (ht : S t = []) :
    ∃ v' S', Run M (2 * x.length + 2) ⟨some l₁, v, S⟩ ⟨some l₃, v', S'⟩ ∧ S' a = A ∧
      S' t = [] ∧ S' b = x.map g ++ S b ∧ ∀ k, k ≠ a → k ≠ t → k ≠ b → S' k = S k
Uses 6 · Used by 3
Statement usesEnd of a bit block · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · Bit-moving loop
Proof usesRunning the bit-moving loop
Used byRaw-input PARTITION membership machine runs in quadratic time · The reduction host's run on one input · The verifier host's run

DefinitionCleanup stacks of the generic host#✓fully proved

For a component machine \(c\) and a host stack \(o\), the cleanup stacks are the list of all host stacks with \(o\) removed, in the order of the list of host stacks. The cleanup empties these stacks and leaves the output stack \(o\).

def cleanKs (c : Comp) (o : HK c) : List (HK c) := (allKs c).filter (· ≠ o)
Uses 3 · Used by 4
Statement usesComponent machine · Stacks of the generic host · The list of host stacks
Used byCleanup in a host · Membership in the cleanup stacks of the generic host · Reduction host program · Verifier host program

TheoremMembership in the cleanup stacks of the generic host#✓fully proved

For a component machine \(c\) and host stacks \(o\) and \(k\), the stack \(k\) belongs to the list of stacks that the cleanup for the output stack \(o\) empties if and only if \(k \ne o\).

theorem mem_cleanKs {c : Comp} {o k : HK c} : k ∈ cleanKs c o ↔ k ≠ o
Uses 4 · Used by 1
Statement usesComponent machine · Stacks of the generic host · Cleanup stacks of the generic host
Proof usesThe list of host stacks
Used byCleanup in a host

TheoremCleanup in a host#✓fully proved

Let \(c\) be a component machine, \(\alpha\) an input alphabet, \(o\) a host stack, \(a\) a bit, and \(M\) a host program with Boolean state whose statement at the cleanup label for \(a\) is the cleanup round on the list of all host stacks with \(o\) removed, kept in the order of the list of host stacks, repeating at the cleanup label for \(a\) and exiting to the output label for \(a\). If \(S\) assigns to every host stack at most \(m\) symbols, then for every state \(v\), \(M\) runs from the cleanup label for \(a\) with state \(v\) and stacks \(S\) to the output label for \(a\) in at most \(m + 1\) steps, ending with state false, stack \(o\) holding \(S(o)\) and every other stack empty.

theorem cleanup_run {c : Comp} {α : Type} {M : HLab c → TM2.Stmt (HΓ c α) (HLab c) Bool}
    {o : HK c} {ans : Bool} (hM : M (.clean ans) = cleanS (cleanKs c o) (.clean ans) (.fin ans))
    (m : ℕ) (v : Bool) (S : ∀ k, List (HΓ c α k)) (hl : ∀ k, (S k).length ≤ m) :
    RunLe M (m + 1) ⟨some (.clean ans), v, S⟩
      ⟨some (.fin ans), false, update (fun _ => []) o (S o)⟩
Uses 11 · Used by 2
Statement usesComponent machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Cleanup stacks of the generic host · Flag bit of a machine state · Runs within a step budget · Cleanup round
Proof usesThe list of host stacks · Membership in the cleanup stacks of the generic host · Cleanup empties its stacks
Used byThe reduction host's run on one input · The verifier host's run

TheoremStack lengths grow by at most the push bound per step#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with push bound \(B\). If every stack of \(S\) has length at most \(N\) and \(M\) runs in \(n\) steps from a configuration with some label, state \(v\) and stacks \(S\) to a configuration with some label, state \(v'\) and stacks \(S'\), then every stack of \(S'\) has length at most \(N + Bn\).

theorem stk_length_le (M : FinTM2) {n N : ℕ} {S S' : ∀ k, List (M.Γ k)} {v v' : M.σ}
    {l l' : M.Λ} (hS : ∀ k, (S k).length ≤ N) (h : Run M.m n ⟨some l, v, S⟩ ⟨some l', v', S'⟩) :
    ∀ k, (S' k).length ≤ N + TM2Composition.pushBound M * n
Uses 4 · Used by 2
Statement usesPush bound of a finite multi-stack Turing machine · Exact-length runs of a TM2 machine
Proof usesNumber of push instructions in a TM2 statement · A halted run stays halted
Used byThe reduction host's run on one input · The verifier host's run

TheoremInitial configuration of a finite multi-stack machine#✓fully proved

For a finite multi-stack Turing machine \(M\) with input stack \(k_0\), main label \(\lambda_0\) and initial internal state \(\sigma_0\), and a list \(l\) over the alphabet of \(k_0\), the initial configuration of \(M\) on \(l\) has current label \(\lambda_0\), internal state \(\sigma_0\), the list \(l\) on \(k_0\) and every other stack empty.

theorem initList_eq (M : FinTM2) (l : List (M.Γ M.k₀)) :
    initList M l = ⟨some M.main, M.initialState, update (fun _ => []) M.k₀ l⟩
Used by 3
Used byReduction host · Verifier host · The clocked universal function is polynomial-time computable

TheoremHalting configuration of a finite multi-stack machine#✓fully proved

For a finite multi-stack Turing machine \(M\) with output stack \(k_1\) and initial internal state \(\sigma_0\), and a list \(l\) over the alphabet of \(k_1\), the halting configuration of \(M\) with output \(l\) has no current label, internal state \(\sigma_0\), the list \(l\) on \(k_1\) and every other stack empty.

theorem haltList_eq (M : FinTM2) (l : List (M.Γ M.k₁)) :
    haltList M l = ⟨none, M.initialState, update (fun _ => []) M.k₁ l⟩
Used by 3
Used byReduction host · Verifier host · The clocked universal function is polynomial-time computable

TheoremStack lengths when only one stack is filled#✓fully proved

Let \(c\) be a component machine and consider its host with input alphabet \(\alpha\). If a host stack \(o\) holds a list \(l\) and every other host stack is empty, then every host stack has length at most the length of \(l\).

theorem update_length_le {c : Comp} {α : Type} (o : HK c) (l : List (HΓ c α o)) :
    ∀ k, (update (fun _ => []) o l k).length ≤ l.length
Uses 3 · Used by 2
Statement usesComponent machine · Stacks of the generic host · Alphabets of the generic host
Used byThe reduction host's run on one input · The verifier host's run

The reduction host

DefinitionComponent labels in the reduction host#✓fully proved

For a component with exit label \(\mathit{done}\), the label \(\mathit{done}\) is sent to the host's cleanup label with answer false, and every other component label \(l\) to the host label that runs the component at \(l\).

def φR (l : c.L) : HLab c := if l = done then .clean false else .comp l
Uses 2 · Used by 3
Statement usesComponent machine · Labels of the generic host
Used byThe reduction host embeds the component · Reduction host program · The reduction host's run on one input

DefinitionReduction host program#✓fully proved

The program of the reduction host for a component with stacks \(c_X\) and \(c_O\), an encoding \(g_X\) of bits as symbols of \(c_X\) and labels \(\mathit{start}\) and \(\mathit{done}\). Phase 0 moves the whole input stack onto the buffer \(X_1\) with the bit-moving loop, then moves \(X_1\) onto the host's copy of \(c_X\) re-encoded by \(g_X\) (so in the original order), then sets the state to false and goes to \(\mathit{start}\), or to the cleanup if \(\mathit{start} = \mathit{done}\). At the host label of a component label \(l\) it runs the component's statement at \(l\) on the host's copies of the component stacks, with every jump to \(\mathit{done}\) sent to the cleanup. The cleanup pops every stack other than the copy of \(c_O\) once per round, repeating while something was popped, and then goes to the final label, which halts. The phase-0 labels for a separator and a second block halt.

def rprog : HLab c → TM2.Stmt (HΓ c Bool) (HLab c) Bool
  | .ph .m1 => moveB (Γ := HΓ c Bool) .inp .X1 some id (.ph .m1) (.ph .m2)
  | .ph .m2 => moveB (Γ := HΓ c Bool) .X1 (.comp cX) some gX (.ph .m2) (.ph .go)
  | .ph .go => .load (fun _ => false) (.goto fun _ => φR c done start)
  | .ph .sep | .ph .m3 | .ph .m4 => .halt
  | .comp l => mapS (emb c Bool) (φR c done) (c.prog l)
  | .clean _ => cleanS (cleanKs c (.comp cO)) (.clean false) (.fin false)
  | .fin _ => .halt
Uses 12 · Used by 6
Statement usesComponent machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Phase-0 labels of the generic host · Cleanup stacks of the generic host · The component's stacks inside a host · Component labels in the reduction host · Translating a statement along a stack embedding · Flag bit of a machine state · Cleanup round · Bit-moving loop
Used byThe reduction host embeds the component · Reduction host · The reduction host's run · The reduction host's run on one input · Reduction host machine · The clocked universal function is polynomial-time computable

DefinitionReduction host machine#✓fully proved

The reduction host as a finite multi-stack Turing machine: its stacks are the host stacks with the host alphabets for bit input, its labels are the host labels, its state is a bit starting at false, its program is the reduction host program started at the first phase-0 label, its input stack is the input stack (raw bits) and its output stack is the host's copy of the component's stack \(c_O\).

def rtm : FinTM2 where
  K := HK c
  k₀ := .inp
  k₁ := .comp cO
  Γ := HΓ c Bool
  Λ := HLab c
  main := .ph .m1
  σ := Bool
  initialState := false
  Γk₀Fin := (inferInstance : Fintype Bool)
  m := rprog c cX cO gX start done
Uses 8 · Used by 4
Statement usesComponent machine · Stacks of the generic host · Labels of the generic host · Labels of the generic host as a sum type · Alphabets of the generic host · Phase-0 labels of the generic host · The list of host stacks · Reduction host program
Used byReduction host · The reduction host's run on one input · Step bound of the reduction host · The clocked universal function is polynomial-time computable

DefinitionStep bound of the reduction host#✓fully proved

Let \(c\) be a component machine with stacks \(c_X\) and \(c_O\), an encoding \(g_X\) of bits as symbols of \(c_X\) and labels \(\mathit{start}\) and \(\mathit{done}\), and let \(B\) be the push bound of the reduction host machine built from these data. For a polynomial \(p\) with natural-number coefficients, the step bound of the reduction host is the polynomial in the variable \(X\)

\[(B + 1)(2X + 3 + p) + X + 2.\]

At an input length \(n\) it counts phase 0 and the component, at most \(2n + 3 + p(n)\) steps, then the cleanup, which takes at most one step more than the longest stack, of length at most \(n\) plus \(B\) times the steps so far, and the halt.

noncomputable def rtime (p : Polynomial ℕ) : Polynomial ℕ :=
  Polynomial.C (TM2Composition.pushBound (rtm c cX cO gX start done) + 1) *
      (Polynomial.C 2 * Polynomial.X + Polynomial.C 3 + p) + Polynomial.X + Polynomial.C 2
Uses 3 · Used by 4
Statement usesComponent machine · Reduction host machine · Push bound of a finite multi-stack Turing machine
Used byReduction host · The reduction host's run · The reduction host's run on one input · The clocked universal function is polynomial-time computable

TheoremThe reduction host embeds the component#✓fully proved

Let \(c\) be a component machine with stacks \(c_X\) and \(c_O\), a map \(g_X\) from bits to the alphabet of \(c_X\), and labels \(s\) and \(d\), and suppose that \(c\) halts at \(d\). Rename the labels of \(c\) by sending \(d\) to the cleanup label with answer false and every other label \(l\) to the host's copy of \(l\), and embed the stacks of \(c\) as the host's copies over the bit input alphabet. Then the reduction host built from \(c_X\), \(c_O\), \(g_X\), \(s\) and \(d\) embeds \(c\): for every label \(l\) of \(c\), either \(c\) halts at \(l\), or the host's statement at the renamed label of \(l\) is the statement of \(c\) at \(l\) with stacks and labels translated.

theorem embeds_rprog (hdone : c.prog done = .halt) :
    Embeds (emb c Bool) (φR c done) c.prog (rprog c cX cO gX start done)
Uses 9 · Used by 1
Statement usesComponent machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · The component's stacks inside a host · Reduction host program · Component labels in the reduction host · Embedding of a machine in a host
Proof usesTranslating a statement along a stack embedding
Used byThe reduction host's run on one input

TheoremThe reduction host's run on one input#✓fully proved

Let \(c\) be a component with stacks \(c_X\) and \(c_O\), an encoding \(g_X\) of bits as symbols of \(c_X\), an identification \(e_O\) of the alphabet of \(c_O\) with the bits, and labels \(\mathit{start}\) and \(\mathit{done}\), where the component halts at \(\mathit{done}\). Let \(p\) be a polynomial with natural-number coefficients and \(x\), \(o\) bit lists, and suppose that the component, started at \(\mathit{start}\) with state false, with \(x\) encoded by \(g_X\) on \(c_X\) and every other stack empty, reaches \(\mathit{done}\) within \(p(|x|)\) steps with some state and stacks in which \(c_O\) holds \(o\) translated symbol by symbol by \(e_O^{-1}\). Then the reduction host program, started at its first phase-0 label with state false, \(x\) on the input stack and every other stack empty, halts within \(T(|x|)\) steps, where \(T\) is the reduction host's step bound for \(p\), with state false, \(o\) translated by \(e_O^{-1}\) on the host's copy of \(c_O\) and every other stack empty.

theorem rprog_run_at (eO : c.Γ cO ≃ Bool) (out : List Bool) (p : Polynomial ℕ)
    (hdone : c.prog done = .halt) (x : List Bool)
    (hrun : ∃ v S', RunLe c.prog (p.eval x.length)
      ⟨some start, false, update (fun _ => []) cX (x.map gX)⟩ ⟨some done, v, S'⟩ ∧
        S' cO = out.map eO.symm) :
    RunLe (rprog c cX cO gX start done) ((rtime c cX cO gX start done p).eval x.length)
      ⟨some (.ph .m1), false, update (fun _ => []) .inp x⟩
      ⟨none, false, update (fun _ => []) (.comp cO) (out.map eO.symm)⟩
Uses 23 · Used by 2
Statement usesComponent machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Phase-0 labels of the generic host · Reduction host program · Step bound of the reduction host · Runs within a step budget
Proof usesAgreement with the embedded component · Cleanup in a host · The component's stacks inside a host · The reduction host embeds the component · Moving a bit block through a buffer · Reduction host machine · Stack lengths grow by at most the push bound per step · Stack lengths when only one stack is filled · Component labels in the reduction host · Push bound of a finite multi-stack Turing machine · Agreement of host and sub-machine stacks · Frame condition for a stack embedding · Run embedding for bounded runs · Exact-length runs of a TM2 machine · A single step executes the statement at the current label
Used byThe reduction host's run · The clocked universal function is polynomial-time computable

TheoremThe reduction host's run#✓fully proved

Let \(c\) be a component with stacks \(c_X\) and \(c_O\), an encoding \(g_X\) of bits as symbols of \(c_X\), an identification \(e_O\) of the alphabet of \(c_O\) with the bits, and labels \(\mathit{start}\) and \(\mathit{done}\), where the component halts at \(\mathit{done}\). Let \(f\) be a function from bit lists to bit lists and \(p\) a polynomial with natural-number coefficients, and suppose that for every bit list \(y\) the component, started at \(\mathit{start}\) with state false, with \(y\) encoded by \(g_X\) on \(c_X\) and every other stack empty, reaches \(\mathit{done}\) within \(p(|y|)\) steps with some state and stacks in which \(c_O\) holds \(f(y)\) translated symbol by symbol by \(e_O^{-1}\). Then for every bit list \(x\) the reduction host program, started at its first phase-0 label with state false, \(x\) on the input stack and every other stack empty, halts within \(T(|x|)\) steps, where \(T\) is the reduction host's step bound for \(p\), with state false, \(f(x)\) translated by \(e_O^{-1}\) on the host's copy of \(c_O\) and every other stack empty.

theorem rprog_run (eO : c.Γ cO ≃ Bool) (f : List Bool → List Bool) (p : Polynomial ℕ)
    (hdone : c.prog done = .halt)
    (hrun : ∀ x, ∃ v S', RunLe c.prog (p.eval x.length)
      ⟨some start, false, update (fun _ => []) cX (x.map gX)⟩ ⟨some done, v, S'⟩ ∧
        S' cO = (f x).map eO.symm)
    (x : List Bool) :
    RunLe (rprog c cX cO gX start done) ((rtime c cX cO gX start done p).eval x.length)
      ⟨some (.ph .m1), false, update (fun _ => []) .inp x⟩
      ⟨none, false, update (fun _ => []) (.comp cO) ((f x).map eO.symm)⟩
Uses 9 · Used by 1
Statement usesComponent machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Phase-0 labels of the generic host · Reduction host program · Step bound of the reduction host · Runs within a step budget
Proof usesThe reduction host's run on one input
Used byReduction host

DefinitionReduction host#✓fully proved

Let \(c\) be a component with stacks \(c_X\) and \(c_O\), an encoding \(g_X\) of bits as symbols of \(c_X\), an identification \(e_O\) of the alphabet of \(c_O\) with the bits, and labels \(\mathit{start}\) and \(\mathit{done}\), where the component halts at \(\mathit{done}\). Let \(f\) be a function from bit lists to bit lists and \(p\) a polynomial with natural-number coefficients. Suppose that for every bit list \(x\) the component, started at \(\mathit{start}\) with state false, with \(x\) encoded by \(g_X\) on \(c_X\) and every other stack empty, reaches \(\mathit{done}\) within \(p(|x|)\) steps with some state and stacks in which \(c_O\) holds \(f(x)\) translated symbol by symbol by \(e_O^{-1}\). Then \(f\) is computable in polynomial time on raw bit lists (the identity as input and output encoding): by the reduction host machine, with the bits as input alphabet, \(e_O\) as output alphabet and the reduction host's step bound for \(p\) as time bound.

Cslib.Complexity.Host.reduction · 16 lines 
noncomputable def reduction (eO : c.Γ cO ≃ Bool) (f : List Bool → List Bool) (p : Polynomial ℕ)
    (hdone : c.prog done = .halt)
    (hrun : ∀ x, ∃ v S', RunLe c.prog (p.eval x.length)
      ⟨some start, false, update (fun _ => []) cX (x.map gX)⟩ ⟨some done, v, S'⟩ ∧
        S' cO = (f x).map eO.symm) :
    TM2ComputableInPolyTime (fun l : List Bool => l) (fun l : List Bool => l) f where
  tm := rtm c cX cO gX start done
  inputAlphabet := Equiv.refl Bool
  outputAlphabet := eO
  time := rtime c cX cO gX start done p
  outputsFun := fun x => by
    have h := rprog_run eO f p hdone hrun x
    unfold RunLe at h
    refine ⟨⟨Classical.choose h, ?_⟩, (Classical.choose_spec h).1⟩
    erw [List.map_id, initList_eq, Option.map_some, haltList_eq]
    exact (Classical.choose_spec h).2
Uses 13 · Used by 6
Statement 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 · Step bound of the reduction host · Reduction host machine · Exact-length runs of a TM2 machine · Runs within a step budget
Used byReversing and dropping the first bit is polynomial-time · The readout on raw bits in polynomial time · The checking machine in polynomial time · The layout in polynomial time · Decider host · Reduction host, canonical form

TheoremReduction host, canonical form#✓fully proved

Let \(c\) be a component machine with stacks \(c_X\) and \(c_O\) and labels \(\mathit{start}\) and \(\mathit{done}\), where the statement at \(\mathit{done}\) is the halting statement. Let \(g_X\) map bits to symbols of \(c_X\), let \(e_O\) be a bijection from the alphabet of \(c_O\) to the booleans, let \(f\) map bit lists to bit lists, and let \(p\) be a polynomial with coefficients in \(\mathbb{N}\). Suppose that for every bit list \(x\), the component started at \(\mathit{start}\) with internal state false, with \(g_X\) applied to each bit of \(x\) on \(c_X\) and every other stack empty, reaches the label \(\mathit{done}\) in at most \(p(|x|)\) steps with stack \(c_O\) holding exactly \(e_O^{-1}\) applied to each bit of \(f(x)\). Then \(f\) is polynomial-time computable for the canonical bitstring encodings.

theorem isPolyTime_reduction (eO : c.Γ cO ≃ Bool) (f : List Bool → List Bool)
    (p : Polynomial ℕ) (hdone : c.prog done = .halt)
    (hrun : ∀ x, ∃ v S', RunLe c.prog (p.eval x.length)
      ⟨some start, false, update (fun _ => []) cX (x.map gX)⟩ ⟨some done, v, S'⟩ ∧
        S' cO = (f x).map eO.symm) :
    ComplexityTheory.IsPolyTime f
Uses 15 · Used by 8
Statement usesComponent machine · 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 computable functions · Runs within a step budget
Proof usesPolynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Reduction host · Polynomial-time TM2-computable functions are closed under composition
Used byPayload normalization is polynomial-time · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · SUBSET-SUM to PARTITION map is polynomial-time · PARTITION to SUBSET-SUM map is polynomial-time · PARTITION doubling pass is polynomial-time · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time · Emitter reductions out of SAT are polynomial-time

TheoremDecider host#✓fully proved

Let \(c\) be a component machine with stacks \(c_X\) and \(c_O\) and labels \(\mathit{start}\) and \(\mathit{done}\), where the statement at \(\mathit{done}\) is the halting statement. Let \(g_X\) map bits to symbols of \(c_X\), let \(e_O\) be a bijection from the alphabet of \(c_O\) to the booleans, let \(L\) map bit lists to booleans, and let \(p\) be a polynomial with coefficients in \(\mathbb{N}\). Suppose that for every bit list \(x\), the component started at \(\mathit{start}\) with internal state false, with \(g_X\) applied to each bit of \(x\) on \(c_X\) and every other stack empty, reaches the label \(\mathit{done}\) in at most \(p(|x|)\) steps with exactly the one symbol \(e_O^{-1}(L(x))\) on \(c_O\). Then \(L\) is polynomial-time computable for the canonical bitstring encodings, that is, \(L\) belongs to the class \(\mathrm{P}\) of decision problems decidable in polynomial time.

The proof applies the reduction host to \(x \mapsto [L(x)]\), read with the one-bit encoding of the booleans.

theorem isPolyTime_decider (eO : c.Γ cO ≃ Bool) (L : List Bool → Bool) (p : Polynomial ℕ)
    (hdone : c.prog done = .halt)
    (hrun : ∀ x, ∃ v S', RunLe c.prog (p.eval x.length)
      ⟨some start, false, update (fun _ => []) cX (x.map gX)⟩ ⟨some done, v, S'⟩ ∧
        S' cO = [eO.symm (L x)]) :
    ComplexityTheory.IsPolyTime L
Uses 14 · Used by 1
Statement usesComponent machine · 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 computable functions · Runs within a step budget
Proof usesPolynomial-time decoder of the canonical bit-list encoding · Reduction host · Polynomial-time TM2-computable functions are closed under composition
Used byThe marking algorithm is polynomial-time

The verifier host

DefinitionRelabelling in the verifier host#✓fully proved

Given labels \(\mathit{yes}\) and \(\mathit{no}\) of a component machine \(c\), a label \(l\) of \(c\) is sent to the host label that starts the cleanup with answer true if \(l = \mathit{yes}\), to the host label that starts the cleanup with answer false if \(l \ne \mathit{yes}\) and \(l = \mathit{no}\), and to the host label that runs the component at \(l\) otherwise.

def φV (l : c.L) : HLab c :=
  if l = yes then .clean true else if l = no then .clean false else .comp l
Uses 2 · Used by 3
Statement usesComponent machine · Labels of the generic host
Used byThe verifier host embeds the component · Verifier host program · The verifier host's run

DefinitionReading a bit of \(x\)#✓fully proved

On the pair alphabet of the \(x \# w\) input, the symbol that encodes a bit \(b\) of \(x\) (the left injection of \(b\)) is read as the bit \(b\); every other symbol, the separator \(\#\) or a bit of \(w\) (both right injections), is read as no bit.

def dX : Verifier.G → Option Bool
  | .inl b => some b
  | _ => none
Uses 1 · Used by 2
Statement usesWork alphabet of the dense-SAT verifier
Used byVerifier host program · The verifier host's run

DefinitionReading a bit of \(w\)#✓fully proved

On the pair alphabet of the \(x \# w\) input, the symbol that encodes a bit \(b\) of \(w\) (the right injection of \(\mathrm{some}\,b\)) is read as the bit \(b\); every other symbol, a bit of \(x\) (a left injection) or the separator \(\#\) (the right injection of \(\mathrm{none}\)), is read as no bit.

def dW : Verifier.G → Option Bool
  | .inr (some b) => some b
  | _ => none
Uses 1 · Used by 2
Statement usesWork alphabet of the dense-SAT verifier
Used byVerifier host program · The verifier host's run

DefinitionVerifier host program#✓fully proved

The program of the verifier host for a component machine \(c\) with stacks \(c_X\) and \(c_W\), encodings \(g_X\) and \(g_W\) of bits as symbols of \(c_X\) and \(c_W\), and labels \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\), on the host stacks with the work alphabet of the dense-SAT verifier on the input stack. On an input \(x \# w\) in the pair encoding, phase 0 moves the symbols on top of the input stack that encode bits of \(x\) onto the buffer \(X_1\) with the bit-moving loop, then moves \(X_1\) onto the host's copy of \(c_X\) re-encoded by \(g_X\) (so in the original order); it pops one symbol off the input stack (the separator \(\#\)); it moves the symbols that encode bits of \(w\) onto the buffer \(W_1\) and then \(W_1\) onto the host's copy of \(c_W\) re-encoded by \(g_W\); then it sets the state to false and goes to the renamed label of \(\mathit{start}\). Here a label of \(c\) is renamed to the cleanup label with answer true if it is \(\mathit{yes}\), to the cleanup label with answer false if it is \(\mathit{no}\) but not \(\mathit{yes}\), and to the host's copy of itself otherwise. At the host's copy of a component label \(l\) it runs the component's statement at \(l\) on the host's copies of the component stacks, with every jump target renamed. The cleanup label with answer \(a\) pops every stack other than the output stack once per round, repeating while something was popped, and then goes to the output label with answer \(a\), which pushes \(a\) on the output stack and halts.

def vprog : HLab c → TM2.Stmt (HΓ c Verifier.G) (HLab c) Bool
  | .ph .m1 => moveB (Γ := HΓ c Verifier.G) .inp .X1 dX id (.ph .m1) (.ph .m2)
  | .ph .m2 => moveB (Γ := HΓ c Verifier.G) .X1 (.comp cX) some gX (.ph .m2) (.ph .sep)
  | .ph .sep => .pop .inp (fun s _ => s) (.goto fun _ => .ph .m3)
  | .ph .m3 => moveB (Γ := HΓ c Verifier.G) .inp .W1 dW id (.ph .m3) (.ph .m4)
  | .ph .m4 => moveB (Γ := HΓ c Verifier.G) .W1 (.comp cW) some gW (.ph .m4) (.ph .go)
  | .ph .go => .load (fun _ => false) (.goto fun _ => φV c yes no start)
  | .comp l => mapS (emb c Verifier.G) (φV c yes no) (c.prog l)
  | .clean ans => cleanS (cleanKs c .out) (.clean ans) (.fin ans)
  | .fin ans => .push .out (fun _ => ans) .halt
Uses 15 · Used by 4
Statement usesWork alphabet of the dense-SAT verifier · Component machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Phase-0 labels of the generic host · Cleanup stacks of the generic host · Reading a bit of \(w\) · Reading a bit of \(x\) · The component's stacks inside a host · Relabelling in the verifier host · Translating a statement along a stack embedding · Flag bit of a machine state · Cleanup round · Bit-moving loop
Used byThe verifier host embeds the component · Verifier host · The verifier host's run · The verifier host machine

DefinitionThe verifier host machine#✓fully proved

The verifier host as a finite multi-stack Turing machine for a component machine \(c\): its stacks are the host stacks, with the pair alphabet on the input stack, the alphabets of \(c\) on the component's stacks and bits on the other stacks; its labels are the host labels and its program is the verifier host program; it starts at the first phase-0 label with a boolean internal state, initially false; it reads its input from the input stack and leaves its output on the output stack.

def vtm : FinTM2 where
  K := HK c
  k₀ := .inp
  k₁ := .out
  Γ := HΓ c Verifier.G
  Λ := HLab c
  main := .ph .m1
  σ := Bool
  initialState := false
  Γk₀Fin := (inferInstance : Fintype Verifier.G)
  m := vprog c cX cW gX gW start yes no
Uses 9 · Used by 3
Statement usesWork alphabet of the dense-SAT verifier · Component machine · Stacks of the generic host · Labels of the generic host · Labels of the generic host as a sum type · Alphabets of the generic host · Phase-0 labels of the generic host · The list of host stacks · Verifier host program
Used byVerifier host · The verifier host's run · Step bound of the verifier host

DefinitionStep bound of the verifier host#✓fully proved

Let \(c\) be a component machine with stacks \(c_X\) and \(c_W\), encodings \(g_X\) and \(g_W\) of bits as symbols of \(c_X\) and \(c_W\), and labels \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\), and let \(B\) be the push bound of the verifier host machine built from these data. For a polynomial \(p\) with natural-number coefficients, the step bound of the verifier host is the polynomial in the variable \(X\)

\[(B + 1)(2X + 4 + p) + X + 2.\]

At an input length \(n\) it counts phase 0 and the component, at most \(2n + 4 + p(n)\) steps, then the cleanup, which takes at most one step more than the longest stack, of length at most \(n\) plus \(B\) times the steps so far, and the output step.

noncomputable def vtime (p : Polynomial ℕ) : Polynomial ℕ :=
  Polynomial.C (TM2Composition.pushBound (vtm c cX cW gX gW start yes no) + 1) *
      (Polynomial.C 2 * Polynomial.X + Polynomial.C 4 + p) + Polynomial.X + Polynomial.C 2
Uses 3 · Used by 2
Statement usesComponent machine · The verifier host machine · Push bound of a finite multi-stack Turing machine
Used byVerifier host · The verifier host's run

TheoremThe verifier host embeds the component#✓fully proved

Let \(c\) be a component machine with stacks \(c_X\) and \(c_W\), maps \(g_X\) and \(g_W\) from bits to the alphabets of \(c_X\) and \(c_W\), and labels \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\), and suppose that the statement of \(c\) at \(\mathit{yes}\) and the statement of \(c\) at \(\mathit{no}\) are the halt statement. Rename the labels of \(c\) by sending \(\mathit{yes}\) to the cleanup label with answer true, \(\mathit{no}\) (when it differs from \(\mathit{yes}\)) to the cleanup label with answer false, and every other label \(l\) to the host's copy of \(l\), and embed the stacks of \(c\) as the host's copies over the work alphabet of the dense-SAT verifier. Then the verifier host program built from \(c_X\), \(c_W\), \(g_X\), \(g_W\), \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\) embeds \(c\): for every label \(l\) of \(c\), either the statement of \(c\) at \(l\) is the halt statement, or the host's statement at the renamed label of \(l\) is the statement of \(c\) at \(l\) with stacks and labels translated.

theorem embeds_vprog (hyes : c.prog yes = .halt) (hno : c.prog no = .halt) :
    Embeds (emb c Verifier.G) (φV c yes no) c.prog (vprog c cX cW gX gW start yes no)
Uses 10 · Used by 1
Statement usesWork alphabet of the dense-SAT verifier · Component machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · The component's stacks inside a host · Verifier host program · Relabelling in the verifier host · Embedding of a machine in a host
Proof usesTranslating a statement along a stack embedding
Used byThe verifier host's run

TheoremThe verifier host's run#✓fully proved

Let \(c\) be a component machine with stacks \(c_X \ne c_W\), maps \(g_X\) and \(g_W\) from bits to the alphabets of \(c_X\) and \(c_W\), and labels \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\) with \(\mathit{yes} \ne \mathit{no}\), where the program halts at \(\mathit{yes}\) and at \(\mathit{no}\). Let \(f\) assign a boolean to each pair of bit lists and let \(p\) be a polynomial with natural number coefficients. Suppose that for all bit lists \(x\) and \(w\), the component started at \(\mathit{start}\) with state false, the bits of \(x\) mapped by \(g_X\) on \(c_X\), the bits of \(w\) mapped by \(g_W\) on \(c_W\) and every other stack empty reaches the label \(\mathit{yes}\) if \(f(x, w)\) is true and \(\mathit{no}\) otherwise within \(p(|x| + |w|)\) steps. Then for all bit lists \(x\) and \(w\), with \(n\) the length of the pair encoding of \((x, w)\), the verifier host program started at its first phase-0 label with state false, the pair encoding of \((x, w)\) on the input stack and every other stack empty halts within \(T(n)\) steps, where \(T\) is the verifier host's step bound for \(p\), with state false, the one-element list \([f(x, w)]\) on the output stack and every other stack empty.

theorem vprog_run (f : List Bool → List Bool → Bool) (p : Polynomial ℕ) (hXW : cX ≠ cW)
    (hyn : yes ≠ no) (hyes : c.prog yes = .halt) (hno : c.prog no = .halt)
    (hrun : ∀ x w, ∃ v S', RunLe c.prog (p.eval (x.length + w.length))
      ⟨some start, false, update (update (fun _ => []) cX (x.map gX)) cW (w.map gW)⟩
      ⟨some (if f x w then yes else no), v, S'⟩)
    (x w : List Bool) :
    RunLe (vprog c cX cW gX gW start yes no)
      ((vtime c cX cW gX gW start yes no p).eval (Verifier.pairEncode (x, w)).length)
      ⟨some (.ph .m1), false, update (fun _ => []) .inp (Verifier.pairEncode (x, w))⟩
      ⟨none, false, update (fun _ => []) .out [f x w]⟩
Uses 29 · Used by 1
Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Component machine · Stacks of the generic host · Labels of the generic host · Alphabets of the generic host · Phase-0 labels of the generic host · Verifier host program · Step bound of the verifier host · Runs within a step budget
Proof usesAgreement with the embedded component · Cleanup in a host · Reading a bit of \(w\) · Reading a bit of \(x\) · The component's stacks inside a host · The verifier host embeds the component · Moving a bit block through a buffer · Stack lengths grow by at most the push bound per step · Stack lengths when only one stack is filled · The verifier host machine · Relabelling in the verifier host · Evaluation of a natural-number polynomial is monotone · Push bound of a finite multi-stack Turing machine · Agreement of host and sub-machine stacks · Frame condition for a stack embedding · Stack embedding · Run embedding for bounded runs · Exact-length runs of a TM2 machine · A single step executes the statement at the current label
Used byVerifier host

DefinitionVerifier host#✓fully proved

Let \(c\) be a component machine with stacks \(c_X \ne c_W\), maps \(g_X\) and \(g_W\) from bits to the alphabets of \(c_X\) and \(c_W\), and labels \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\) with \(\mathit{yes} \ne \mathit{no}\), where the program halts at \(\mathit{yes}\) and at \(\mathit{no}\). Let \(f\) assign a boolean to each pair of bit lists and let \(p\) be a polynomial with natural number coefficients. Suppose that for all bit lists \(x\) and \(w\), the component started at \(\mathit{start}\) with state false, the bits of \(x\) mapped by \(g_X\) on \(c_X\), the bits of \(w\) mapped by \(g_W\) on \(c_W\) and every other stack empty reaches the label \(\mathit{yes}\) if \(f(x, w)\) is true and \(\mathit{no}\) otherwise within \(p(|x| + |w|)\) steps. Then the verifier host machine computes \((x, w) \mapsto f(x, w)\) in polynomial time, with the verifier host's step bound for \(p\) as time bound: on the pair encoding of \((x, w)\), over the pair alphabet, it outputs the one-element bit list \([f(x, w)]\).

Cslib.Complexity.Host.verifier · 17 lines 
noncomputable def verifier (f : List Bool → List Bool → Bool) (p : Polynomial ℕ) (hXW : cX ≠ cW)
    (hyn : yes ≠ no) (hyes : c.prog yes = .halt) (hno : c.prog no = .halt)
    (hrun : ∀ x w, ∃ v S', RunLe c.prog (p.eval (x.length + w.length))
      ⟨some start, false, update (update (fun _ => []) cX (x.map gX)) cW (w.map gW)⟩
      ⟨some (if f x w then yes else no), v, S'⟩) :
    TM2ComputableInPolyTime Verifier.pairEncode (fun b : Bool => [b]) (fun q => f q.1 q.2) where
  tm := vtm c cX cW gX gW start yes no
  inputAlphabet := Equiv.refl Verifier.G
  outputAlphabet := Equiv.refl Bool
  time := vtime c cX cW gX gW start yes no p
  outputsFun := fun q => by
    obtain ⟨x, w⟩ := q
    have h := vprog_run f p hXW hyn hyes hno hrun x w
    unfold RunLe at h
    refine ⟨⟨Classical.choose h, ?_⟩, (Classical.choose_spec h).1⟩
    erw [List.map_id, List.map_id, initList_eq, Option.map_some, haltList_eq]
    exact (Classical.choose_spec h).2
Uses 15 · Used by 1
Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Component 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 · Verifier host program · The verifier host's run · Step bound of the verifier host · The verifier host machine · Exact-length runs of a TM2 machine · Runs within a step budget
Used byVerifier host, canonical form

TheoremVerifier host, canonical form#✓fully proved

Let \(c\) be a component machine with distinct stacks \(c_X\) and \(c_W\) and labels \(\mathit{start}\), \(\mathit{yes}\) and \(\mathit{no}\), where \(\mathit{yes} \ne \mathit{no}\) and the statements at \(\mathit{yes}\) and \(\mathit{no}\) are the halting statement. Let \(g_X\) and \(g_W\) map bits to symbols of \(c_X\) and \(c_W\), let \(f\) assign a boolean \(f(x, w)\) to all bit lists \(x\) and \(w\), and let \(p\) be a polynomial with coefficients in \(\mathbb{N}\). Suppose that for all bit lists \(x\) and \(w\), the component started at \(\mathit{start}\) with internal state false, with \(g_X\) applied to each bit of \(x\) on \(c_X\), \(g_W\) applied to each bit of \(w\) on \(c_W\) and every other stack empty, reaches in at most \(p(|x| + |w|)\) steps the label \(\mathit{yes}\) if \(f(x, w)\) is true and the label \(\mathit{no}\) if it is false. Then the map \((x, w) \mapsto f(x, w)\) on pairs of bit lists is polynomial-time computable for the canonical bitstring encodings.

theorem isPolyTime_verifier (f : List Bool → List Bool → Bool) (p : Polynomial ℕ)
    (hXW : cX ≠ cW) (hyn : yes ≠ no) (hyes : c.prog yes = .halt) (hno : c.prog no = .halt)
    (hrun : ∀ x w, ∃ v S', RunLe c.prog (p.eval (x.length + w.length))
      ⟨some start, false, update (update (fun _ => []) cX (x.map gX)) cW (w.map gW)⟩
      ⟨some (if f x w then yes else no), v, S'⟩) :
    ComplexityTheory.IsPolyTime fun q : List Bool × List Bool => f q.1 q.2
Uses 16 · Used by 4
Statement usesComponent machine · 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 computable functions · Runs within a step budget
Proof usesPolynomial-time conversion to the verifier's pair encoding · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Verifier host · Polynomial-time TM2-computable functions are closed under composition
Used by3-COLOR is in NP · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier · SUBSET-SUM is in NP · HAMPATH is in NP

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.