A match, read off as a finite certificate

The mathematical content of DescriptiveComplexity.PCP ∈ RE: a Post system has a match exactly when a finite amount of data witnesses it, and that data is a handful of relations over the instance extended by a segment of invented slots – the places of the sequence of dominoes.

The shape of the certificate

DescriptiveComplexity.Pcp.Cert is the data:

• SLe – a linear order on the slots, so that they are a sequence;
• Dm – the domino sitting at each slot;
• Mt – the matching between the two parses.

The common word is not invented, and no length or position of it is ever named. The top concatenation is cut into blocks by the slots, so its letters are indexed by the pairs (slot, position of the top word of the domino there), in lexicographic order (DescriptiveComplexity.Pcp.parseIx); the bottom concatenation is indexed the same way by its own parse. Mt s p s' p' says that the letter at the top index (s, p) is the same occurrence as the letter at the bottom index (s', p').

Why a matching is as good as an equality

Equality of the two concatenations is not first-order in the instance: it compares two words of unbounded length. A matching is a relation variable, and what a kernel can ask of it is local: that it lands in the two parses, that it is defined everywhere on both, that it reflects the two lexicographic orders, and that matched indices carry the same letter. That is already enough (DescriptiveComplexity.Pcp.forall₂_of_matching): a relation between the members of two strictly sorted lists that is total on both sides and reflects the order pairs their entries index by index, so the two concatenations agree letter by letter. Functionality and injectivity of the matching are not asked: they follow.

The two directions of DescriptiveComplexity.Pcp.pcpOn_iff_cert are therefore not symmetric in effort. A match hands its matching back for free – the two parses have the same length, so pairing them index by index (DescriptiveComplexity.Pcp.IdxMatch) does it – while a certificate has to rebuild the two words from their enumerations before the matching lemma applies.

The certificate

structure DescriptiveComplexity.Pcp.Cert (A D : Type) : Type

A match of a Post correspondence system, as relations on a segment of invented slots. SLe orders the slots; Dm s d says the domino d sits at the slot s; Mt s p s' p' matches the position p of the top word at the slot s with the position p' of the bottom word at the slot s', as occurrences of the same letter of the common word.

• SLe : D → D → Prop

  The order of the slots.

• Dm : D → A → Prop

  Dm s d: the domino d sits at the slot s.

• Mt : D → A → D → A → Prop

  Mt s p s' p': the top index (s, p) and the bottom index (s', p') are the same occurrence of the common word.

def DescriptiveComplexity.Pcp.Cert.SLt {A D : Type} (c : Cert A D) (s t : D) : Prop

Strictly earlier, in the order of the slots.

Equations

• c.SLt s t = (c.SLe s t ∧ s ≠ t)

def DescriptiveComplexity.Pcp.Cert.TopIx {A D : Type} [FirstOrder.Language.pcp.Structure A] (c : Cert A D) (s : D) (p : A) : Prop

p is a position of the top word of the domino sitting at the slot s.

Equations

• c.TopIx s p = ∃ (d : A), c.Dm s d ∧ DescriptiveComplexity.Pcp.UsedU d p

def DescriptiveComplexity.Pcp.Cert.BotIx {A D : Type} [FirstOrder.Language.pcp.Structure A] (c : Cert A D) (s : D) (p : A) : Prop

p is a position of the bottom word of the domino sitting at the slot s.

Equations

• c.BotIx s p = ∃ (d : A), c.Dm s d ∧ DescriptiveComplexity.Pcp.UsedV d p

def DescriptiveComplexity.Pcp.Cert.LexLt {A D : Type} [FirstOrder.Language.pcp.Structure A] (c : Cert A D) (s : D) (p : A) (t : D) (q : A) : Prop

The lexicographic order on the indices of a parse: first the slot, then the position inside the word sitting there. Both parses are ordered by it, which is why one matching relates them.

Equations

• c.LexLt s p t q = (c.SLt s t ∨ s = t ∧ DescriptiveComplexity.Pcp.OrdLt p q)

