Skip to content

Encoding converters for the Cook-Levin reduction

24 fully proved

From w # y to the canonical pair encoding

InductiveStacks of the converter to the canonical pair encoding#✓fully proved

The converter has four stacks: the input stack, whose symbols are left-tagged bits, right-tagged bits and the separator (the input is the bits of a first bit list tagged left, a separator, then the bits of a second bit list tagged right); the output stack, holding bits; and two stashes, holding the bits of the first and of the second list.

inductive Stk | inp | out | fst | snd
  deriving DecidableEq
Used by 7
Used byCanonical bit-list decoder · Run of the pair-to-canonical converter · Program of the converter to the canonical pair encoding · Runs of the converter to the canonical pair encoding · Stack contents of the converter to the canonical pair encoding · Machine converting the separator form of a pair to its canonical encoding · Stack alphabets of the separator-to-canonical converter

DefinitionStack alphabets of the separator-to-canonical converter#✓fully proved

The input stack of the converter from the separator form of a pair to its canonical encoding has the verifier's alphabet, and each of its other three stacks (the output and the two stashes) has the alphabet of bits.

@[reducible] def Γ : Stk → Type
  | .inp => Verifier.G
  | _ => Bool
Uses 2 · Used by 6
Statement usesStacks of the converter to the canonical pair encoding · Work alphabet of the dense-SAT verifier
Used byCanonical bit-list decoder · Run of the pair-to-canonical converter · Program of the converter to the canonical pair encoding · Runs of the converter to the canonical pair encoding · Stack contents of the converter to the canonical pair encoding · Machine converting the separator form of a pair to its canonical encoding

InductiveLabels of the converter to the canonical pair encoding#✓fully proved

The machine that turns the separated form of a pair \((x, w)\) of bit lists (the bits of \(x\) tagged left, a separator, then the bits of \(w\) tagged right) into the canonical encoding of the pair has five labels: reading the first part, reading the second part, emitting the second part, writing the separator, and emitting the first part.

inductive Lab | readFst | readSnd | emitSnd | sep | emitFst
  deriving DecidableEq
Used by 5
Used byCanonical bit-list decoder · Run of the pair-to-canonical converter · Program of the converter to the canonical pair encoding · Runs of the converter to the canonical pair encoding · Machine converting the separator form of a pair to its canonical encoding

AbbreviationStates of the converter to the canonical pair encoding#✓fully proved

A state of the converter is either empty or one symbol of the verifier's input alphabet, that is, a left-tagged bit, a right-tagged bit or the separator.

The state holds the last symbol popped; bits popped from the stashes are stored as left-tagged bits.

abbrev St := Option Verifier.G
Uses 1 · Used by 8
Statement usesWork alphabet of the dense-SAT verifier
Used byBit carried by a converter state · Canonical bit-list decoder · Run of the pair-to-canonical converter · Left-tagged state test · Right-tagged state test · Program of the converter to the canonical pair encoding · Runs of the converter to the canonical pair encoding · Machine converting the separator form of a pair to its canonical encoding

DefinitionLeft-tagged state test#✓fully proved

For a state \(s\) of the pair-to-canonical converter (either empty or a symbol of the verifier alphabet), the test is true exactly when \(s\) is a left-tagged bit \(\mathrm{inl}\,b\) for some bit \(b\), and false when \(s\) is empty, the separator \(\mathrm{inr}(\mathrm{none})\) or a right-tagged bit.

def isFst : St → Bool
  | some (.inl _) => true
  | _ => false
Uses 2 · Used by 2
Statement usesStates of the converter to the canonical pair encoding · Work alphabet of the dense-SAT verifier
Used byRun of the pair-to-canonical converter · Program of the converter to the canonical pair encoding

DefinitionRight-tagged state test#✓fully proved

For a state \(s\) of the pair-to-canonical converter (either empty or a symbol of the verifier alphabet), the test is true exactly when \(s\) is a right-tagged bit \(\mathrm{inr}(\mathrm{some}\,b)\) for some bit \(b\), and false when \(s\) is empty, the separator \(\mathrm{inr}(\mathrm{none})\) or a left-tagged bit.

