Boolean features of configurations

A configuration of a multi-tape machine over Bool is described by finitely-valued features: the control state, the position of the input head, the position of each work head, the contents of each work cell, and what has been written on the output (Turing.OutView). Three more features say what a step depends on: the symbol under each work head, the symbol under the input head, and the situation (Turing.MultiTapeTM.Situation) — the state together with all the symbols read.

Each feature of the next configuration is a Boolean combination of features of the current one: a halted configuration does not change, and otherwise exactly one situation holds, which determines the action. The step equations (holds_step_state_iff, …) state this kind by kind. For inputs of length n and work heads in the window |z| ≤ T, the basic features (Feature.basic: state, input head, work heads and cells in the window, output view) come in groups of which exactly one feature holds, and the step equation of each basic feature is a disjunction of terms, conjunctions of basic features, their negations and situations (Feature.stepTerms, holds_step_iff_exists_stepTerms). Reductions that describe runs by Boolean variables, such as the Cook–Levin tableau, and circuits simulating machines are built on these equations.

Main definitions

• Turing.MultiTapeTM.Situation, Turing.Cfg.situation.
• Turing.MultiTapeTM.Feature, Turing.MultiTapeTM.Feature.Holds.
• Turing.MultiTapeTM.Feature.groups, Turing.MultiTapeTM.Feature.basic: the basic features.
• Turing.MultiTapeTM.Feature.stepTerms: the terms of the step equation of a basic feature.

Main results

• Turing.MultiTapeTM.Feature.holds_read_iff, holds_inRead_iff, holds_sit_iff: the symbols read and the situation, from the basic features.
• Turing.MultiTapeTM.Feature.holds_step_state_iff, holds_step_inPos_iff, holds_step_head_iff, holds_step_cell_iff, holds_step_out_iff: the step equations.
• Turing.MultiTapeTM.Feature.exists_holds_of_mem_groups, eq_of_holds_of_mem_groups: exactly one basic feature of each group holds.
• Turing.MultiTapeTM.Feature.holds_step_iff_exists_stepTerms: the step equations as disjunctions of terms.

theorem Turing.mem_window_iff_abs_le {T : ℕ} {z : ℤ} : z ∈ window T ↔ |z| ≤ ↑T

A cell is in the window -T, …, T exactly when its absolute value is at most T.

def Turing.windowList (T : ℕ) : List ℤ

The cells -T, …, T of the window, from left to right.

@[simp]

theorem Turing.mem_windowList {T : ℕ} {z : ℤ} : z ∈ windowList T ↔ |z| ≤ ↑T

@[simp]

theorem Turing.length_windowList (T : ℕ) : (windowList T).length = 2 * T + 1

theorem Turing.nodup_windowList (T : ℕ) : (windowList T).Nodup

@[simp]

theorem Turing.toFinset_windowList (T : ℕ) : (windowList T).toFinset = window T

@[reducible, inline]

abbrev Turing.MultiTapeTM.Situation (k : ℕ) (State : Type) : Type

The situation of a step: the state, the symbol under the input head, and the symbols under the work heads. The transition function maps a situation to an action.

