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

A run is read in three ways, and which one a construction uses is what its resource bound can see. DescriptiveComplexity.TMData.StepsIn counts exactly, so two phases of unknown length do not compose; Relation.ReflTransGen composes but carries no count, so DescriptiveComplexity.TMData.Accepts cannot read it; and DescriptiveComplexity.TMData.ReachesIn – a run of at most n steps – does both, composing by adding budgets and weakening upwards. A clocked program is written with the third and a space-bounded one with its erasure, which is how the two share their phase lemmas.

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.Agree.accepts 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 {A : Type} {x y : Config A} (state : x.state = y.state) (head : x.head = y.head) (tape : x.tape = y.tape) : x = y

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

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 neighboring 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 neighbor, 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 and not merely an implication.

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

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

Reaching one configuration from another within a budget: some run of at most n steps.

This is the form in which a program's phases are stated when the machine is on a clock. DescriptiveComplexity.TMData.StepsIn counts exactly, so two phases whose lengths are not known separately do not compose; Relation.ReflTransGen composes but carries no count, and DescriptiveComplexity.TMData.Accepts cannot read it. A budget is what does both: it composes by adding (DescriptiveComplexity.TMData.ReachesIn.trans), it weakens upwards (DescriptiveComplexity.TMData.ReachesIn.mono), so a phase may be charged more than it spends and the arithmetic done once at the end, and it still gives the witness Accepts asks for. The space-bounded reading is its erasure (DescriptiveComplexity.TMData.ReachesIn.reflTransGen).

Equations

• M.ReachesIn n c c' = ∃ k ≤ n, M.StepsIn k c c'

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.

theorem DescriptiveComplexity.TMData.reflTransGen_of_stepsIn {A : Type} {M : TMData A} {n : ℕ} {c d : Config A} : M.StepsIn n c d → Relation.ReflTransGen M.Step c d

A budgeted run is a run: the space-bounded reading of acceptance forgets the count, so every lemma stated with DescriptiveComplexity.TMData.StepsIn – the sweep primitives of DescriptiveComplexity.Problems.Machine.Program, in particular – feeds straight into it.

theorem DescriptiveComplexity.TMData.exists_stepsIn_of_reflTransGen {A : Type} {M : TMData A} {c d : Config A} (h : Relation.ReflTransGen M.Step c d) : ∃ (n : ℕ), M.StepsIn n c d

Every run has a length: the converse of DescriptiveComplexity.TMData.reflTransGen_of_stepsIn. A reachability claim carries no count, but a chain of steps has one, so a phase proved without a budget can still be handed to a caller that needs one – the count is whatever the chain happens to be.

The algebra of budgets

theorem DescriptiveComplexity.TMData.StepsIn.reachesIn {A : Type} {M : TMData A} {n : ℕ} {c d : Config A} (h : M.StepsIn n c d) : M.ReachesIn n c d

A run of exactly n steps is a run within n.

theorem DescriptiveComplexity.TMData.exists_reachesIn_of_reflTransGen {A : Type} {M : TMData A} {c d : Config A} (h : Relation.ReflTransGen M.Step c d) : ∃ (n : ℕ), M.ReachesIn n c d

Every run has a budget, the same fact stated for DescriptiveComplexity.TMData.ReachesIn.

theorem DescriptiveComplexity.TMData.ReachesIn.mono {A : Type} {M : TMData A} {n m : ℕ} {c d : Config A} (hnm : n ≤ m) (h : M.ReachesIn n c d) : M.ReachesIn m c d

A budget may be raised, which is what makes phases of different lengths composable: each is charged a bound it need not meet.

theorem DescriptiveComplexity.TMData.reachesIn_refl {A : Type} {M : TMData A} {n : ℕ} {c : Config A} : M.ReachesIn n c c

Standing still costs nothing.

theorem DescriptiveComplexity.TMData.reachesIn_of_step {A : Type} {M : TMData A} {c d : Config A} (h : M.Step c d) : M.ReachesIn 1 c d

One step costs one.

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

Budgeted runs compose, and their budgets add. This is the whole reason for the notion: a program's cost is read off its phases as a sum, and compared with the clock once.

theorem DescriptiveComplexity.TMData.ReachesIn.tail {A : Type} {M : TMData A} {n : ℕ} {c d e : Config A} (h : M.ReachesIn n c d) (hstep : M.Step d e) : M.ReachesIn (n + 1) c e

A budgeted run extended by one step at its end.

theorem DescriptiveComplexity.TMData.ReachesIn.head {A : Type} {M : TMData A} {n : ℕ} {c d e : Config A} (hstep : M.Step c d) (h : M.ReachesIn n d e) : M.ReachesIn (n + 1) c e

A budgeted run extended by one step at its start.

theorem DescriptiveComplexity.TMData.reachesIn_five {A : Type} {M : TMData A} {n : ℕ} {c₀ c₁ c₂ c₃ c₄ c₅ : Config A} (h₁ : M.Step c₀ c₁) (h₂ : M.ReachesIn n c₁ c₂) (h₃ : M.Step c₂ c₃) (h₄ : M.ReachesIn n c₃ c₄) (h₅ : M.Step c₄ c₅) : M.ReachesIn (2 * n + 3) c₀ c₅

Five legs, added up: two runs of the same length with a step before, between and after them. This is the shape a program's opening has – enter, a sweep, turn round, a sweep, enter the next phase – and the addition is all there is to its cost.

theorem DescriptiveComplexity.TMData.ReachesIn.reflTransGen {A : Type} {M : TMData A} {n : ℕ} {c d : Config A} (h : M.ReachesIn n c d) : Relation.ReflTransGen M.Step c d

A budgeted run is a run. The erasure that turns every statement of a clocked program into the corresponding statement of a space-bounded one, which is why the two models share their phase lemmas.

theorem DescriptiveComplexity.TMData.accepts_of_reachesIn {A : Type} {M : TMData A} {n : ℕ} {c₀ c : Config A} (hinit : M.IsInit c₀) (hrun : M.ReachesIn n c₀ c) (hlt : n < Nat.card { p : A // M.Posn p }) (hacc : M.Acc c.state) : M.Accepts

A budgeted run that ends accepting makes the machine accept, provided the budget is below the clock. The one place a program's arithmetic meets DescriptiveComplexity.TMData.Accepts.

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.