def isSnd : St → Bool
  | some (.inr (some _)) => true
  | _ => false
Uses 2 · Used by 2
Statement usesStates of the converter to the canonical pair encoding · Work alphabet of the dense-SAT verifier
Used byRun of the pair-to-canonical converter · Program of the converter to the canonical pair encoding

DefinitionBit carried by a converter state#✓fully proved

For a state \(s\) of the pair-to-canonical converter (either empty or a symbol of the verifier alphabet), the bit of \(s\) is \(b\) when \(s\) is a left-tagged bit \(\mathrm{inl}\,b\) or a right-tagged bit \(\mathrm{inr}(\mathrm{some}\,b)\), and \(\mathrm{false}\) when \(s\) is empty or the separator \(\mathrm{inr}(\mathrm{none})\).

def bit : St → Bool
  | some (.inl b) => b
  | some (.inr (some b)) => b
  | _ => false
Uses 2 · Used by 2
Statement usesStates of the converter to the canonical pair encoding · Work alphabet of the dense-SAT verifier
Used byRun of the pair-to-canonical converter · Program of the converter to the canonical pair encoding

DefinitionProgram of the converter to the canonical pair encoding#✓fully proved

The machine has an input stack of symbols, each a left-tagged bit, a right-tagged bit or the separator, and three stacks of bits: the output and two stashes. Its program first pops input symbols and pushes the bit of each left-tagged one onto the first stash, until the input is empty or the symbol popped is not a left-tagged bit. It then pops input symbols and pushes the bit of each right-tagged one onto the second stash, until the input is empty or the symbol popped is not a right-tagged bit. Next it pops each bit \(b\) of the second stash and pushes false, \(b\), true onto the output, and then pushes a single false. Finally it pops each bit \(b\) of the first stash and pushes false, true, \(b\), true, true, true onto the output, and halts when the first stash is empty.

Each output block is pushed in reverse, so that it reads true, \(b\), false (respectively true, true, true, \(b\), true, false) from the top.

Cslib.Complexity.DenseSAT.ToCanonical.prog · 21 lines 
def prog : Lab → TM2.Stmt Γ Lab St
  | .readFst =>
      .pop .inp (fun _ o => o) <| .branch isFst
        (.push .fst bit <| .goto fun _ => .readFst)
        (.goto fun _ => .readSnd)
  | .readSnd =>
      .pop .inp (fun _ o => o) <| .branch isSnd
        (.push .snd bit <| .goto fun _ => .readSnd)
        (.goto fun _ => .emitSnd)
  | .emitSnd =>
      .pop .snd (fun _ o => o.map Sum.inl) <| .branch isFst
        (.push .out (fun _ => false) <| .push .out bit <| .push .out (fun _ => true) <|
          .goto fun _ => .emitSnd)
        (.goto fun _ => .sep)
  | .sep => .push .out (fun _ => false) <| .goto fun _ => .emitFst
  | .emitFst =>
      .pop .fst (fun _ o => o.map Sum.inl) <| .branch isFst
        (.push .out (fun _ => false) <| .push .out (fun _ => true) <| .push .out bit <|
          .push .out (fun _ => true) <| .push .out (fun _ => true) <|
          .push .out (fun _ => true) <| .goto fun _ => .emitFst)
        .halt
Uses 8 · Used by 4
Statement usesLabels of the converter to the canonical pair encoding · States of the converter to the canonical pair encoding · Stacks of the converter to the canonical pair encoding · Bit carried by a converter state · Left-tagged state test · Right-tagged state test · Stack alphabets of the separator-to-canonical converter · Work alphabet of the dense-SAT verifier
Used byCanonical bit-list decoder · Run of the pair-to-canonical converter · Runs of the converter to the canonical pair encoding · Machine converting the separator form of a pair to its canonical encoding

DefinitionMachine converting the separator form of a pair to its canonical encoding#✓fully proved

