Turing machines on an unbounded tape

The third acceptance notion of DescriptiveComplexity.TMData, beside DescriptiveComplexity.TMData.Accepts (a run bounded by the number of positions, hence NP) and DescriptiveComplexity.TMData.AcceptsSpace (a run of any length on a tape indexed by the positions, hence PSPACE): a run of any length on a tape that leaves the instance. It is the acceptance notion of the halting problem, and the one whose certificate no function of the instance bounds – which is what puts it in RE and nowhere lower.

The machine itself is unchanged: the vocabulary, the record DescriptiveComplexity.TMData, its well-formedness and the whole Agree transport layer are reused. Only the configuration changes, and it has to: DescriptiveComplexity.Config has tape : A → A, so space-boundedness is built into the type.

The cells: an unbounded strip of pages

A cell is a pair (z, p) : ℤ × A with p a position, ordered lexicographically – an unbounded strip of pages, each page a copy of the instance's positions, with the input on page 0:

   … ‖ page -1 ‖ page 0 (the input) ‖ page 1 ‖ …
          p₀ … pₙ      p₀ … pₙ           p₀ … pₙ

On a finite instance this is an ordinary two-way infinite tape up to renaming the cells (ℤ ×ₗ {p // Posn p} is order-isomorphic to ℤ). Naming the cells by a page and an offset rather than by an integer is what keeps all arithmetic out of the semantics: the head's move (DescriptiveComplexity.TMData.SuccCell) is one step of DescriptiveComplexity.SuccPos inside a page, or the step from the last position of a page to the first position of the next, so the order vocabulary of DescriptiveComplexity.Numbers.BinRel covers it unchanged. It is also what places the input with no rank function: the input is page 0.

Unlike the bounded model, no move is ever impossible: there is no “the head falls off the end and the run stops” case, one branch fewer in every proof downstream.

structure DescriptiveComplexity.ConfigU (A : Type) : Type

A configuration of a machine on an unbounded tape: the current state, the cell the head is on, and the contents of every cell. A cell is a pair of a page – an integer – and a position of the instance.

• state : A

  The current state.

• head : ℤ × A

  The cell the head is on.

• tape : ℤ × A → A

  The symbol in each cell.

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

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

def DescriptiveComplexity.TMData.SuccCell {A : Type} (M : TMData A) (c c' : ℤ × A) : Prop

The next cell: one step along the order of the positions inside a page, or the step from the last position of a page to the first position of the next page. Since the pages are indexed by ℤ, every cell has a next one and a previous one, on a well-formed machine with at least one position.

Equations

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

def DescriptiveComplexity.TMData.IsInitU {A : Type} (M : TMData A) (c : ConfigU A) : Prop

Being an initial configuration on an unbounded tape: a start state, the head on the lowest position of page 0, the input on page 0 and blanks everywhere else.

Equations

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

def DescriptiveComplexity.TMData.StepU {A : Type} (M : TMData A) (c c' : ConfigU A) : Prop

One step on an unbounded tape: the clauses of DescriptiveComplexity.TMData.Step, with DescriptiveComplexity.TMData.SuccCell in place of DescriptiveComplexity.SuccPos for the move.

Equations

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

def DescriptiveComplexity.TMData.StepsInU {A : Type} (M : TMData A) : ℕ → ConfigU A → ConfigU A → Prop

Reaching one configuration from another in exactly n steps.

Equations

• M.StepsInU 0 x✝¹ x✝ = (x✝¹ = x✝)
• M.StepsInU n.succ x✝¹ x✝ = ∃ (d : DescriptiveComplexity.ConfigU A), M.StepU x✝¹ d ∧ M.StepsInU n d x✝

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

Acceptance on an unbounded tape: some run from an initial configuration reaches an accepting state, in any number of steps whatever.

This is DescriptiveComplexity.TMData.Accepts with the step bound dropped and DescriptiveComplexity.TMData.AcceptsSpace with the space bound dropped: the same ∃ n, with nothing bounding it and nothing bounding the tape. A run is still a finite object, so acceptance is an unbounded search over finite witnesses – the shape of ∃SO[new], and the reason the halting problem is in RE and in nothing smaller.

Equations

• M.AcceptsU = ∃ (c₀ : DescriptiveComplexity.ConfigU A) (c : DescriptiveComplexity.ConfigU A) (n : ℕ), M.IsInitU c₀ ∧ M.StepsInU n c₀ c ∧ M.Acc c.state

theorem DescriptiveComplexity.TMData.StepsInU.trans_step {A : Type} {M : TMData A} {n : ℕ} {c d e : ConfigU A} : M.StepsInU n c d → M.StepU d e → M.StepsInU (n + 1) c e

A run extended by one more step at its end.

theorem DescriptiveComplexity.TMData.stepsInU_succ_iff {A : Type} {M : TMData A} {n : ℕ} {c e : ConfigU A} : M.StepsInU (n + 1) c e ↔ ∃ (d : ConfigU A), M.StepsInU n c d ∧ M.StepU d e

A run decomposed at its far end: n + 1 steps are n steps and then one. DescriptiveComplexity.TMData.StepsInU recurses at the near end, while an induction along the time order needs this reading.

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

Runs compose; the step counts add.

The head stays in a bounded band of pages

A run of n steps moves the head by at most one page per step, so the pages it visits lie within n of the page it started on. This is what makes the certificate of the membership proof finite, and it is the only quantitative fact the unbounded model needs.

theorem DescriptiveComplexity.TMData.page_dist_stepU {A : Type} {M : TMData A} {c c' : ConfigU A} (h : M.StepU c c') : (c'.head.1 - c.head.1).natAbs ≤ 1

One step moves the head by at most one page, in either direction.

theorem DescriptiveComplexity.TMData.page_dist_stepsInU {A : Type} {M : TMData A} {n : ℕ} {c c' : ConfigU A} : M.StepsInU n c c' → (c'.head.1 - c.head.1).natAbs ≤ n

The band of a run: after n steps the head is within n pages of where it started.

Transport along an equivalence of universes

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

Transport of an unbounded configuration along an equivalence: the page of a cell is untouched, the offset and the contents move along u.

Equations

• DescriptiveComplexity.ConfigU.map u c = { state := u c.state, head := (c.head.1, u c.head.2), tape := fun (x : ℤ × A) => u (c.tape (x.1, u.symm x.2)) }

@[simp]

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

@[simp]

theorem DescriptiveComplexity.ConfigU.map_head {A B : Type} (u : B ≃ A) (c : ConfigU B) : (map u c).head = (c.head.1, u c.head.2)

@[simp]

theorem DescriptiveComplexity.ConfigU.map_tape {A B : Type} (u : B ≃ A) (c : ConfigU B) (x : ℤ × A) : (map u c).tape x = u (c.tape (x.1, u.symm x.2))

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

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

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

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

Highest positions correspond, the companion of DescriptiveComplexity.TMData.Agree.minPos: the bounded model never mentions a highest position, but the page-crossing move does.

theorem DescriptiveComplexity.TMData.Agree.succCell {A B : Type} {M : TMData A} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {c c' : ℤ × B} : N.SuccCell c c' ↔ M.SuccCell (c.1, u c.2) (c'.1, u c'.2)

theorem DescriptiveComplexity.TMData.Agree.isInitU {A B : Type} {M : TMData A} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {c : ConfigU B} : N.IsInitU c ↔ M.IsInitU (ConfigU.map u c)

theorem DescriptiveComplexity.TMData.Agree.stepU {A B : Type} {M : TMData A} {u : B ≃ A} {N : TMData B} (h : Agree u N M) {c c' : ConfigU B} : N.StepU c c' ↔ M.StepU (ConfigU.map u c) (ConfigU.map u c')

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

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

Acceptance on an unbounded tape transports along an equivalence.