The uniform tableau circuit of a multi-tape machine

The run of a multi-tape machine over Bool for T steps on inputs of length n is simulated by a De Morgan circuit written down gate by gate (Cslib.Circuits.Boolean.Tableau.gates), in the format of Cslib.Circuits.Circuit.code. The circuit is uniform: the operation and the wires of gate g are given by a table of constant size, indexed by g modulo the size of a block, and by a few additions and multiplications of g, n and T (Cslib.Circuits.Boolean.Tableau.gateCode). This is the circuit of Ladner's proof that the circuit value problem is P-complete under logarithmic-space reductions [Lad75], Arora and Barak, Section 6.7, Papadimitriou, Theorem 8.1.

The circuit follows the configuration in the model of Turing.MultiTapeTM, without conversion to a single-tape or oblivious machine. Work-tape cells -T, …, T and input positions 0, …, n + 1 share the 2 T + 1 columns c: column c holds the input head at position c, and the work heads and work cells at c - T. After two constant gates (false at wire n, true at wire n + 1), the circuit has one block of gates for each time t ≤ T. Block 0 consists of constants describing the initial configuration. Block t + 1 reads block t and has four regions (Complexity/Computability/Circuit/Boolean/Tableau/Layout.lean):

• the scan, column by column: the symbols under the heads, as disjunctions accumulated across the columns (Cslib.Circuits.Boolean.Tableau.ScanLoc), and the negated head positions;
• the global gates: each situation (Turing.MultiTapeTM.Situation) as a conjunction of the state and the symbols read, and each attribute of the action (Cslib.Circuits.Boolean.Tableau.Attr) as a disjunction over the situations with that attribute;
• the global features: the state and the view of the output (Turing.OutView);
• the column features: the input head, the work heads and the work cells of each column.

Every feature at time t + 1 is a disjunction of at most eight conjunctions of two wires (Cslib.Circuits.Boolean.Tableau.gfTerms, Cslib.Circuits.Boolean.Tableau.colTerms), computed by sixteen gates. A gate refers to wires symbolically (Cslib.Circuits.Boolean.Tableau.Ref), relative to its block and column, and a reference is resolved to a wire number by arithmetic (Cslib.Circuits.Boolean.Tableau.Ref.resolve).

The circuit is well formed (Cslib.Circuits.Boolean.Tableau.isCodeFrom_gates): every gate reads only inputs and earlier gates. Its correctness is proved in Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean.

Main definitions

• Cslib.Circuits.Boolean.Tableau.table: the gate at each position of a block.
• Cslib.Circuits.Boolean.Tableau.gateAt, Cslib.Circuits.Boolean.Tableau.gateCode: the gate at a block position and the gate with a given number.
• Cslib.Circuits.Boolean.Tableau.gates, Cslib.Circuits.Boolean.Tableau.outWire: the gate list and the output wire.
• Cslib.Circuits.Boolean.Tableau.circuit: the tableau as a De Morgan circuit.

Main results

• Cslib.Circuits.Boolean.Tableau.gateCode_wire: the gate at a position's wire is the gate of its position.
• Cslib.Circuits.Boolean.Tableau.isCodeFrom_gates: the gate list is the code of a program.
• Cslib.Circuits.Boolean.Tableau.code_circuit: the code of the circuit is the gate list with the output wire.

References

• R. E. Ladner, The circuit value problem is log space complete for P
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Sections 6.1 and 6.7
• C. H. Papadimitriou, Computational Complexity, Theorem 8.1

The gates

def Cslib.Circuits.Boolean.Tableau.Attr.test {k : ℕ} {State : Type} [DecidableEq State] (a : Turing.Action k Bool State) : Attr k State → Bool

Whether an action has an attribute.

noncomputable def Cslib.Circuits.Boolean.Tableau.sitOf {k : ℕ} {State : Type} [Fintype State] (j : Fin (numSit k State)) : Turing.MultiTapeTM.Situation k State