The multi-stack Turing machine with the four stacks of the converter to the canonical pair encoding (input, output and two stashes), whose input stack holds symbols of the verifier's alphabet (left-tagged bits, right-tagged bits and the separator) and whose other stacks hold bits, reading its input from the input stack and leaving its output on the output stack, with the five labels of that converter and start label \(\mathrm{readFst}\), the converter's states (empty or one verifier symbol) as internal states, initially empty, and the program of the converter to the canonical pair encoding. It pops input symbols, pushing the bit of each left-tagged one onto the first stash, until the input is empty or the symbol popped is not a left-tagged bit. It then pops input symbols, pushing the bit of each right-tagged one onto the second stash, until the input is empty or the symbol popped is not a right-tagged bit. Next it pops each bit \(b\) of the second stash and pushes a block reading true, \(b\), false from the top onto the output, pushes a single false, pops each bit \(b\) of the first stash and pushes a block reading true, true, true, \(b\), true, false from the top, and halts when the first stash is empty.

def tm : FinTM2 where
  K := Stk
  k₀ := .inp
  k₁ := .out
  Γ := Γ
  Λ := Lab
  main := .readFst
  σ := St
  initialState := none
  Γk₀Fin := (inferInstance : Fintype Verifier.G)
  m := prog
Uses 6 · Used by 1
Statement usesLabels of the converter to the canonical pair encoding · States of the converter to the canonical pair encoding · Stacks of the converter to the canonical pair encoding · Program of the converter to the canonical pair encoding · Stack alphabets of the separator-to-canonical converter · Work alphabet of the dense-SAT verifier
Used byCanonical bit-list decoder

DefinitionStack contents of the converter to the canonical pair encoding#✓fully proved

Given a list \(i\) of input symbols and bit lists \(o\), \(a\) and \(b\), this is the contents of the four stacks of the converter with \(i\) on the input stack, \(o\) on the output stack, \(a\) on the first stash and \(b\) on the second stash.

def stk (i : List Verifier.G) (o a b : List Bool) : ∀ k, List (Γ k)
  | .inp => i
  | .out => o
  | .fst => a
  | .snd => b
Uses 3 · Used by 2
Statement usesStacks of the converter to the canonical pair encoding · Stack alphabets of the separator-to-canonical converter · Work alphabet of the dense-SAT verifier
Used byCanonical bit-list decoder · Run of the pair-to-canonical converter

AbbreviationRuns of the converter to the canonical pair encoding#✓fully proved

For a natural number \(n\) and configurations \(c\) and \(d\) of the converter, this is the proposition that \(n\) steps of its program lead from \(c\) to \(d\): applying the step function \(n\) times to \(c\) is defined at every step (no configuration before the last one is halted) and gives \(d\).

abbrev Run (n : ℕ) (c d : TM2.Cfg Γ Lab St) : Prop := TM2Program.Run prog n c d
Uses 6 · Used by 1
Statement usesLabels of the converter to the canonical pair encoding · States of the converter to the canonical pair encoding · Stacks of the converter to the canonical pair encoding · Program of the converter to the canonical pair encoding · Stack alphabets of the separator-to-canonical converter · Exact-length runs of a TM2 machine
Used byRun of the pair-to-canonical converter

TheoremRun of the pair-to-canonical converter#✓fully proved

Let \(x\) and \(w\) be bit lists, write \(x \# w\) for the verifier input of the pair \((x, w)\), and read \(1\) for true and \(0\) for false. Let \(\mathrm{encFst}(x)\) replace each bit \(b\) of \(x\) by \(1, 1, 1, b, 1, 0\) and \(\mathrm{encSnd}(w)\) replace each bit \(b\) of \(w\) by \(1, b, 0\). The program of the pair-to-canonical converter goes in exactly \(2|x| + 2|w| + 5\) steps from the configuration at label \(\mathrm{readFst}\) with empty state, \(x \# w\) on the input stack and the output stack and both stashes empty, to the halted configuration with empty state, empty input stack and stashes, and output stack reading \(\mathrm{encFst}(x)\), then \(0\), then \(\mathrm{encSnd}(w)\) from the top.

theorem convert_run (x w : List Bool) :
    Run (2 * x.length + 2 * w.length + 5)
      ⟨some .readFst, none, stk (Verifier.pairEncode (x, w)) [] [] []⟩
      ⟨none, none, stk [] (encFst x ++ false :: encSnd w) [] []⟩
Uses 16 · Used by 1
Statement usesConverter encoding of the first component · Converter encoding of the second component · Labels of the converter to the canonical pair encoding · Runs of the converter to the canonical pair encoding · States of the converter to the canonical pair encoding · Stacks of the converter to the canonical pair encoding · Stack contents of the converter to the canonical pair encoding · Stack alphabets of the separator-to-canonical converter · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)
Proof usesBit carried by a converter state · Left-tagged state test · Right-tagged state test · Program of the converter to the canonical pair encoding · Exact-length runs of a TM2 machine · A single step executes the statement at the current label
Used byCanonical bit-list decoder

