The certificate as relations on invented values

DescriptiveComplexity.TMData.RunCert carries the two orders as types and the run as functions, which is what made the combinatorics of DescriptiveComplexity.TMData.acceptsU_iff_runCert short. An ∃SO[new] certificate cannot: its relation variables range over A ⊕ Fin m, so the two sorts have to become unary predicates on the invented values, their orders binary relations, and the four functions relations with totality and functionality demanded of them.

DescriptiveComplexity.TMData.RunRel is that presentation and DescriptiveComplexity.TMData.RunRelOK its conditions, each of them a clause the first-order kernel can mirror. The two ends of the time order and the step relation are DescriptiveComplexity.MinPos, DescriptiveComplexity.MaxPos and DescriptiveComplexity.SuccPos – the same order vocabulary the bounded machine problems already use, reused here on a guessed order rather than on the instance's.

The two sorts need not be disjoint. Time and Page are independent predicates on the invented values, and nothing asks them to be apart; that is what lets the run of n steps be read off over Fin (2n + 1) alone, with the time points the first n + 1 values and the pages all of them, instead of over a disjoint sum that would then have to be transported to a Fin m.

Linear orders on a marked subset

def DescriptiveComplexity.TMData.IsLinOrdOn {D : Type} (Le : D → D → Prop) (S : D → Prop) : Prop

A relation is a linear order on the elements marked by S: the form a first-order kernel states a guessed order in, since the guessed order says nothing outside the sort it is meant for.

Equations

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

