An accepting run, read off as a finite certificate

The mathematical content of HALT ∈ RE: a machine accepts on an unbounded tape exactly when a finite amount of data witnesses it, namely a finite linear order of time points, a finite linear order of pages with a distinguished input page, and the state, the head and the tape contents at each time.

Neither order is bounded by the instance – that is the whole point, and it is why the certificate needs invented values rather than tuples of the universe – but both are finite, because a run of n steps has n + 1 time points and moves the head by at most one page per step (DescriptiveComplexity.TMData.page_dist_stepsInU), so it stays inside a band of 2n + 1 pages.

The shape of the certificate

DescriptiveComplexity.TMData.RunCert is the data – four functions, not relations, because the combinatorics is much lighter that way; the first-order kernel of the membership proof adds their totality and functionality as conjuncts – and DescriptiveComplexity.TMData.RunOK the conditions:

• at a least time point the configuration is initial: a start state, the head on the lowest position of the input page, the input on that page and blanks on every other;
• between two time points one covering the other, some transition applies, writes, moves and leaves every other cell alone;
• at a greatest time point the state is accepting.

The conditions are stated with “least” and “greatest” as hypotheses rather than with ⊥ and ⊤ so that they transcribe literally into first-order logic, where that is how the ends of a guessed order are named.

The page successor of the step clause is DescriptiveComplexity.TMData.SuccCellAt, which is DescriptiveComplexity.TMData.SuccCell with z + 1 replaced by “z is covered by z'”: the certificate's pages are an abstract order, and covering is what a first-order kernel can say about one.

Reading a run off as a sequence

DescriptiveComplexity.TMData.StepsInU is an existential chain; the certificate needs it as a function of the time index, which is what these two lemmas supply.

theorem DescriptiveComplexity.TMData.exists_runU {A : Type} {M : TMData A} (n : ℕ) (c d : ConfigU A) : M.StepsInU n c d → ∃ (f : ℕ → ConfigU A), f 0 = c ∧ f n = d ∧ ∀ i < n, M.StepU (f i) (f (i + 1))

A run is a sequence of configurations.

theorem DescriptiveComplexity.TMData.stepsInU_of_steps {A : Type} {M : TMData A} {n : ℕ} {f : ℕ → ConfigU A} (hs : ∀ i < n, M.StepU (f i) (f (i + 1))) (i : ℕ) : i ≤ n → M.StepsInU i (f 0) (f i)

The prefix of a sequence of steps is a run.

The certificate

def DescriptiveComplexity.TMData.SuccCellAt {A P : Type} [Preorder P] (M : TMData A) (z : P) (p : A) (z' : P) (p' : A) : Prop

The next cell, over an abstract order of pages: DescriptiveComplexity.TMData.SuccCell with “the next page” read as covering rather than as z + 1.

Equations

• M.SuccCellAt z p z' p' = (z' = z ∧ DescriptiveComplexity.SuccPos M.Le M.Posn p p' ∨ z ⋖ z' ∧ DescriptiveComplexity.MaxPos M.Le M.Posn p ∧ DescriptiveComplexity.MinPos M.Le M.Posn p')

structure DescriptiveComplexity.TMData.RunCert (A T P : Type) : Type

A run, as finite data: the state, the page and the offset of the head, and the contents of every cell, at each time point.

• st : T → A

  The state at a time point.

• hdP : T → P

  The page the head is on at a time point.

• hdC : T → A

  The position within that page.

• sym : T → P → A → A

  The symbol a cell holds at a time point.

structure DescriptiveComplexity.TMData.RunOK {A T P : Type} [Preorder T] [Preorder P] (M : TMData A) (zero : P) (r : RunCert A T P) : Prop

The conditions making the data a run: initial at a least time point, one transition along every cover, accepting at a greatest one.

• init (t : T) : (∀ (t' : T), t ≤ t') → M.Start (r.st t) ∧ r.hdP t = zero ∧ MinPos M.Le M.Posn (r.hdC t) ∧ ∀ (p : A), M.Posn p → M.InitTape p (r.sym t zero p) ∧ ∀ (z : P), z ≠ zero → M.Blank (r.sym t z p)

  At a least time point the configuration is initial.

• step (t t' : T) : t ⋖ t' → ∃ (τ : A), M.Tr τ ∧ M.Src τ (r.st t) ∧ M.Read τ (r.sym t (r.hdP t) (r.hdC t)) ∧ M.Dst τ (r.st t') ∧ M.Write τ (r.sym t' (r.hdP t) (r.hdC t)) ∧ (∀ (z : P) (p : A), ¬(z = r.hdP t ∧ p = r.hdC t) → r.sym t' z p = r.sym t z p) ∧ (M.Right τ ∧ M.SuccCellAt (r.hdP t) (r.hdC t) (r.hdP t') (r.hdC t') ∨ ¬M.Right τ ∧ M.SuccCellAt (r.hdP t') (r.hdC t') (r.hdP t) (r.hdC t))

  Along a cover of the time order, one transition applies.

• acc (t : T) : (∀ (t' : T), t' ≤ t) → M.Acc (r.st t)

  At a greatest time point the state is accepting.

From a run to a certificate

The time points are Fin (n + 1) and the pages Fin (2n + 1), the page z standing for the integer z - n: by DescriptiveComplexity.TMData.page_dist_stepsInU the head of a run of n steps starting on page 0 never leaves that band.

theorem DescriptiveComplexity.TMData.runCert_of_acceptsU {A : Type} {M : TMData A} (h : M.AcceptsU) : ∃ (n : ℕ) (zero : Fin (2 * n + 1)) (r : RunCert A (Fin (n + 1)) (Fin (2 * n + 1))), M.RunOK zero r

A run yields a certificate: the time points are the steps of the run and the pages the band the head stays inside.

From a certificate to a run

The converse: an abstract certificate is realized by an actual run on the unbounded tape. The pages are embedded into ℤ by their rank, shifted so that the input page goes to 0; every cell outside that image holds the blank, and the head never reaches one, since the step clause moves it along a cover of the page order.

theorem DescriptiveComplexity.TMData.acceptsU_of_runCert {A T P : Type} {M : TMData A} [LinearOrder T] [Finite T] [Nonempty T] [LinearOrder P] [Finite P] (hb : ∃ (b : A), M.Blank b) {zero : P} {r : RunCert A T P} (h : M.RunOK zero r) : M.AcceptsU

A certificate is realized by a run: the abstract time order supplies the steps and the abstract page order the cells, so an accepting certificate makes the machine accept on the unbounded tape.

The equivalence

theorem DescriptiveComplexity.TMData.acceptsU_iff_runCert {A : Type} {M : TMData A} (hb : ∃ (b : A), M.Blank b) : M.AcceptsU ↔ ∃ (T : Type) (P : Type) (x : LinearOrder T) (_ : Finite T) (_ : Nonempty T) (x_3 : LinearOrder P) (_ : Finite P) (zero : P) (r : RunCert A T P), M.RunOK zero r

Acceptance on an unbounded tape is a finite certificate: a machine accepts exactly when some finite linear order of time points and some finite linear order of pages carry a run of it. The two orders are not bounded by the instance, which is why the certificate needs invented values; they are finite, which is why it is a certificate at all.