DefinitionCanonical bit-list decoder#✓fully proved

This is a multi-stack Turing machine over the alphabet \(\mathrm{Bool}\), with time bound \(n + 2\), such that for every bit list \(x\), started on the canonical bitstring encoding of \(x\), it halts within \(n + 2\) steps, where \(n\) is the length of that encoding, with \(x\) on its output stack and all other stacks empty. So the identity on bit lists is computable in polynomial time from the canonical encoding to the raw bits.

Cslib.Complexity.DenseSAT.ToCanonical.computable · 19 lines 
noncomputable def computable :
    TM2ComputableInPolyTime Verifier.pairEncode
      (BitstringEncoding.toEncoding (α := List Bool × List Bool)).encode id where
  tm := tm
  inputAlphabet := Equiv.refl Verifier.G
  outputAlphabet := Equiv.refl Bool
  time := Polynomial.C 2 * Polynomial.X + Polynomial.C 3
  outputsFun := fun p => by
    obtain ⟨x, w⟩ := p
    unfold TM2OutputsInTime
    refine { steps := 2 * x.length + 2 * w.length + 5, evals_in_steps := ?_, steps_le_m := ?_ }
    · change (flip bind (TM2.step prog))^[_] (some (initList tm _)) =
        Option.map (haltList tm) (some _)
      erw [List.map_id, List.map_id, id, bitEncode_pair_eq, initList_tm, Option.map_some,
        haltList_tm]
      exact convert_run x w
    · simp only [Verifier.pairEncode, List.length_append, List.length_cons, List.length_map,
        Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_X, Polynomial.eval_C]
      omega
Uses 21 · Used by 3
Statement usesCanonical encoding of a pair of bit lists · Converter encoding of the first component · Converter encoding of the second component · Labels of the converter to the canonical pair encoding · States of the converter to the canonical pair encoding · Stacks of the converter to the canonical pair encoding · Run of the pair-to-canonical converter · Program of the converter to the canonical pair encoding · Stack contents of the converter to the canonical pair encoding · Machine converting the separator form of a pair to its canonical encoding · Stack alphabets of the separator-to-canonical converter · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · 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
Used byMapping the first component of a pair is polynomial-time · Every NP problem reduces to dense CNF-SAT · Every NP problem reduces to binary-index CNF-SAT

Bit lists: canonical encoding to raw bits and back

InductiveStacks of the bit-list converters#✓fully proved

The two bit-list converters use three stacks: the input stack, the output stack and one stash.

inductive BStk | inp | out | stash
  deriving DecidableEq
Used by 9
Used byStack contents of the bit-list converters · Polynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Program of the bit-list decoder · Program of the bit-list encoder · Runs of the bit-list decoder · Runs of the bit-list encoder · Machine decoding the canonical encoding of a bit list · Machine writing the canonical encoding of a bit list

InductiveLabels of the bit-list converters#✓fully proved

The two bit-list converters have two program labels, \(\mathrm{read}\) and \(\mathrm{emit}\).

inductive BLab | read | emit
  deriving DecidableEq
Used by 8
Used byPolynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Program of the bit-list decoder · Program of the bit-list encoder · Runs of the bit-list decoder · Runs of the bit-list encoder · Machine decoding the canonical encoding of a bit list · Machine writing the canonical encoding of a bit list

DefinitionStack contents of the bit-list converters#✓fully proved