theorem DescriptiveComplexity.TMData.isLinOrd_subtype {D : Type} {Le : D → D → Prop} {S : D → Prop} (h : IsLinOrdOn Le S) : IsLinOrd fun (x y : { d : D // S d }) => Le ↑x ↑y

A linear order on a marked subset is a linear order on the subtype it marks.

The certificate, as relations

structure DescriptiveComplexity.TMData.RunRel (A D : Type) : Type

A run, as relations on the invented values: two sorts with their orders, the input page, and the state, the head and the tape contents as relations rather than functions.

• Time : D → Prop

  The invented values that are time points.

• TLe : D → D → Prop

  The order of time.

• Page : D → Prop

  The invented values that are pages.

• PLe : D → D → Prop

  The order of the pages.

• Zero : D → Prop

  The input page.

• St : D → A → Prop

  St t q: the state at the time point t.

• HdP : D → D → Prop

  HdP t z: the page the head is on at the time point t.

• HdC : D → A → Prop

  HdC t p: the position within that page.

• Sym : D → D → A → A → Prop

  Sym t z p a: the cell (z, p) holds a at the time point t.

def DescriptiveComplexity.TMData.SuccCellRel {A D : Type} (M : TMData A) (c : RunRel A D) (z : D) (p : A) (z' : D) (p' : A) : Prop

The next cell, over the guessed order of the pages: DescriptiveComplexity.TMData.SuccCellAt with covering replaced by DescriptiveComplexity.SuccPos on the marked pages.

Equations

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

structure DescriptiveComplexity.TMData.RunRelOK {A D : Type} (M : TMData A) (c : RunRel A D) : Prop

The conditions making the relations a run. Beside the shape conditions – the two orders are linear on their sorts, the input page is unique, and the four relations are total and functional where they are read – there are the three of DescriptiveComplexity.TMData.RunOK: initial at the lowest time point, one transition along every step of the time order, accepting at the highest.

• time_ne : ∃ (t : D), c.Time t

  There is a time point.

• tle_lin : IsLinOrdOn c.TLe c.Time

  Time is linearly ordered.

• page_ne : ∃ (z : D), c.Page z

  There is a page.

• ple_lin : IsLinOrdOn c.PLe c.Page

  The pages are linearly ordered.

• zero_ex : ∃ (z : D), c.Zero z

  There is an input page.

• zero_page (z : D) : c.Zero z → c.Page z

  The input page is a page.

• zero_uniq (z z' : D) : c.Zero z → c.Zero z' → z = z'

  There is at most one input page.

• st_tot (t : D) : c.Time t → ∃ (q : A), c.St t q

  Every time point has a state.

• st_fun (t : D) (q q' : A) : c.St t q → c.St t q' → q = q'

  A time point has at most one state.

• hdP_tot (t : D) : c.Time t → ∃ (z : D), c.Page z ∧ c.HdP t z

  At every time point the head is on a page.

• hdP_fun (t z z' : D) : c.HdP t z → c.HdP t z' → z = z'

  The head is on at most one page.

• hdC_tot (t : D) : c.Time t → ∃ (p : A), c.HdC t p

  At every time point the head is at a position of its page.

• hdC_fun (t : D) (p p' : A) : c.HdC t p → c.HdC t p' → p = p'

  The head is at most at one position.

• sym_tot (t z : D) (p : A) : c.Time t → c.Page z → ∃ (a : A), c.Sym t z p a

  Every cell holds a symbol at every time point.

• sym_fun (t z : D) (p a a' : A) : c.Sym t z p a → c.Sym t z p a' → a = a'

  A cell holds at most one symbol.

• init (t : D) (q : A) (z : D) (p : A) : MinPos c.TLe c.Time t → c.St t q → c.HdP t z → c.HdC t p → M.Start q ∧ c.Zero z ∧ MinPos M.Le M.Posn p ∧ ∀ (z' : D) (p' a : A), c.Page z' → M.Posn p' → c.Sym t z' p' a → (c.Zero z' → M.InitTape p' a) ∧ (¬c.Zero z' → M.Blank a)

  At the lowest time point the configuration is initial.

• step (t t' : D) (q q' : A) (z : D) (p a a' : A) : SuccPos c.TLe c.Time t t' → c.St t q → c.St t' q' → c.HdP t z → c.HdC t p → c.Sym t z p a → c.Sym t' z p a' → ∃ (τ : A), M.Tr τ ∧ M.Src τ q ∧ M.Read τ a ∧ M.Dst τ q' ∧ M.Write τ a' ∧ (∀ (z₁ : D) (p₁ b b' : A), c.Page z₁ → ¬(z₁ = z ∧ p₁ = p) → c.Sym t z₁ p₁ b → c.Sym t' z₁ p₁ b' → b = b') ∧ ∀ (z₂ : D) (p₂ : A), c.HdP t' z₂ → c.HdC t' p₂ → M.Right τ ∧ M.SuccCellRel c z p z₂ p₂ ∨ ¬M.Right τ ∧ M.SuccCellRel c z₂ p₂ z p

  Along every step of the time order, one transition applies.

• acc (t : D) (q : A) : MaxPos c.TLe c.Time t → c.St t q → M.Acc q

  At the highest time point the state is accepting.

From the relations to a run

The two sorts become the subtypes they mark, the four relations become functions by choice, and DescriptiveComplexity.TMData.acceptsU_of_runCert does the rest. The only work is the dictionary between the order vocabulary on the marked sets (MinPos, MaxPos, SuccPos) and the order of the subtype (least, greatest, covering).

The dictionary between the order vocabulary on a marked set (MinPos, MaxPos, SuccPos) and the order of the subtype it marks (least, greatest, covering). Stated for an arbitrary linear order on the subtype whose ≤ is the marked relation, so that the instance built by DescriptiveComplexity.IsLinOrd.toLinearOrder is not baked into the statements.

theorem DescriptiveComplexity.TMData.minPos_of_le {D : Type} {Le : D → D → Prop} {S : D → Prop} [LinearOrder { d : D // S d }] (hle : ∀ (a b : { d : D // S d }), a ≤ b ↔ Le ↑a ↑b) {t : { d : D // S d }} (ht : ∀ (t' : { d : D // S d }), t ≤ t') : MinPos Le S ↑t

A least element of the subtype is a lowest marked element.

theorem DescriptiveComplexity.TMData.maxPos_of_le {D : Type} {Le : D → D → Prop} {S : D → Prop} [LinearOrder { d : D // S d }] (hle : ∀ (a b : { d : D // S d }), a ≤ b ↔ Le ↑a ↑b) {t : { d : D // S d }} (ht : ∀ (t' : { d : D // S d }), t' ≤ t) : MaxPos Le S ↑t

A greatest element of the subtype is a highest marked element.

theorem DescriptiveComplexity.TMData.succPos_of_covBy {D : Type} {Le : D → D → Prop} {S : D → Prop} [LinearOrder { d : D // S d }] (hle : ∀ (a b : { d : D // S d }), a ≤ b ↔ Le ↑a ↑b) {a b : { d : D // S d }} (hab : a ⋖ b) : SuccPos Le S ↑a ↑b

Covering in the subtype is the successor relation on the marked set.

theorem DescriptiveComplexity.TMData.covBy_of_succPos {D : Type} {Le : D → D → Prop} {S : D → Prop} [LinearOrder { d : D // S d }] (hle : ∀ (a b : { d : D // S d }), a ≤ b ↔ Le ↑a ↑b) {a b : { d : D // S d }} (hs : SuccPos Le S ↑a ↑b) : a ⋖ b

…and conversely.

theorem DescriptiveComplexity.TMData.acceptsU_of_runRel {A D : Type} {M : TMData A} [Finite D] (hb : ∃ (b : A), M.Blank b) {c : RunRel A D} (h : M.RunRelOK c) : M.AcceptsU

The relations are realized by a run: the two sorts are the subtypes they mark, and the four relations become functions by choice.

From a run to the relations

The time points are the first n + 1 values of Fin (2n + 1) and the pages all of them: the two sorts are not disjoint, and need not be, which is what keeps the invented values a single Fin m with no disjoint sum to transport.

theorem DescriptiveComplexity.TMData.runRel_of_acceptsU {A : Type} {M : TMData A} (h : M.AcceptsU) : ∃ (m : ℕ) (c : RunRel A (Fin m)), M.RunRelOK c

A machine that accepts carries a relational certificate on Fin m.

theorem DescriptiveComplexity.TMData.acceptsU_iff_runRel {A : Type} {M : TMData A} (hb : ∃ (b : A), M.Blank b) : M.AcceptsU ↔ ∃ (m : ℕ) (c : RunRel A (Fin m)), M.RunRelOK c

Acceptance on an unbounded tape is a relational certificate on invented values: the statement the ∃SO[new] kernel of the membership proof mirrors clause by clause.

The statement the kernel mirrors

Everything above, at the problem: what remains for HALT ∈ RE is to write DescriptiveComplexity.TMData.RunRelOK and DescriptiveComplexity.TMData.WellFormed as a first-order kernel over the extended universe, with each quantifier guarded by its sort.

theorem DescriptiveComplexity.halt_iff_runRel (A : Type) [FirstOrder.Language.turing.Structure A] : HALT.Holds A ↔ (tmData A).WellFormed ∧ ∃ (m : ℕ) (c : TMData.RunRel A (Fin m)), (tmData A).RunRelOK c

HALT is well-formedness together with a relational certificate on invented values. The right-hand side is a conjunction of first-order conditions on the instance and on a block of nine relation variables, which is exactly what an ∃SO[new] sentence says.