structure DescriptiveComplexity.Pcp.CertOK {A D : Type} [FirstOrder.Language.pcp.Structure A] (c : Cert A D) : Prop

The conditions on a certificate. The instance is well-formed, the slots are a nonempty sequence carrying one domino each, and the matching is a letter-preserving order isomorphism between the two parses – stated as being inside them, defined everywhere on both, order-reflecting, and letter-preserving.

• wf : IsWF A

  The instance is well-formed.

• sle_lin : IsLinOrd c.SLe

  The slots are linearly ordered.

• slot_ex : ∃ (s : D), c.SLe s s

  There is at least one slot: a match is a nonempty sequence.

• dm_tot (s : D) : ∃ (d : A), c.Dm s d

  Every slot carries a domino.

• dm_fun (s : D) (d d' : A) : c.Dm s d → c.Dm s d' → d = d'

  A slot carries only one domino.

• dm_dom (s : D) (d : A) : c.Dm s d → DomG d

  What a slot carries is a domino of the instance.

• mt_ix (s : D) (p : A) (s' : D) (p' : A) : c.Mt s p s' p' → c.TopIx s p ∧ c.BotIx s' p'

  The matching relates an index of the top parse to one of the bottom parse.

• mt_left (s : D) (p : A) : c.TopIx s p → ∃ (s' : D) (p' : A), c.Mt s p s' p'

  Every index of the top parse is matched.

• mt_right (s' : D) (p' : A) : c.BotIx s' p' → ∃ (s : D) (p : A), c.Mt s p s' p'

  Every index of the bottom parse is matched.

• mt_mono (s : D) (p : A) (s' : D) (p' : A) (t : D) (q : A) (t' : D) (q' : A) : c.Mt s p s' p' → c.Mt t q t' q' → (c.LexLt s p t q ↔ c.LexLt s' p' t' q')

  The matching reflects the lexicographic order of the two parses.

• mt_lab (s : D) (p : A) (s' : D) (p' d d' ℓ : A) : c.Mt s p s' p' → c.Dm s d → c.Dm s' d' → (UAt d p ℓ ↔ VAt d' p' ℓ)

  Matched indices carry the same letter.

The order of the positions

theorem DescriptiveComplexity.Pcp.isLinOrd_ord {A : Type} [FirstOrder.Language.pcp.Structure A] (h : IsWF A) : IsLinOrd Ord

The order symbol of a well-formed instance is a linear order.

theorem DescriptiveComplexity.Pcp.asymm_ordLt {A : Type} [FirstOrder.Language.pcp.Structure A] (h : IsWF A) (a b : A) (hab : OrdLt a b) (hba : OrdLt b a) : False

Strict precedence of positions is asymmetric.

From a certificate to a match

theorem DescriptiveComplexity.Pcp.pcpOn_of_cert {A D : Type} [FirstOrder.Language.pcp.Structure A] [Finite A] [Finite D] {c : Cert A D} (h : CertOK c) : PcpOn A

A certificate exhibits a match. The slots are enumerated in their order, the positions of each word in theirs, and the matching lemma turns the guessed relation into the equality of the two concatenations.

From a match to a certificate

theorem DescriptiveComplexity.Pcp.cert_of_pcpOn {A : Type} [FirstOrder.Language.pcp.Structure A] (h : PcpOn A) : ∃ (n : ℕ) (c : Cert A (Fin n)), CertOK c

A match is a certificate. The slots are the places of the sequence of dominoes, and the matching is the pairing of the two parses index by index, which is legitimate exactly because the two concatenations are the same word.

theorem DescriptiveComplexity.Pcp.pcpOn_iff_cert (A : Type) [FirstOrder.Language.pcp.Structure A] [Finite A] : PcpOn A ↔ ∃ (n : ℕ) (c : Cert A (Fin n)), CertOK c

A Post system has a match exactly when a finite certificate says so. The certificate invents a segment of slots and nothing else: the common word, whose length no function of the instance bounds, is never written down – only the matching between the two ways of cutting it into blocks is.