The drawn instance has a match exactly when the machine accepts #

The combinatorial half of the correctness of the reduction from DescriptiveComplexity.HALT to DescriptiveComplexity.PCP, over any Language.pcp-structure whose four relations read as the semantic predicates of DescriptiveComplexity.Problems.Pcp.Hardness.Draw (DescriptiveComplexity.HaltPcp.Reads) – which is exactly what the interpretation of the sibling Interp file provides.

Words by tables #

Everything a word of the drawn instance says is of the form “the pair (position, letter) is an entry of a zipped table”, with the position side strictly increasing. Two abstract lemmas turn such a table into the unique word of a domino (DescriptiveComplexity.HaltPcp.isWord_of_zip, DescriptiveComplexity.HaltPcp.eq_of_isWord_zip): the enumeration of the used positions is pinned by sortedness, and the letters by functionality of the zip. The short words instantiate them at the shared position prefix; the start domino's bottom word at its own layout, whose table DescriptiveComplexity.HaltPcp.startBotAt_iff_zip is proved by walking the input page along the enumeration of the positions.

The two directions #

A match of DescriptiveComplexity.Pcp.History maps to a solution of the instance by encoding each abstract domino (DescriptiveComplexity.HaltPcp.exists_encode) and reading the tables forward; a solution maps back by decoding each marked element (DescriptiveComplexity.HaltPcp.decodeDom) and using uniqueness of the words, injectivity of the letter map turning the equality of the two concatenations back into the equality of the abstract words. Chained with DescriptiveComplexity.HaltPcp.acceptsU_iff_hasMatch, this gives the correctness statement DescriptiveComplexity.HaltPcp.pcpOn_iff_of_reads the Interp file consumes.

Sorted lists, zips and tables #

Reading the instance #

source

structure DescriptiveComplexity.HaltPcp.Reads {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] (e : B ≃ PV A) :

Prop

The four relations of the instance read as the drawn predicates, along an equivalence of the universes. This is what the defining formulas of the interpretation are proved to realize.

ord (x y : B) : Pcp.Ord x y ↔ PLe (e x) (e y)
The order of the positions is the drawn order.
dom (x : B) : Pcp.DomG x ↔ PDom (e x)
The marked dominoes are the drawn dominoes.
uAt (d p c : B) : Pcp.UAt d p c ↔ PUAt (e d) (e p) (e c)
The top words read off the top tables.
vAt (d p c : B) : Pcp.VAt d p c ↔ PVAt (e d) (e p) (e c)
The bottom words read off the bottom tables.

Instances For

Dependency graph

source

theorem DescriptiveComplexity.HaltPcp.Reads.ordLt {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} (h : Reads e) (x y : B) :

Pcp.OrdLt x y ↔ PLt (e x) (e y)

Dependency graph

Tables are words #

DescriptiveComplexity.Pcp.IsWordU/IsWordV both have the shape “some strictly increasing enumeration of the used positions carries the word”; the two lemmas below handle any letter relation given by a zipped table with a strictly increasing position side.

source

theorem DescriptiveComplexity.HaltPcp.isWord_of_zip {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} {R : B → B → Prop} {P W : List (PV A)} (h : Reads e) (hlen : P.length = W.length) (hsort : List.Pairwise PLt P) (htab : ∀ (p c : B), R p c ↔ (e p, e c) ∈ P.zip W) :

∃ (ps : List B), List.Pairwise Pcp.OrdLt ps ∧ (∀ (p : B), p ∈ ps ↔ ∃ (c : B), R p c) ∧ List.Forall₂ R ps (List.map (⇑e.symm) W)

A table is a word: the position side, transported, enumerates the used positions in order and carries the letter side.

Dependency graph

source

theorem DescriptiveComplexity.HaltPcp.eq_of_isWord_zip {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {B : Type} [FirstOrder.Language.pcp.Structure B] {e : B ≃ PV A} {R : B → B → Prop} {P W : List (PV A)} (h : Reads e) (hasym : ∀ (x y : B), Pcp.OrdLt x y → Pcp.OrdLt y x → False) (hlen : P.length = W.length) (hsort : List.Pairwise PLt P) (htab : ∀ (p c : B), R p c ↔ (e p, e c) ∈ P.zip W) {ps w : List B} (hps : List.Pairwise Pcp.OrdLt ps) (hmem : ∀ (p : B), p ∈ ps ↔ ∃ (c : B), R p c) (hf : List.Forall₂ R ps w) :

w = List.map (⇑e.symm) W

The word of a table is unique: any word of the letter relation is the letter side of the table.

Dependency graph

The tables of the dominoes #

The start domino's table #

source

theorem DescriptiveComplexity.HaltPcp.startBotAt_iff_zip {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hwf : (tmData A).WellFormed) {ps inp : List A} (hps : IsPosEnum (tmData A) ps) (hinp : List.Forall₂ (tmData A).InitTape ps inp) {p c : PV A} :

StartBotAt p c ↔ (p, c) ∈ (startPos ps).zip (startBot inp)

The layout of the start domino's bottom word is its table: the letter relation of the start domino says exactly that the pair is an entry of the zipped layout.

Dependency graph