Turing machines over a universe, without a vocabulary

The semantics half of the machine bridge: what it means for a nondeterministic Turing machine, presented as relations on a universe, to accept. No vocabulary appears here – DescriptiveComplexity.Problems.Machine.Defs supplies one and reads these definitions off a structure – so that the reductions, which build machines rather than read them, can reason about runs without unfolding any RelMap.

The model

A machine is DescriptiveComplexity.TMData: the sorts (Posn, Tr), the marks (Start, Acc, Blank, Right), the binary attributes of a transition (Src, Read, Dst, Write), the initial tape Inp, and a linear order Le. Two decisions from the plan are visible in the types.

• Transitions are elements. A transition is an element τ of the universe with four binary attributes, rather than a 5-ary relation; every relation here has arity at most two, which is what keeps the defining formulas of an interpretation indexed by pairs of tags.
• Time steps and tape cells are the same sort. A configuration's head is a position, and the time bound of DescriptiveComplexity.TMData.Accepts is the number of positions – a unary bound by construction, with no arithmetic. A head at the last position moving right has no successor (DescriptiveComplexity.SuccPos fails), and the run simply stops.

The tape is a total function A → A, so the semantics is total: reading a cell never fails. Which functions count as initial tapes is DescriptiveComplexity.TMData.InitTape – the input where it is defined, blank elsewhere – stated as a relation so that no choice is needed and so that the first-order kernel of the membership proof can check it literally.

Transport

DescriptiveComplexity.TMData.Agree records that two machines over different universes correspond along an equivalence, fieldwise; DescriptiveComplexity.TMData.accepts_congr transports acceptance along it. This is all the isomorphism-invariance proof of the decision problems needs.

structure DescriptiveComplexity.Config (A : Type) : Type

A configuration: the current state, the position of the head, and the contents of the tape.

• state : A

  The current state.

• head : A

  The cell the head is on.

• tape : A → A

  The symbol in each cell.

theorem DescriptiveComplexity.Config.ext_iff {A : Type} {x y : Config A} : x = y ↔ x.state = y.state ∧ x.head = y.head ∧ x.tape = y.tape

theorem DescriptiveComplexity.Config.ext {A : Type} {x y : Config A} (state : x.state = y.state) (head : x.head = y.head) (tape : x.tape = y.tape) : x = y

structure DescriptiveComplexity.TMData (A : Type) : Type

A Turing machine presented as relations on a universe: the sorts, the marks, the attributes of the transitions, the initial tape and the order along which the head moves.

• Posn : A → Prop

  Being a position – a tape cell, and equally a time step.

• Le : A → A → Prop

  The order on positions, along which the head moves.

• Tr : A → Prop

  Being a transition.

• Start : A → Prop

  Being a start state.

• Acc : A → Prop

  Being an accepting state.

• Blank : A → Prop

  Being the blank symbol.

• Right : A → Prop

  This transition moves the head right (rather than left).

• Src : A → A → Prop

  The state a transition applies in.

• Read : A → A → Prop

  The symbol a transition reads.

• Dst : A → A → Prop

  The state a transition moves to.

• Write : A → A → Prop

  The symbol a transition writes.

• Inp : A → A → Prop

  The input: the symbol initially in a cell.

def DescriptiveComplexity.TMData.InitTape {A : Type} (M : TMData A) (p a : A) : Prop

The symbols a cell may initially hold: the input symbol where the input is defined, the blank elsewhere.

Equations

• M.InitTape p a = (M.Inp p a ∨ (∀ (b : A), ¬M.Inp p b) ∧ M.Blank a)

def DescriptiveComplexity.TMData.IsInit {A : Type} (M : TMData A) (c : Config A) : Prop

Being an initial configuration: a start state, the head on the lowest position, and an initial tape.

Equations

• M.IsInit c = (M.Start c.state ∧ DescriptiveComplexity.MinPos M.Le M.Posn c.head ∧ ∀ (p : A), M.InitTape p (c.tape p))