For bit lists \(i\), \(o\) and \(a\), this assigns contents to the three stacks of the bit-list converters: \(i\) to the input stack, \(o\) to the output stack and \(a\) to the stash. Every stack alphabet is \(\mathrm{Bool}\).

def bstk (i o a : List Bool) : BStk → List Bool
  | .inp => i
  | .out => o
  | .stash => a
Uses 1 · Used by 2
Statement usesStacks of the bit-list converters
Used byPolynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding

DefinitionProgram of the bit-list decoder#✓fully proved

The program of the machine that decodes the canonical encoding of a bit list acts on the three stacks of the bit-list converters, all over bits, with an optional bit as internal state. At label \(\mathrm{read}\) it pops a symbol from the input stack into the state (which becomes empty if the input is empty). If that symbol is true, it pops a second symbol \(b\) into the state, pops and discards a third, pushes \(b\) onto the stash (false if the input ran out before \(b\)) and returns to \(\mathrm{read}\); otherwise it goes to \(\mathrm{emit}\). At label \(\mathrm{emit}\) it pops a bit from the stash, pushes it onto the output and returns to \(\mathrm{emit}\), and it halts when the stash is empty.

def prog : BLab → TM2.Stmt (fun _ : BStk => Bool) BLab (Option Bool)
  | .read =>
      .pop .inp (fun _ o => o) <| .branch (fun s => s == some true)
        (.pop .inp (fun _ o => o) <| .pop .inp (fun s _ => s) <|
          .push .stash (fun s => s.getD false) <| .goto fun _ => .read)
        (.goto fun _ => .emit)
  | .emit =>
      .pop .stash (fun _ o => o) <| .branch (fun s => s.isSome)
        (.push .out (fun s => s.getD false) <| .goto fun _ => .emit)
        .halt
Uses 2 · Used by 3
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters
Used byPolynomial-time decoder of the canonical bit-list encoding · Runs of the bit-list decoder · Machine decoding the canonical encoding of a bit list

DefinitionMachine decoding the canonical encoding of a bit list#✓fully proved

The multi-stack Turing machine with the three stacks of the bit-list converters (input, output and a stash), all over bits, reading its input from the input stack and leaving its output on the output stack, with the two labels \(\mathrm{read}\) and \(\mathrm{emit}\) and start label \(\mathrm{read}\), an optional bit as internal state, initially empty, and the program of the bit-list decoder. It repeatedly pops an input symbol; while that symbol is true, it pops two more and pushes the first of them onto the stash (false if the input ran out before it). Then it moves the stash, bit by bit, onto the output, and halts.

def tm : FinTM2 where
  K := BStk
  k₀ := .inp
  k₁ := .out
  Γ := fun _ => Bool
  Λ := BLab
  main := .read
  σ := Option Bool
  initialState := none
  Γk₀Fin := (inferInstance : Fintype Bool)
  m := prog
Uses 3 · Used by 1
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters · Program of the bit-list decoder
Used byPolynomial-time decoder of the canonical bit-list encoding

AbbreviationRuns of the bit-list decoder#✓fully proved

For a natural number \(n\) and configurations \(c\) and \(d\) of the machine decoding the canonical encoding of a bit list (each an optional label, an optional bit as internal state and the contents of the three bit stacks), this is the proposition that \(n\) steps of its program lead from \(c\) to \(d\): applying the step function \(n\) times to \(c\) is defined at every step (no configuration before the last one is halted) and gives \(d\).

abbrev Run (n : ℕ) (c d : TM2.Cfg (fun _ : BStk => Bool) BLab (Option Bool)) : Prop :=
  TM2Program.Run prog n c d
Uses 4 · Used by 1
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters · Program of the bit-list decoder · Exact-length runs of a TM2 machine
Used byPolynomial-time decoder of the canonical bit-list encoding

DefinitionPolynomial-time decoder of the canonical bit-list encoding#✓fully proved