The situation with number j.

def Cslib.Circuits.Boolean.Tableau.scanTerm {k : ℕ} {State : Type} [Fintype State] : ScanQ k → Ref k State × Ref k State

The two wires of the contribution of a column to a scanned quantity.

def Cslib.Circuits.Boolean.Tableau.gfTerms {k : ℕ} {State : Type} [Fintype State] : GFeat State → List (Ref k State × Ref k State)

The terms of a global feature at the next time: the feature holds after the step exactly when both wires of one term are true.

def Cslib.Circuits.Boolean.Tableau.colTerms {k : ℕ} {State : Type} [Fintype State] : ColFeat k → List (Ref k State × Ref k State)

The terms of a column feature at the next time.

noncomputable def Cslib.Circuits.Boolean.Tableau.table {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) : Loc k State → Op × Ref k State × Ref k State

The gate at each position of a block after the first, with symbolic references to its wires.

def Cslib.Circuits.Boolean.Tableau.gfInit {k : ℕ} {State : Type} [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) : GFeat State → Bool

The value of a global feature in the initial configuration.

def Cslib.Circuits.Boolean.Tableau.colInit {k : ℕ} (T c : ℕ) : ColFeat k → Bool

The value of a column feature in the initial configuration, for the column c of 2 T + 1: the input head on the first input cell, the work heads on cell 0, the work cells blank.

def Cslib.Circuits.Boolean.Tableau.initBit {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (T c : ℕ) : Loc k State → Bool

The constant at each position of the first block: the initial value of a feature at the last gate of its gadget, false elsewhere.

noncomputable def Cslib.Circuits.Boolean.Tableau.gateAt {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T t c : ℕ) (l : Loc k State) : Op × List ℕ

The gate at the position l of block t, in column c.

noncomputable def Cslib.Circuits.Boolean.Tableau.gateCode {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T g : ℕ) : Op × List ℕ

The gate with number g of the tableau of tm for T steps on inputs of length n: gates 0 and 1 are the constants false and true, and gate 2 + t * B + r is the gate at offset r of block t, for blocks of B gates.

noncomputable def Cslib.Circuits.Boolean.Tableau.gates {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T : ℕ) : List (Op × List ℕ)

The gate list of the tableau of tm for T steps on inputs of length n.

noncomputable def Cslib.Circuits.Boolean.Tableau.outWire (k : ℕ) (State : Type) [Fintype State] (n T : ℕ) : ℕ

The output wire of the tableau: the output has the view [true] at time T.

Gates at their wires

theorem Cslib.Circuits.Boolean.Tableau.gateCode_wire {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {n T t : ℕ} {l : Loc k State} {c : ℕ} (hl : Loc.ColOK T c l) : gateCode tm n T (wire n T t l c - n) = gateAt tm n T t c l

The gate at a wire is the gate of its position.

Well-formedness

The gate list is the code of a circuit

theorem Cslib.Circuits.Boolean.Tableau.isCodeFrom_gates {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T : ℕ) : Program.IsCodeFrom signature n 0 (gates tm n T)

The tableau is well formed: its gate list is the code of a program on n inputs.

theorem Cslib.Circuits.Boolean.Tableau.outWire_lt {k : ℕ} {State : Type} [Fintype State] (n T : ℕ) : outWire k State n T < n + numGates k State T

theorem Cslib.Circuits.Boolean.Tableau.isSome_ofCode {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T : ℕ) : (Circuit.ofCode n 1 (gates tm n T, [outWire k State n T])).isSome = true

noncomputable def Cslib.Circuits.Boolean.Tableau.circuit {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T : ℕ) : Circuit signature n 1

The tableau circuit of tm for T steps on inputs of length n.

theorem Cslib.Circuits.Boolean.Tableau.code_circuit {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (n T : ℕ) : (circuit tm n T).code = (gates tm n T, [outWire k State n T])

The code of the tableau circuit is its gate list with the output wire.