Circuits simulating multi-tape machines

The run of a multi-tape machine over Bool on inputs of length n is simulated by a circuit, time step by time step. At each step t the circuit holds the basic features (Turing.MultiTapeTM.Feature) of the configuration: the control state, the input head, the work heads and the work cells within the window |z| ≤ T, and the view of the output. From them it derives the symbols read and the situation of the step, and from the terms of the step equations (Turing.MultiTapeTM.Feature.stepTerms) each basic feature at time t + 1 with a constant number of gates. Running for T steps takes O(T · (n + T)) gates Sipser, Theorem 9.30.

The language of the inputs on which the machine has written [true] after T n steps is therefore in P/poly whenever T is polynomially bounded (acceptedWithin_mem_PPoly); this is the core of P ⊆ P/poly Arora and Barak, Theorem 6.6.

Main definitions

• Cslib.Circuits.Boolean.MachineSimulation.cfgAt, Cslib.Circuits.Boolean.MachineSimulation.featureFn: the configuration after t steps and a feature at time t as a Boolean function of the input.
• Cslib.Circuits.Boolean.MachineSimulation.basicFeatures, Cslib.Circuits.Boolean.MachineSimulation.basicAt, Cslib.Circuits.Boolean.MachineSimulation.readsAt, Cslib.Circuits.Boolean.MachineSimulation.sitsAt, Cslib.Circuits.Boolean.MachineSimulation.stepSources: the feature sets tracked across one step of the simulation.
• Cslib.Circuits.Boolean.MachineSimulation.featureCount, Cslib.Circuits.Boolean.MachineSimulation.readsCost, Cslib.Circuits.Boolean.MachineSimulation.featureCost, Cslib.Circuits.Boolean.MachineSimulation.stepCost: gate budgets for each phase and step of the simulation.
• Cslib.Circuits.Boolean.MachineSimulation.acceptedWithin: the inputs on which the output after T n steps is [true].

Main results

• Cslib.Circuits.Boolean.MachineSimulation.synthesis_step: one step, from the basic features at time t to those at time t + 1.
• Cslib.Circuits.Boolean.MachineSimulation.synthesis_basic: the basic features at every time t ≤ T, from the inputs.
• Cslib.Circuits.Boolean.MachineSimulation.acceptedWithin_mem_PPoly.

References

• M. Sipser, Introduction to the Theory of Computation, Section 9.3
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.cfgAt {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} (t : ℕ) (x : Fin n → Bool) : Turing.Cfg k Bool State (List.ofFn x)

The configuration of tm after t steps on the input x.

theorem Cslib.Circuits.Boolean.MachineSimulation.cfgAt_succ {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} (t : ℕ) (x : Fin n → Bool) : cfgAt tm (t + 1) x = Turing.MultiTapeTM.step (cfgAt tm t x)

The configuration at step t + 1 is obtained by applying tm.step to the configuration at step t.

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.featureFn {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] (t : ℕ) (φ : Turing.MultiTapeTM.Feature k State) : BooleanFunction n

A feature of the configuration after t steps, as a Boolean function of the input.

theorem Cslib.Circuits.Boolean.MachineSimulation.featureFn_eq_false {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] {t : ℕ} {φ : Turing.MultiTapeTM.Feature k State} {x : Fin n → Bool} : featureFn tm t φ x = false ↔ ¬Turing.MultiTapeTM.Feature.Holds (cfgAt tm t x) φ

featureFn tm t φ x is false iff the feature φ does not hold at step t on input x.

Feature sets

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.basicFeatures {k : ℕ} {State : Type} [DecidableEq State] [Fintype State] (n T : ℕ) : Finset (Turing.MultiTapeTM.Feature k State)

The basic features within the window |z| ≤ T, for inputs of length n (Turing.MultiTapeTM.Feature.basic).

def Cslib.Circuits.Boolean.MachineSimulation.featureCount (n T k : ℕ) (State : Type) [Fintype State] : ℕ

A bound on the number of basic features.

theorem Cslib.Circuits.Boolean.MachineSimulation.state_mem_basicFeatures {k : ℕ} {State : Type} {n : ℕ} [DecidableEq State] [Fintype State] {T : ℕ} (q : Option State) : Turing.MultiTapeTM.Feature.state q ∈ basicFeatures n T

Every control-state feature belongs to basicFeatures n T.

theorem Cslib.Circuits.Boolean.MachineSimulation.inPos_mem_basicFeatures {k : ℕ} {State : Type} {n : ℕ} [DecidableEq State] [Fintype State] {T j : ℕ} (hj : j < n + 2) : Turing.MultiTapeTM.Feature.inPos j ∈ basicFeatures n T

Every input-head position feature for j < n + 2 belongs to basicFeatures n T.

theorem Cslib.Circuits.Boolean.MachineSimulation.head_mem_basicFeatures {k : ℕ} {State : Type} {n : ℕ} [DecidableEq State] [Fintype State] {T : ℕ} (i : Fin k) {z : ℤ} (hz : |z| ≤ ↑T) : Turing.MultiTapeTM.Feature.head i z ∈ basicFeatures n T