This is a multi-stack Turing machine whose input and output alphabets are the bits, together with the polynomial time bound \(t(n) = n + 2\), such that for every bit list \(x\), whose canonical bitstring encoding has length \(n\), the machine started with that encoding on its input stack and all other stacks empty halts within \(t(n)\) steps with \(x\) on its output stack, all other stacks empty and its internal state back to the initial one. So the identity on bit lists is computable in polynomial time from the canonical encoding to the raw bits.

The canonical encoding writes each bit \(b\) of \(x\) as the three bits true, \(b\), false.

Cslib.Complexity.DenseSAT.DecodeBits.computable · 25 lines 
noncomputable def computable :
    TM2ComputableInPolyTime (BitstringEncoding.toEncoding (α := List Bool)).encode
      (fun l : List Bool => l) id where
  tm := tm
  inputAlphabet := Equiv.refl Bool
  outputAlphabet := Equiv.refl Bool
  time := Polynomial.X + Polynomial.C 2
  outputsFun := fun x => by
    unfold TM2OutputsInTime
    refine { steps := 2 * x.length + 2, evals_in_steps := ?_, steps_le_m := ?_ }
    · change (flip bind (TM2.step prog))^[_] (some (initList tm _)) =
        Option.map (haltList tm) (some _)
      have h := (read_run x [] [] none).trans (emit_run (x.reverse ++ []) [] none)
      simp only [List.append_nil, List.reverse_reverse, List.length_reverse] at h
      have hx : (BitstringEncoding.toEncoding (α := List Bool)).encode x = encSnd x :=
        bitEncode_list x
      erw [List.map_id, List.map_id, id, hx, initList_tm, Option.map_some, haltList_tm]
      exact h.of_eq (by omega)
    · change 2 * x.length + 2 ≤ (Polynomial.X + Polynomial.C 2).eval
        (BitstringEncoding.bitEncode x).length
      rw [bitEncode_list]
      simp only [encSnd, List.length_flatMap, List.length_cons, List.length_nil,
        Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_C, List.map_const',
        List.sum_replicate, smul_eq_mul]
      omega
Uses 17 · Used by 6
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters · Converter encoding of the second component · Runs of the bit-list decoder · Program of the bit-list decoder · Machine decoding the canonical encoding of a bit list · Stack contents of the bit-list converters · 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 · Exact-length runs of a TM2 machine · A single step executes the statement at the current label
Used byPolynomial-time maps run on unframed bit lists · The quadratic diagonal language is in P · The Cook–Levin reduction is polynomial-time · The dense-to-binary translation is polynomial-time in the canonical encoding · Decider host · Reduction host, canonical form

DefinitionProgram of the bit-list encoder#✓fully proved

The program of the machine that writes the canonical encoding of a bit list acts on the three stacks of the bit-list converters, all over bits, with an optional bit as internal state. At label \(\mathrm{read}\) it pops a bit from the input stack, pushes it onto the stash and returns to \(\mathrm{read}\); when the input is empty it goes to \(\mathrm{emit}\). At label \(\mathrm{emit}\) it pops a bit \(b\) from the stash, pushes false, \(b\) and true onto the output, so that the output then reads true, \(b\), false from the top, and returns to \(\mathrm{emit}\); it halts when the stash is empty.

def prog : BLab → TM2.Stmt (fun _ : BStk => Bool) BLab (Option Bool)
  | .read =>
      .pop .inp (fun _ o => o) <| .branch (fun s => s.isSome)
        (.push .stash (fun s => s.getD false) <| .goto fun _ => .read)
        (.goto fun _ => .emit)
  | .emit =>
      .pop .stash (fun _ o => o) <| .branch (fun s => s.isSome)
        (.push .out (fun _ => false) <| .push .out (fun s => s.getD false) <|
          .push .out (fun _ => true) <| .goto fun _ => .emit)
        .halt
Uses 2 · Used by 3
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters
Used byPolynomial-time encoder to the canonical bit-list encoding · Runs of the bit-list encoder · Machine writing the canonical encoding of a bit list

DefinitionMachine writing the canonical encoding of a bit list#✓fully proved