noncomputable def Turing.MultiTapeTM.actionOf {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (y : Situation k State) : Action k Bool State

The action that tm takes in situation y.

inductive Turing.MultiTapeTM.Feature (k : ℕ) (State : Type) : Type

The features describing configurations of a machine over Bool.

• state {k : ℕ} {State : Type} (q : Option State) : Feature k State

  The control state is q (none once halted).

• inPos {k : ℕ} {State : Type} (j : ℕ) : Feature k State

  The input head is at position j.

• head {k : ℕ} {State : Type} (i : Fin k) (z : ℤ) : Feature k State

  The head of work tape i is at cell z.

• cell {k : ℕ} {State : Type} (i : Fin k) (z : ℤ) (s : Option Bool) : Feature k State

  Cell z of work tape i holds s.

• out {k : ℕ} {State : Type} (o : OutView) : Feature k State

  The output written so far has view o.

• read {k : ℕ} {State : Type} (i : Fin k) (s : Option Bool) : Feature k State

  The head of work tape i reads s.

• inRead {k : ℕ} {State : Type} (s : Option Bool) : Feature k State

  The input head reads s.

• sit {k : ℕ} {State : Type} (y : Situation k State) : Feature k State

  The configuration is running in situation y.

def Turing.MultiTapeTM.instDecidableEqFeature.decEq {k✝ : ℕ} {State✝ : Type} [DecidableEq State✝] (x✝ x✝¹ : Feature k✝ State✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqFeature {k✝ : ℕ} {State✝ : Type} [DecidableEq State✝] : DecidableEq (Feature k✝ State✝)

def Turing.Cfg.situation {k : ℕ} {State : Type} {input : List Bool} (cfg : Cfg k Bool State input) (q : State) : MultiTapeTM.Situation k State

The situation of a configuration running in state q.

def Turing.MultiTapeTM.Feature.Holds {k : ℕ} {State : Type} {input : List Bool} (cfg : Cfg k Bool State input) : Feature k State → Prop

Whether a feature holds of a configuration.

@[instance_reducible]

instance Turing.MultiTapeTM.Feature.instDecidableHoldsOfDecidableEq {k : ℕ} {State : Type} {input : List Bool} [DecidableEq State] (cfg : Cfg k Bool State input) (φ : Feature k State) : Decidable (Holds cfg φ)

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_state {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {q : Option State} : Holds cfg (state q) ↔ cfg.state = q

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_inPos {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {j : ℕ} : Holds cfg (inPos j) ↔ ↑cfg.inputPos = j

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_head {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {i : Fin k} {z : ℤ} : Holds cfg (head i z) ↔ cfg.workTapePos i = z

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_cell {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {i : Fin k} {z : ℤ} {s : Option Bool} : Holds cfg (cell i z s) ↔ cfg.workTapes i z = s

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_out {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {o : OutView} : Holds cfg (out o) ↔ OutView.ofList cfg.output = o

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_read {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {i : Fin k} {s : Option Bool} : Holds cfg (read i s) ↔ cfg.workTapeSymbols i = s

@[simp]

theorem Turing.MultiTapeTM.Feature.holds_inRead {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {s : Option Bool} : Holds cfg (inRead s) ↔ cfg.inputSymbol = s

The symbols read and the situation

theorem Turing.MultiTapeTM.Feature.holds_read_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {i : Fin k} {T : ℕ} (hb : |cfg.workTapePos i| ≤ ↑T) (s : Option Bool) : Holds cfg (read i s) ↔ ∃ z ∈ window T, Holds cfg (head i z) ∧ Holds cfg (cell i z s)

A work head reads the symbol in the cell it is on, for a head within the window.

theorem Turing.MultiTapeTM.Feature.holds_inRead_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (s : Option Bool) : Holds cfg (inRead s) ↔ ∃ j ∈ Finset.range (input.length + 2), Holds cfg (inPos j) ∧ inputAt input j = s

The input head reads the input symbol at its position.

theorem Turing.MultiTapeTM.Feature.holds_sit_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (y : Situation k State) : Holds cfg (sit y) ↔ Holds cfg (state (some y.1)) ∧ Holds cfg (inRead y.2.1) ∧ ∀ (i : Fin k), Holds cfg (read i (y.2.2 i))

The situation holds when the state and the symbols read are those of the situation.

theorem Turing.MultiTapeTM.Feature.holds_sit_iff_eq {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {q : State} (hq : cfg.state = some q) (y : Situation k State) : Holds cfg (sit y) ↔ y = cfg.situation q

In a configuration running in state q, exactly its own situation holds.

theorem Turing.MultiTapeTM.Feature.not_holds_sit {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (h : cfg.state = none) (y : Situation k State) : ¬Holds cfg (sit y)

In a halted configuration, no situation holds.

The step equations

theorem Turing.MultiTapeTM.Feature.holds_step_of_halted {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (tm : MultiTapeTM k Bool State) (h : cfg.state = none) (φ : Feature k State) : Holds (step cfg) φ ↔ Holds cfg φ

A halted configuration does not change.

theorem Turing.MultiTapeTM.Feature.step_eq_apply {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (tm : MultiTapeTM k Bool State) {q : State} (hq : cfg.state = some q) : step cfg = (tm.actionOf (cfg.situation q)).apply cfg

theorem Turing.MultiTapeTM.Feature.holds_step_state_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (tm : MultiTapeTM k Bool State) [Fintype State] [DecidableEq State] (q' : Option State) : Holds (step cfg) (state q') ↔ Holds cfg (state none) ∧ q' = none ∨ ∃ y ∈ {y : Situation k State | (tm.actionOf y).state = q'}, Holds cfg (sit y)

The step equation for the state.

theorem Turing.MultiTapeTM.Feature.holds_step_inPos_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (tm : MultiTapeTM k Bool State) [Fintype State] (j : ℕ) : Holds (step cfg) (inPos j) ↔ Holds cfg (state none) ∧ Holds cfg (inPos j) ∨ ∃ y ∈ {y ∈ Finset.univ ×ˢ {j - 1, j, j + 1} | y.2 < input.length + 2 ∧ moveInputPosNat input.length y.2 (tm.actionOf y.1).inputTape = j}, Holds cfg (sit y.1) ∧ Holds cfg (inPos y.2)

The step equation for the input head. The input head moves at most one cell, so it comes from one of the positions j - 1, j, j + 1.

theorem Turing.MultiTapeTM.Feature.holds_step_head_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {i : Fin k} (tm : MultiTapeTM k Bool State) [Fintype State] {T : ℕ} (hb : |cfg.workTapePos i| ≤ ↑T) (z : ℤ) : Holds (step cfg) (head i z) ↔ Holds cfg (state none) ∧ Holds cfg (head i z) ∨ ∃ y ∈ {y : Situation k State | |z - ↑((tm.actionOf y).workTapes i).2| ≤ ↑T}, Holds cfg (sit y) ∧ Holds cfg (head i (z - ↑((tm.actionOf y).workTapes i).2))

The step equation for a work head within the window |z| ≤ T, for a head that was within the window.

theorem Turing.MultiTapeTM.Feature.holds_step_cell_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {i : Fin k} (tm : MultiTapeTM k Bool State) [Fintype State] (z : ℤ) (s : Option Bool) : Holds (step cfg) (cell i z s) ↔ Holds cfg (cell i z s) ∧ (Holds cfg (state none) ∨ ¬Holds cfg (head i z)) ∨ ∃ y ∈ {y ∈ Finset.univ ×ˢ Finset.univ | ((tm.actionOf y.1).workTapes i).1.getD y.2 = s}, Holds cfg (sit y.1) ∧ Holds cfg (head i z) ∧ Holds cfg (cell i z y.2)

The step equation for a work cell.

theorem Turing.MultiTapeTM.Feature.holds_step_out_iff {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} (tm : MultiTapeTM k Bool State) [Fintype State] (o : OutView) : Holds (step cfg) (out o) ↔ Holds cfg (state none) ∧ Holds cfg (out o) ∨ ∃ y ∈ {y ∈ Finset.univ ×ˢ Finset.univ | y.2.push (tm.actionOf y.1).output = o}, Holds cfg (sit y.1) ∧ Holds cfg (out y.2)

The step equation for the output.

Basic features and step terms

def Turing.MultiTapeTM.Feature.symbols : List (Option Bool)

The three symbols a cell can hold: blank, false and true.

@[simp]

theorem Turing.MultiTapeTM.Feature.mem_symbols (s : Option Bool) : s ∈ symbols

@[simp]

theorem Turing.MultiTapeTM.Feature.length_symbols : symbols.length = 3

@[reducible, inline]

abbrev Turing.MultiTapeTM.Feature.Term (k : ℕ) (State : Type) : Type

A term: a conjunction of features, written (φ, true), and of negated features, written (φ, false).

def Turing.MultiTapeTM.Feature.Term.Holds {k : ℕ} {State : Type} {input : List Bool} (cfg : Cfg k Bool State input) (c : Term k State) : Prop

A term holds of a configuration when each of its features holds or fails as it says.

@[simp]

theorem Turing.MultiTapeTM.Feature.Term.holds_nil {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} : Holds cfg []

@[simp]

theorem Turing.MultiTapeTM.Feature.Term.holds_cons {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} {φ : Feature k State} {b : Bool} {c : Term k State} : Holds cfg ((φ, b) :: c) ↔ (Feature.Holds cfg φ ↔ b = true) ∧ Holds cfg c

noncomputable def Turing.MultiTapeTM.Feature.states {State : Type} [Fintype State] : List (Option State)

Every control state, none included, in a fixed order.

@[simp]

theorem Turing.MultiTapeTM.Feature.mem_states {State : Type} [Fintype State] (q : Option State) : q ∈ states

@[simp]

theorem Turing.MultiTapeTM.Feature.length_states {State : Type} [Fintype State] : states.length = Fintype.card State + 1

noncomputable def Turing.MultiTapeTM.Feature.situations {k : ℕ} {State : Type} [Fintype State] : List (Situation k State)

Every situation, in a fixed order.

@[simp]

theorem Turing.MultiTapeTM.Feature.mem_situations {k : ℕ} {State : Type} [Fintype State] (y : Situation k State) : y ∈ situations

@[simp]

theorem Turing.MultiTapeTM.Feature.length_situations {k : ℕ} {State : Type} [Fintype State] : situations.length = Fintype.card (Situation k State)

noncomputable def Turing.MultiTapeTM.Feature.groups {k : ℕ} {State : Type} [Fintype State] (n T : ℕ) : List (List (Feature k State))

The basic features for inputs of length n within the window |z| ≤ T, in groups: the states, the positions of the input head, the positions of each work head in the window, the contents of each work cell in the window, and the views of the output. In a configuration on an input of length n whose work heads are in the window, exactly one feature of each group holds (exists_holds_of_mem_groups, eq_of_holds_of_mem_groups). The window |z| ≤ T contains every cell that a head can reach within T steps.

noncomputable def Turing.MultiTapeTM.Feature.basic {k : ℕ} {State : Type} [Fintype State] (n T : ℕ) : List (Feature k State)

The basic features for inputs of length n within the window |z| ≤ T: the features of all groups.

theorem Turing.MultiTapeTM.Feature.mem_groups {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} {g : List (Feature k State)} : g ∈ groups n T ↔ g = List.map state states ∨ g = List.map inPos (List.range (n + 2)) ∨ (∃ (i : Fin k), g = List.map (head i) (windowList T)) ∨ (∃ (i : Fin k) (z : ℤ), |z| ≤ ↑T ∧ g = List.map (cell i z) symbols) ∨ g = List.map out OutView.all

theorem Turing.MultiTapeTM.Feature.exists_holds_of_mem_groups {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} [Fintype State] {n T : ℕ} (hn : input.length = n) (hb : ∀ (i : Fin k), |cfg.workTapePos i| ≤ ↑T) {g : List (Feature k State)} (hg : g ∈ groups n T) : ∃ φ ∈ g, Holds cfg φ

In a configuration whose work heads are in the window, some feature of each group holds.

theorem Turing.MultiTapeTM.Feature.eq_of_holds_of_mem_groups {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} [Fintype State] {n T : ℕ} {g : List (Feature k State)} (hg : g ∈ groups n T) {φ ψ : Feature k State} (hφ : φ ∈ g) (hψ : ψ ∈ g) (h₁ : Holds cfg φ) (h₂ : Holds cfg ψ) : φ = ψ

At most one feature of each group holds.

theorem Turing.MultiTapeTM.Feature.mem_basic_iff_exists_mem_groups {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} {φ : Feature k State} : φ ∈ basic n T ↔ ∃ g ∈ groups n T, φ ∈ g

theorem Turing.MultiTapeTM.Feature.mem_basic {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} {φ : Feature k State} : φ ∈ basic n T ↔ (∃ (q : Option State), φ = state q) ∨ (∃ j < n + 2, φ = inPos j) ∨ (∃ (i : Fin k) (z : ℤ), |z| ≤ ↑T ∧ φ = head i z) ∨ (∃ (i : Fin k) (z : ℤ) (s : Option Bool), |z| ≤ ↑T ∧ φ = cell i z s) ∨ ∃ (o : OutView), φ = out o

theorem Turing.MultiTapeTM.Feature.state_mem_basic {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} (q : Option State) : state q ∈ basic n T

theorem Turing.MultiTapeTM.Feature.inPos_mem_basic {k : ℕ} {State : Type} [Fintype State] {n T j : ℕ} (hj : j < n + 2) : inPos j ∈ basic n T

theorem Turing.MultiTapeTM.Feature.head_mem_basic {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} (i : Fin k) {z : ℤ} (hz : |z| ≤ ↑T) : head i z ∈ basic n T

theorem Turing.MultiTapeTM.Feature.cell_mem_basic {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} (i : Fin k) {z : ℤ} (hz : |z| ≤ ↑T) (s : Option Bool) : cell i z s ∈ basic n T

theorem Turing.MultiTapeTM.Feature.out_mem_basic {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} (o : OutView) : out o ∈ basic n T

theorem Turing.MultiTapeTM.Feature.length_basic {k : ℕ} {State : Type} [Fintype State] (n T : ℕ) : (basic n T).length = Fintype.card State + 1 + (n + 2) + k * (2 * T + 1) + k * (2 * T + 1) * 3 + 4

The number of basic features.

noncomputable def Turing.MultiTapeTM.Feature.stepTerms {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : MultiTapeTM k Bool State) (n T : ℕ) : Feature k State → List (Term k State)

The terms of the step equation of a basic feature, for inputs of length n and the window |z| ≤ T: the feature holds after a step exactly when one of its terms holds before it (holds_step_iff_exists_stepTerms). Every term is made of basic features, their negations, and situations (mem_basic_of_mem_stepTerms).

theorem Turing.MultiTapeTM.Feature.holds_step_iff_exists_stepTerms {k : ℕ} {State : Type} {input : List Bool} {cfg : Cfg k Bool State input} [Fintype State] {n T : ℕ} [DecidableEq State] (tm : MultiTapeTM k Bool State) (hn : input.length = n) (hb : ∀ (i : Fin k), |cfg.workTapePos i| ≤ ↑T) {φ : Feature k State} (hφ : φ ∈ basic n T) : Holds (step cfg) φ ↔ ∃ c ∈ stepTerms tm n T φ, Term.Holds cfg c

The step equation. Within the window, a basic feature holds after a step exactly when one of its terms holds before it.

theorem Turing.MultiTapeTM.Feature.length_stepTerms_le {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} [DecidableEq State] (tm : MultiTapeTM k Bool State) (φ : Feature k State) : (stepTerms tm n T φ).length ≤ 4 * Fintype.card (Situation k State) + 2

A feature has at most 4 |Situation| + 2 terms in its step equation.

theorem Turing.MultiTapeTM.Feature.length_le_three_of_mem_stepTerms {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} [DecidableEq State] (tm : MultiTapeTM k Bool State) {φ : Feature k State} {c : Term k State} (hc : c ∈ stepTerms tm n T φ) : List.length c ≤ 3

Every term of a step equation has at most three literals.

theorem Turing.MultiTapeTM.Feature.mem_basic_of_mem_stepTerms {k : ℕ} {State : Type} [Fintype State] {n T : ℕ} [DecidableEq State] (tm : MultiTapeTM k Bool State) {φ : Feature k State} (hφ : φ ∈ basic n T) {c : Term k State} (hc : c ∈ stepTerms tm n T φ) {l : Std.Sat.Literal (Feature k State)} (hl : l ∈ c) : l.1 ∈ basic n T ∨ ∃ (y : Situation k State), l = (sit y, true)

The terms of a basic feature are made of basic features, their negations, and situations.