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.featureFn: a feature at time t, as a Boolean function of the input.
• 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)

theorem Cslib.Circuits.Boolean.MachineSimulation.abs_workTapePos_cfgAt_le {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} (t : ℕ) (x : Fin n → Bool) (i : Fin k) : |(cfgAt tm t x).workTapePos i| ≤ ↑t

A work head is within t cells of the origin after t steps.

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.

def Cslib.Circuits.Boolean.MachineSimulation.inputIs {n : ℕ} (j : ℕ) (s : Option Bool) : BooleanFunction n

The input symbol at position j is s, as a Boolean function of the input.

theorem Cslib.Circuits.Boolean.MachineSimulation.featureFn_eq_true {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 = true ↔ Turing.MultiTapeTM.Feature.Holds (cfgAt tm t x) φ

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) φ

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.card_basicFeatures_le {k : ℕ} {State : Type} [DecidableEq State] [Fintype State] (n T : ℕ) : (basicFeatures n T).card ≤ featureCount n T k State

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

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

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

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

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

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

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

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

One step

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_inputIs {n : ℕ} (j : ℕ) (b : Option Bool) : Synthesis interpretation (inputs n) {inputIs j b} 1

An input symbol, or a constant, costs at most one gate.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_read {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (ht : t ≤ T) (i : Fin k) (s : Option Bool) : Synthesis interpretation (inputs n ∪ basicAt tm T t) {featureFn tm t (Turing.MultiTapeTM.Feature.read i s)} ((2 * T + 1) * 2 + 1)

The symbol read by a work head, from the heads and cells in the window.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_inRead {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (s : Option Bool) : Synthesis interpretation (inputs n ∪ basicAt tm T t) {featureFn tm t (Turing.MultiTapeTM.Feature.inRead s)} ((n + 2) * 3 + 1)

The symbol read by the input head, from its position and the input bits.

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

The cost of the first phase of a step.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_reads {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) (readsAt tm t) (readsCost n k T)

Phase 1: the symbols read, from the basic features and the inputs.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_sit {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (y : Turing.MultiTapeTM.Situation k State) : Synthesis interpretation (inputs n ∪ basicAt tm T t ∪ readsAt tm t) {featureFn tm t (Turing.MultiTapeTM.Feature.sit y)} (k + 3)

The indicator of a situation, from the state and the symbols read.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_sits {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} : Synthesis interpretation (inputs n ∪ basicAt tm T t ∪ readsAt tm t) (sitsAt tm t) (Fintype.card (Turing.MultiTapeTM.Situation k State) * (k + 3))

Phase 2: every situation indicator.

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.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_next {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (ht : t ≤ T) {φ : Turing.MultiTapeTM.Feature k State} (hφ : φ ∈ basicFeatures n T) : Synthesis interpretation (stepSources tm T t) {featureFn tm (t + 1) φ} (featureCost k State)

Every basic feature of the next configuration, from the terms of its step equation.

theorem Cslib.Circuits.Boolean.MachineSimulation.synthesis_nexts {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T t : ℕ} (ht : t ≤ T) : Synthesis interpretation (stepSources tm T t) (basicAt tm T (t + 1)) (featureCount n T k State * featureCost k State)

Phase 3: all basic features of the next configuration.

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_zero {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) {n : ℕ} [DecidableEq State] [Fintype State] {T : ℕ} : Synthesis interpretation (inputs n) (basicAt tm T 0) (featureCount n T k State)

The basic features at time 0, which do not depend on the input.

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.

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

The total cost of simulating T steps on inputs of length n.

theorem Cslib.Circuits.Boolean.MachineSimulation.polynomiallyBounded_simulationCost {k : ℕ} {State : Type} [Fintype State] {T : ℕ → ℕ} (hT : PolynomiallyBounded T) : PolynomiallyBounded fun (n : ℕ) => simulationCost n (T n) k State

The simulation cost is polynomially bounded when the number of steps is.

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.