Correctness of the uniform tableau circuit

The tableau circuit of a multi-tape machine (Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean) computes the run: on an input x of length n, for T steps with n < 2 T, the wire of each feature at time t ≤ T carries the value of that feature in the configuration after t steps (Cslib.Circuits.Boolean.Tableau.invariant_le). In particular the output wire is true exactly when the output written after T steps is [true] (Cslib.Circuits.Boolean.Tableau.evalOutput_gates), and the tableau circuit outputs this value (Cslib.Circuits.Boolean.Tableau.eval_circuit).

The proof follows the blocks. In block t + 1, the scan accumulates the symbols under the heads across the columns, the global gates compute the situation and the attributes of the action, and the gadget of each feature computes the disjunction of its terms, which is the step equation of the feature.

Main definitions

• Cslib.Circuits.Boolean.Tableau.val: the value of a numbered tableau wire.
• Cslib.Circuits.Boolean.Tableau.colSem, Cslib.Circuits.Boolean.Tableau.gfSem: the column and global features of a machine configuration.
• Cslib.Circuits.Boolean.Tableau.Invariant: the agreement of feature wires with the run.

Main results

• Cslib.Circuits.Boolean.Tableau.invariant_le: the features at every time t ≤ T.
• Cslib.Circuits.Boolean.Tableau.evalOutput_gates: the output wire carries the answer.
• Cslib.Circuits.Boolean.Tableau.eval_circuit: the tableau circuit outputs the answer.

References

• R. E. Ladner, The circuit value problem is log space complete for P
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

Values of wires

def Cslib.Circuits.Boolean.Tableau.opVal : Op → Bool → Bool → Bool

The value of a De Morgan gate from its operation and its first two arguments.

noncomputable def Cslib.Circuits.Boolean.Tableau.val {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (T : ℕ) (x : List Bool) (w : ℕ) : Bool

The value of wire w of the tableau of tm for T steps, on the input x.

theorem Cslib.Circuits.Boolean.Tableau.val_add {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} {g : ℕ} (hg : g < numGates k State T) : val tm T x (x.length + g) = interpretation (gateCode tm x.length T g).1 fun (a : Fin (signature.Arity (gateCode tm x.length T g).1)) => (gateCode tm x.length T g).2[↑a]?.elim false (val tm T x)

The value of a numbered gate is its operation applied to the values of its arguments.

The features of configurations

def Cslib.Circuits.Boolean.Tableau.colSem {k : ℕ} {State : Type} (T : ℕ) {input : List Bool} (cfg : Turing.Cfg k Bool State input) (c : ℕ) : ColFeat k → Bool

The value of a column feature in column c of a configuration: the input head at c, the work heads and the work cells at c - T.

def Cslib.Circuits.Boolean.Tableau.gfSem {k : ℕ} {State : Type} [DecidableEq State] {input : List Bool} (cfg : Turing.Cfg k Bool State input) : GFeat State → Bool

The value of a global feature of a configuration.

noncomputable def Cslib.Circuits.Boolean.Tableau.actSem {k : ℕ} {State : Type} [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {input : List Bool} (cfg : Turing.Cfg k Bool State input) (v : Attr k State) : Bool

Whether the action of the step from a configuration has the attribute v: never, once halted.

def Cslib.Circuits.Boolean.Tableau.Invariant {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (T : ℕ) (x : List Bool) (t : ℕ) : Prop

The invariant at time t: the wire of every feature carries its value after t steps.

theorem Cslib.Circuits.Boolean.Tableau.invariant_zero {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} : Invariant tm T x 0

The first block holds the initial configuration.

Values of references

def Cslib.Circuits.Boolean.Tableau.termSem {k : ℕ} {State : Type} (T : ℕ) (x : List Bool) (cfg : Turing.Cfg k Bool State x) (c : ℕ) : ScanQ k → Prop

The contribution of column c to a scanned quantity.

def Cslib.Circuits.Boolean.Tableau.readSem {k : ℕ} {State : Type} (x : List Bool) (cfg : Turing.Cfg k Bool State x) : ScanQ k → Prop

The symbol read by a head of a configuration.

noncomputable def Cslib.Circuits.Boolean.Tableau.termVal {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (T : ℕ) (x : List Bool) (t c : ℕ) (p : Ref k State × Ref k State) : Bool

The value of a term of a feature, from block t and column c: both of its wires are true.

The scan

Situations and attributes

The gadgets of the features

The step equations of the features

theorem Cslib.Circuits.Boolean.Tableau.invariant_succ {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} {t : ℕ} (hinv : Invariant tm T x t) (hn : x.length < 2 * T) (htT : t + 1 ≤ T) : Invariant tm T x (t + 1)

One step of the simulation: the invariant passes from block t to block t + 1.

theorem Cslib.Circuits.Boolean.Tableau.invariant_le {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} (hn : x.length < 2 * T) (t : ℕ) : t ≤ T → Invariant tm T x t

The tableau computes the run: on an input of length n < 2 T, the wire of each feature at time t ≤ T carries the value of that feature after t steps.

theorem Cslib.Circuits.Boolean.Tableau.evalOutput_gates {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} (hn : x.length < 2 * T) : evalOutput x (gates tm x.length T) (outWire k State x.length T) = decide (Turing.OutView.ofList (Turing.MultiTapeTM.runFrom (tm.initCfg x) T).output = Turing.OutView.one true)

The output wire of the tableau carries the answer: on an input of length n < 2 T, it is true exactly when the output written after T steps is [true].

theorem Cslib.Circuits.Boolean.Tableau.eval_circuit {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {n T : ℕ} (hn : n < 2 * T) (y : BitString n) : (circuit tm n T).eval interpretation y 0 = decide (Turing.OutView.ofList (Turing.MultiTapeTM.runFrom (tm.initCfg (List.ofFn y)) T).output = Turing.OutView.one true)

The tableau circuit outputs the answer: on inputs y of length n < 2 T, it outputs whether tm, started on y, has written exactly [true] after T steps.