Every work-head position feature within the window |z| ≤ T belongs to basicFeatures n T.

theorem Cslib.Circuits.Boolean.MachineSimulation.cell_mem_basicFeatures {k : ℕ} {State : Type} {n : ℕ} [DecidableEq State] [Fintype State] {T : ℕ} (i : Fin k) {z : ℤ} (hz : |z| ≤ ↑T) (s : Option Bool) : Turing.MultiTapeTM.Feature.cell i z s ∈ basicFeatures n T

Every work-cell symbol feature within the window |z| ≤ T belongs to basicFeatures n T.

theorem Cslib.Circuits.Boolean.MachineSimulation.out_mem_basicFeatures {k : ℕ} {State : Type} {n : ℕ} [DecidableEq State] [Fintype State] {T : ℕ} (o : Turing.OutView) : Turing.MultiTapeTM.Feature.out o ∈ basicFeatures n T

Every output-view feature belongs to basicFeatures n T.

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.basicAt {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] (T t : ℕ) : Set (BooleanFunction n)

The basic features at time t, as Boolean functions of the input.

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.readsAt {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] (t : ℕ) : Set (BooleanFunction n)

The symbols read at time t, as Boolean functions of the input.

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.sitsAt {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] (t : ℕ) : Set (BooleanFunction n)

The situations at time t, as Boolean functions of the input.

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.stepSources {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] (T t : ℕ) : Set (BooleanFunction n)

What is available for the third phase of a step: the inputs, the basic features, the symbols read and the situations.

theorem Cslib.Circuits.Boolean.MachineSimulation.featureFn_mem_basicAt {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} {φ : Turing.MultiTapeTM.Feature k State} (h : φ ∈ basicFeatures n T) : featureFn tm t φ ∈ basicAt tm T t

The Boolean function of any basic feature φ ∈ basicFeatures n T at time t belongs to basicAt tm T t.

theorem Cslib.Circuits.Boolean.MachineSimulation.featureFn_mem_stepSources {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} {φ : Turing.MultiTapeTM.Feature k State} (h : φ ∈ basicFeatures n T) : featureFn tm t φ ∈ stepSources tm T t

The Boolean function of any basic feature φ ∈ basicFeatures n T at time t belongs to stepSources tm T t.

theorem Cslib.Circuits.Boolean.MachineSimulation.sit_mem_stepSources {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (y : Turing.MultiTapeTM.Situation k State) : featureFn tm t (Turing.MultiTapeTM.Feature.sit y) ∈ stepSources tm T t

Every situation indicator at time t belongs to stepSources tm T t.

One step

def Cslib.Circuits.Boolean.MachineSimulation.readsCost (n k T : ℕ) : ℕ

The cost of the first phase of a step.

Phase 3: the next configuration

def Cslib.Circuits.Boolean.MachineSimulation.featureCost (k : ℕ) (State : Type) [Fintype State] : ℕ

The budget for one basic feature of the next configuration: its step equation has at most 4 |Situation| + 2 terms (Turing.MultiTapeTM.Feature.length_stepTerms_le), each of at most three literals.

def Cslib.Circuits.Boolean.MachineSimulation.stepCost (n T k : ℕ) (State : Type) [Fintype State] : ℕ

The cost of one step of the simulation.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_step {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (ht : t ≤ T) : Synthesis interpretation (inputs n ∪ basicAt tm T t) (basicAt tm T (t + 1)) (stepCost n T k State)

One step of the simulation: the basic features at time t + 1, from those at time t.

The whole run

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_basic {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T : ℕ} (t : ℕ) : t ≤ T → Synthesis interpretation (inputs n) (basicAt tm T t) (featureCount n T k State + t * stepCost n T k State)

The simulation: the basic features at every time t ≤ T, from the inputs.

noncomputable def Cslib.Circuits.Boolean.MachineSimulation.acceptedWithin {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) [DecidableEq State] (T : ℕ → ℕ) : Language Bool

The inputs on which tm has written [true] after T n steps, on inputs of length n.

theorem Cslib.Circuits.Boolean.MachineSimulation.mem_acceptedWithin_iff {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) [DecidableEq State] (T : ℕ → ℕ) (w : List Bool) : w ∈ acceptedWithin tm T ↔ Turing.OutView.ofList (Turing.MultiTapeTM.runFrom (tm.initCfg w) (T w.length)).output = Turing.OutView.one true

An input is accepted within T steps when the machine has written [true] by then.

theorem Cslib.Circuits.Boolean.MachineSimulation.acceptedWithin_mem_PPoly {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) [DecidableEq State] [Finite State] {T : ℕ → ℕ} (hT : PolynomiallyBounded T) : acceptedWithin tm T ∈ PPoly

Machines with polynomial running time have polynomial circuits. The inputs on which a machine has written [true] within a polynomially bounded number of steps form a language in P/poly.