The multi-stack Turing machine with the three stacks of the bit-list converters (input, output and a stash), all over bits, reading its input from the input stack and leaving its output on the output stack, with the two labels \(\mathrm{read}\) and \(\mathrm{emit}\) and start label \(\mathrm{read}\), an optional bit as internal state, initially empty, and the program of the bit-list encoder. It moves the input, bit by bit, onto the stash. Then it pops the stash bit by bit, pushing for each bit \(b\) the three bits false, \(b\), true onto the output, so that each block reads true, \(b\), false from the top, and halts.

def tm : FinTM2 where
  K := BStk
  k₀ := .inp
  k₁ := .out
  Γ := fun _ => Bool
  Λ := BLab
  main := .read
  σ := Option Bool
  initialState := none
  Γk₀Fin := (inferInstance : Fintype Bool)
  m := prog
Uses 3 · Used by 1
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters · Program of the bit-list encoder
Used byPolynomial-time encoder to the canonical bit-list encoding

AbbreviationRuns of the bit-list encoder#✓fully proved

For a natural number \(n\) and configurations \(c\) and \(d\) of the machine writing the canonical encoding of a bit list (each an optional label, an optional bit as internal state and the contents of the three bit stacks), this is the proposition that \(n\) steps of its program lead from \(c\) to \(d\): applying the step function \(n\) times to \(c\) is defined at every step (no configuration before the last one is halted) and gives \(d\).

abbrev Run (n : ℕ) (c d : TM2.Cfg (fun _ : BStk => Bool) BLab (Option Bool)) : Prop :=
  TM2Program.Run prog n c d
Uses 4 · Used by 1
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters · Program of the bit-list encoder · Exact-length runs of a TM2 machine
Used byPolynomial-time encoder to the canonical bit-list encoding

DefinitionPolynomial-time encoder to the canonical bit-list encoding#✓fully proved

This is a multi-stack Turing machine whose input and output alphabets are the bits, together with the polynomial time bound \(t(n) = 2n + 2\), such that for every bit list \(x\) of length \(n\), the machine started with \(x\) on its input stack and all other stacks empty halts within \(t(n)\) steps with the canonical bitstring encoding of \(x\) on its output stack, all other stacks empty and its internal state back to the initial one. So the identity on bit lists is computable in polynomial time from the raw bits to the canonical encoding.

The canonical encoding writes each bit \(b\) of \(x\) as the three bits true, \(b\), false.

Cslib.Complexity.DenseSAT.EncodeBits.computable · 20 lines 
noncomputable def computable :
    TM2ComputableInPolyTime (fun l : List Bool => l)
      (BitstringEncoding.toEncoding (α := List Bool)).encode id where
  tm := tm
  inputAlphabet := Equiv.refl Bool
  outputAlphabet := Equiv.refl Bool
  time := Polynomial.C 2 * Polynomial.X + Polynomial.C 2
  outputsFun := fun x => by
    unfold TM2OutputsInTime
    refine { steps := 2 * x.length + 2, evals_in_steps := ?_, steps_le_m := ?_ }
    · change (flip bind (TM2.step prog))^[_] (some (initList tm _)) =
        Option.map (haltList tm) (some _)
      have h := (read_run x [] [] none).trans (emit_run (x.reverse ++ []) [] none)
      simp only [List.append_nil, List.reverse_reverse, List.length_reverse] at h
      have hx : (BitstringEncoding.toEncoding (α := List Bool)).encode x = encSnd x :=
        bitEncode_list x
      erw [List.map_id, List.map_id, id, hx, initList_tm, Option.map_some, haltList_tm]
      exact h.of_eq (by omega)
    · simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_X, Polynomial.eval_C]
      omega
Uses 17 · Used by 5
Statement usesLabels of the bit-list converters · Stacks of the bit-list converters · Converter encoding of the second component · Runs of the bit-list encoder · Program of the bit-list encoder · Machine writing the canonical encoding of a bit list · Stack contents of the bit-list converters · 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 · Exact-length runs of a TM2 machine · A single step executes the statement at the current label
Used byProblems in P are decided in polynomial time by single-tape machines · Polynomial-time maps run on unframed bit lists · The Cook–Levin reduction is polynomial-time · The dense-to-binary translation is polynomial-time in the canonical encoding · Reduction host, canonical form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.