The gates of the uniform tableau within linear work space

The gate with number g of the tableau of a multi-tape machine for T steps on inputs of length n (Cslib.Circuits.Boolean.Tableau.gateCode) is computable within work space linear in the binary lengths of n, T and g (Cslib.Circuits.Boolean.Tableau.gateCode_inSpace): its position is found by divisions with remainder, its operation and its references by tables of constant size, and its wires by additions and multiplications. This is the uniformity of the tableau, used to write the circuit down in logarithmic space.

Main results

• Cslib.Circuits.Boolean.Tableau.gateCode_inSpace: the gate with a given number, within a budget covering the binary lengths of n, T and g.

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.7

The layout in normal form

The gates within a budget

theorem Cslib.Circuits.Boolean.Tableau.gfStart_inSpace {k : ℕ} {State : Type} [Fintype State] {α : Type} {encIn : α ↪ List Bool} {Bs T : α → ℕ} (hT : Turing.MultiTapeTM.ComputableInSpace T encIn Turing.MultiTapeTM.encNat Bs) (hin : Turing.MultiTapeTM.BigOLe (fun (x : α) => (encIn x).length) Bs) : Turing.MultiTapeTM.ComputableInSpace (fun (x : α) => gfStart k State (T x)) encIn Turing.MultiTapeTM.encNat Bs

theorem Cslib.Circuits.Boolean.Tableau.blockSize_inSpace {k : ℕ} {State : Type} [Fintype State] {α : Type} {encIn : α ↪ List Bool} {Bs T : α → ℕ} (hT : Turing.MultiTapeTM.ComputableInSpace T encIn Turing.MultiTapeTM.encNat Bs) (hin : Turing.MultiTapeTM.BigOLe (fun (x : α) => (encIn x).length) Bs) : Turing.MultiTapeTM.ComputableInSpace (fun (x : α) => blockSize k State (T x)) encIn Turing.MultiTapeTM.encNat Bs

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFinEnumColSel : FinEnum ColSel

@[instance_reducible]

instance Cslib.Circuits.Boolean.Tableau.instFinEnumGuard : FinEnum Guard

theorem Cslib.Circuits.Boolean.Tableau.gateCode_inSpace {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {α : Type} {encIn : α ↪ List Bool} {Bs n T : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInSpace n encIn Turing.MultiTapeTM.encNat Bs) (hT : Turing.MultiTapeTM.ComputableInSpace T encIn Turing.MultiTapeTM.encNat Bs) (hin : Turing.MultiTapeTM.BigOLe (fun (x : α) => (encIn x).length) Bs) {g : α → ℕ} (hg : Turing.MultiTapeTM.ComputableInSpace g encIn Turing.MultiTapeTM.encNat Bs) : Turing.MultiTapeTM.ComputableInSpace (fun (x : α) => gateCode tm (n x) (T x) (g x)) encIn encGate Bs

The gate with a given number, within a budget covering n, T and the number.