def DescriptiveComplexity.TMData.Step {A : Type} (M : TMData A) (c c' : Config A) : Prop

One step. Some transition applies in the current state to the symbol under the head: it writes in that cell, changes state, and moves the head to the neighbouring position in the direction it names. Cells other than the one under the head are unchanged, and a move off the end of the tape is impossible – there being no such neighbour, no step is available and the run stops.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.TMData.StepsIn {A : Type} (M : TMData A) : ℕ → Config A → Config A → Prop

Reaching one configuration from another in exactly n steps.

Equations

• M.StepsIn 0 x✝¹ x✝ = (x✝¹ = x✝)
• M.StepsIn n.succ x✝¹ x✝ = ∃ (d : DescriptiveComplexity.Config A), M.Step x✝¹ d ∧ M.StepsIn n d x✝

def DescriptiveComplexity.TMData.Accepts {A : Type} (M : TMData A) : Prop

Acceptance: some run from an initial configuration reaches an accepting state within as many steps as there are positions.

The bound is unary by construction – it counts elements of the universe – which is what makes this an NP problem rather than an NEXP one, with no arithmetic anywhere. A reduction buys itself |Tag| · nᵈ steps by choosing the dimension d of its interpretation.

The bound is strict because the positions index the time points of the run: N of them leave N - 1 steps between them, which is what makes DescriptiveComplexity.TMData.accepts_iff_exists_walk an equivalence on the nose.

Equations

• M.Accepts = ∃ (c₀ : DescriptiveComplexity.Config A) (c : DescriptiveComplexity.Config A) (n : ℕ), M.IsInit c₀ ∧ n < Nat.card { p : A // M.Posn p } ∧ M.StepsIn n c₀ c ∧ M.Acc c.state

def DescriptiveComplexity.TMData.AcceptsSpace {A : Type} (M : TMData A) : Prop

Acceptance in bounded space: some run from an initial configuration reaches an accepting state, with no bound on its length.

This is DescriptiveComplexity.TMData.Accepts with the step bound dropped, and that is all the difference between the time-bounded and the space-bounded model: the space is already bounded by construction, since the tape is indexed by the positions and a reduction of dimension d therefore buys nᵈ cells exactly as it buys nᵈ steps. What changes is that a run no longer fits inside the structure – it may visit exponentially many configurations – so acceptance is reachability in the configuration graph rather than a walk indexed by the positions, which is why the membership proof for the space-bounded problems is an SO(TC) specification rather than a Σ₁ definition.

Equations

• M.AcceptsSpace = ∃ (c₀ : DescriptiveComplexity.Config A) (c : DescriptiveComplexity.Config A), M.IsInit c₀ ∧ Relation.ReflTransGen M.Step c₀ c ∧ M.Acc c.state

theorem DescriptiveComplexity.TMData.StepsIn.trans_step {A : Type} {M : TMData A} {n : ℕ} {c d e : Config A} : M.StepsIn n c d → M.Step d e → M.StepsIn (n + 1) c e

A run extended by one more step at its end.

theorem DescriptiveComplexity.TMData.stepsIn_succ_iff {A : Type} {M : TMData A} {n : ℕ} {c e : Config A} : M.StepsIn (n + 1) c e ↔ ∃ (d : Config A), M.StepsIn n c d ∧ M.Step d e

A run decomposed at its far end: n + 1 steps are n steps and then one. DescriptiveComplexity.TMData.StepsIn recurses at the near end; inductions along the time order – the fixed-point description of a deterministic run – need this reading.

theorem DescriptiveComplexity.TMData.stepsIn_split {A : Type} {M : TMData A} {m k : ℕ} {c e : Config A} : M.StepsIn (m + k) c e → ∃ (d : Config A), M.StepsIn m c d ∧ M.StepsIn k d e

A run splits anywhere: m + k steps decompose into m and then k, through the configuration reached halfway. This is what lets two runs from the same configuration be compared at a common time.

theorem DescriptiveComplexity.TMData.StepsIn.trans {A : Type} {M : TMData A} {n m : ℕ} {c d e : Config A} : M.StepsIn n c d → M.StepsIn m d e → M.StepsIn (n + m) c e

Runs compose. Phases of a constructed machine are proved one at a time and chained with this; the step counts add, which is the form the budget obligation of a reduction takes.

def DescriptiveComplexity.TMData.WellFormed {A : Type} (M : TMData A) : Prop

Well-formedness, folded into the yes-instances in the style of DescriptiveComplexity.IsLinOrd for Knapsack: the order is linear, there is a position to start on, the input is functional, and there is exactly one blank symbol. Every conjunct is first-order, so the Σ₁ kernel can check it.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.TMData.Deterministic {A : Type} (M : TMData A) : Prop

Determinism, folded into the yes-instances of DescriptiveComplexity.DTMAccept: one start state, at most one transition applicable in a given state on a given symbol, and at most one destination and written symbol per transition. Together with well-formedness this leaves at most one step from any configuration (DescriptiveComplexity.TMData.step_functional) and at most one initial configuration (DescriptiveComplexity.TMData.isInit_unique), so the run is unique – the shape a least fixed point can compute. Every conjunct is first-order.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.TMData.initTape_functional {A : Type} {M : TMData A} (hwf : M.WellFormed) {p a b : A} (ha : M.InitTape p a) (hb : M.InitTape p b) : a = b

A well-formed initial tape is functional: a cell holds either its unique input symbol or the unique blank, and the two cases exclude each other.

theorem DescriptiveComplexity.TMData.isInit_unique {A : Type} {M : TMData A} (hwf : M.WellFormed) (hstart : ∀ (q q' : A), M.Start q → M.Start q' → q = q') {c c' : Config A} (h : M.IsInit c) (h' : M.IsInit c') : c = c'

A machine with one start state has at most one initial configuration: the start state and the lowest position are pinned, and well-formedness makes the initial tape functional.

theorem DescriptiveComplexity.TMData.exists_isInit {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {q₀ : A} (hq : M.Start q₀) : ∃ (c₀ : Config A), M.IsInit c₀ ∧ c₀.state = q₀

A well-formed machine with a start state has an initial configuration: put the head on the lowest position and read the tape off the input, filling the unwritten cells with the blank.

Transport along an equivalence of universes

structure DescriptiveComplexity.TMData.Agree {A B : Type} (u : B ≃ A) (N : TMData B) (M : TMData A) : Prop

Two machines over different universes agree along an equivalence when every relation of one is the pullback of the other's.

• posn (b : B) : N.Posn b ↔ M.Posn (u b)

  The positions correspond.

• le (b b' : B) : N.Le b b' ↔ M.Le (u b) (u b')

  The orders correspond.

• tr (b : B) : N.Tr b ↔ M.Tr (u b)

  The transitions correspond.

• start (b : B) : N.Start b ↔ M.Start (u b)

  The start states correspond.

• acc (b : B) : N.Acc b ↔ M.Acc (u b)

  The accepting states correspond.

• blank (b : B) : N.Blank b ↔ M.Blank (u b)

  The blanks correspond.

• right (b : B) : N.Right b ↔ M.Right (u b)

  The directions correspond.

• src (b b' : B) : N.Src b b' ↔ M.Src (u b) (u b')

  The sources correspond.

• read (b b' : B) : N.Read b b' ↔ M.Read (u b) (u b')

  The read symbols correspond.

• dst (b b' : B) : N.Dst b b' ↔ M.Dst (u b) (u b')

  The destinations correspond.

• write (b b' : B) : N.Write b b' ↔ M.Write (u b) (u b')

  The written symbols correspond.

• inp (b b' : B) : N.Inp b b' ↔ M.Inp (u b) (u b')

  The inputs correspond.

def DescriptiveComplexity.Config.map {A B : Type} (u : B ≃ A) (c : Config B) : Config A

Transport of a configuration along an equivalence.

Equations

• DescriptiveComplexity.Config.map u c = { state := u c.state, head := u c.head, tape := fun (p : A) => u (c.tape (u.symm p)) }

@[simp]

theorem DescriptiveComplexity.Config.map_state {A B : Type} (u : B ≃ A) (c : Config B) : (map u c).state = u c.state

@[simp]

theorem DescriptiveComplexity.Config.map_head {A B : Type} (u : B ≃ A) (c : Config B) : (map u c).head = u c.head

@[simp]

theorem DescriptiveComplexity.Config.map_tape {A B : Type} (u : B ≃ A) (c : Config B) (p : A) : (map u c).tape p = u (c.tape (u.symm p))

theorem DescriptiveComplexity.Config.map_surjective {A B : Type} (u : B ≃ A) : Function.Surjective (map u)

Every configuration over A is the transport of one over B.

theorem DescriptiveComplexity.Config.map_injective {A B : Type} (u : B ≃ A) : Function.Injective (map u)

theorem DescriptiveComplexity.TMData.Agree.minPos {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {b : B} : MinPos N.Le N.Posn b ↔ MinPos M.Le M.Posn (u b)

theorem DescriptiveComplexity.TMData.Agree.succPos {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {b b' : B} : SuccPos N.Le N.Posn b b' ↔ SuccPos M.Le M.Posn (u b) (u b')

theorem DescriptiveComplexity.TMData.Agree.initTape {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {b b' : B} : N.InitTape b b' ↔ M.InitTape (u b) (u b')

theorem DescriptiveComplexity.TMData.Agree.isInit {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {c : Config B} : N.IsInit c ↔ M.IsInit (Config.map u c)

theorem DescriptiveComplexity.TMData.Agree.step {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {c c' : Config B} : N.Step c c' ↔ M.Step (Config.map u c) (Config.map u c')

theorem DescriptiveComplexity.TMData.Agree.stepsIn {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) (n : ℕ) (c c' : Config B) : N.StepsIn n c c' ↔ M.StepsIn n (Config.map u c) (Config.map u c')

theorem DescriptiveComplexity.TMData.Agree.accepts {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) : N.Accepts ↔ M.Accepts

Acceptance transports along an equivalence.

theorem DescriptiveComplexity.TMData.Agree.reach {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) (c c' : Config B) : Relation.ReflTransGen N.Step c c' ↔ Relation.ReflTransGen M.Step (Config.map u c) (Config.map u c')

Reachability in the configuration graph transports along an equivalence.

theorem DescriptiveComplexity.TMData.Agree.acceptsSpace {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) : N.AcceptsSpace ↔ M.AcceptsSpace

Acceptance in bounded space transports along an equivalence.

theorem DescriptiveComplexity.TMData.Agree.deterministic {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) : N.Deterministic ↔ M.Deterministic

Determinism transports along an equivalence.

theorem DescriptiveComplexity.TMData.Agree.wellFormed {A : Type} {M : TMData A} {B : Type} {u : B ≃ A} {N : TMData B} (h : Agree u N M) : N.WellFormed ↔ M.WellFormed

Well-formedness transports along an equivalence.