PCP: Post's correspondence problem

Given a list of pairs of words, is there a nonempty sequence of them whose top words and whose bottom words have the same concatenation? (Post 1946) This file carries the instance encoding – a list of domino pairs, presented as a finite structure – and its semantics; membership in RE lives in the sibling files.

The encoding

The elements of an instance play three roles at once – dominoes, letters, and positions inside a word – and, as in DescriptiveComplexity.FINSAT, nothing forces those roles to be disjoint:

• dom marks the dominoes: a solution is a sequence of marked elements, so everything outside dom is junk that the semantics never reads;
• uAt d p c says that the top word of the domino d carries the letter c at the position p, and vAt the same for its bottom word;
• le is a linear order on the instance. A word is a string, so an encoding of one may certainly carry the order of its own positions; there is nothing else a position could be, and the semantics has to read the order to know in which order the letters of a word come.

The positions carrying the letters of a word are not required to form an initial segment of the order: the word of d is the sequence of its letters at the positions used, whichever those are. A partial map from a finite linear order to letters already is a word, canonically, so the extra condition would be one more thing to check and to establish for the image of a reduction, and would buy nothing.

The semantics

DescriptiveComplexity.DecisionProblem.Holds is a predicate on every type, finite or not, so the word of a domino may not be defined by sorting a Finset of the universe. Instead the enumeration of the positions is an existential: DescriptiveComplexity.Pcp.IsWordU d w says that some strictly increasing list enumerates exactly the positions used by the top word of d and that w carries the letters at them. Such a list is unique when it exists (two sorted duplicate-free lists with the same members are equal), so IsWordU d holds of at most one list, and it holds of one as soon as the used positions are finite. The problem is then Post's on the nose (DescriptiveComplexity.Pcp.PcpOn): a nonempty sequence of marked dominoes whose top words and bottom words have the same concatenation.

What is and is not claimed

RE is the logically defined class of DescriptiveComplexity.RecursivelyEnumerable (definability in ∃SO[new]), so membership of PCP in it is a statement about that logic. RE-hardness is the computation-history dominoes from the halting problem (DescriptiveComplexity.halt_ordered_fo_reduction_pcp, in DescriptiveComplexity.Problems.Pcp.Hardness) – a machine construction of necessity, since unlike DescriptiveComplexity.FINSAT, PCP is not the syntactic image of any logic. Together the two halves make PCP RE-complete and Post's problem undecidable (DescriptiveComplexity.pcp_RE_complete, DescriptiveComplexity.pcp_not_computable, in DescriptiveComplexity.Computability.PcpComplete).

inductive FirstOrder.Language.pcpRel : ℕ → Type

Relation symbols of the language of Post correspondence systems.

• le : pcpRel 2

  le x y: the order of the positions.

• dom : pcpRel 1

  dom d: the element d is one of the dominoes.

• uAt : pcpRel 3

  uAt d p c: the top word of the domino d has the letter c at the position p.

• vAt : pcpRel 3

  vAt d p c: the bottom word of the domino d has the letter c at the position p.

def FirstOrder.Language.instDecidableEqPcpRel.decEq {a✝ : ℕ} (x✝ x✝¹ : pcpRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqPcpRel.decEq FirstOrder.Language.pcpRel.le FirstOrder.Language.pcpRel.le = isTrue FirstOrder.Language.instDecidableEqPcpRel.decEq._proof_1
• FirstOrder.Language.instDecidableEqPcpRel.decEq FirstOrder.Language.pcpRel.dom FirstOrder.Language.pcpRel.dom = isTrue FirstOrder.Language.instDecidableEqPcpRel.decEq._proof_2
• FirstOrder.Language.instDecidableEqPcpRel.decEq FirstOrder.Language.pcpRel.uAt FirstOrder.Language.pcpRel.uAt = isTrue FirstOrder.Language.instDecidableEqPcpRel.decEq._proof_3
• FirstOrder.Language.instDecidableEqPcpRel.decEq FirstOrder.Language.pcpRel.uAt FirstOrder.Language.pcpRel.vAt = isFalse FirstOrder.Language.instDecidableEqPcpRel.decEq._proof_4
• FirstOrder.Language.instDecidableEqPcpRel.decEq FirstOrder.Language.pcpRel.vAt FirstOrder.Language.pcpRel.uAt = isFalse FirstOrder.Language.instDecidableEqPcpRel.decEq._proof_5
• FirstOrder.Language.instDecidableEqPcpRel.decEq FirstOrder.Language.pcpRel.vAt FirstOrder.Language.pcpRel.vAt = isTrue FirstOrder.Language.instDecidableEqPcpRel.decEq._proof_6

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqPcpRel {a✝ : ℕ} : DecidableEq (pcpRel a✝)

Equations

• FirstOrder.Language.instDecidableEqPcpRel = FirstOrder.Language.instDecidableEqPcpRel.decEq

def FirstOrder.Language.pcp : Language

The relational vocabulary of Post correspondence systems: marked dominoes carrying two words each, over a universe ordered by the order of the positions of those words.

Equations

• FirstOrder.Language.pcp = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.pcpRel }

instance FirstOrder.Language.instIsRelationalPcp : Language.pcp.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.pcpLeSym : Language.pcp.Relations 2

The order symbol of the positions.

Equations

• FirstOrder.Language.pcpLeSym = FirstOrder.Language.pcpRel.le

@[reducible, inline]

abbrev FirstOrder.Language.pcpDomSym : Language.pcp.Relations 1

The symbol marking the dominoes.

Equations

• FirstOrder.Language.pcpDomSym = FirstOrder.Language.pcpRel.dom

@[reducible, inline]

abbrev FirstOrder.Language.pcpUSym : Language.pcp.Relations 3

The symbol giving the letters of the top words.

Equations

• FirstOrder.Language.pcpUSym = FirstOrder.Language.pcpRel.uAt

@[reducible, inline]

abbrev FirstOrder.Language.pcpVSym : Language.pcp.Relations 3

The symbol giving the letters of the bottom words.

Equations

• FirstOrder.Language.pcpVSym = FirstOrder.Language.pcpRel.vAt

Reading the encoding

def DescriptiveComplexity.Pcp.Ord {A : Type} [FirstOrder.Language.pcp.Structure A] (x y : A) : Prop

x precedes y in the order of the positions.

Equations

• DescriptiveComplexity.Pcp.Ord x y = FirstOrder.Language.Structure.RelMap FirstOrder.Language.pcpLeSym ![x, y]

def DescriptiveComplexity.Pcp.OrdLt {A : Type} [FirstOrder.Language.pcp.Structure A] (x y : A) : Prop

x strictly precedes y in the order of the positions.

Equations

• DescriptiveComplexity.Pcp.OrdLt x y = (DescriptiveComplexity.Pcp.Ord x y ∧ x ≠ y)

def DescriptiveComplexity.Pcp.DomG {A : Type} [FirstOrder.Language.pcp.Structure A] (d : A) : Prop

The element d is one of the dominoes.

Equations

• DescriptiveComplexity.Pcp.DomG d = FirstOrder.Language.Structure.RelMap FirstOrder.Language.pcpDomSym ![d]

def DescriptiveComplexity.Pcp.UAt {A : Type} [FirstOrder.Language.pcp.Structure A] (d p c : A) : Prop

The top word of the domino d has the letter c at the position p.

Equations

• DescriptiveComplexity.Pcp.UAt d p c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.pcpUSym ![d, p, c]

def DescriptiveComplexity.Pcp.VAt {A : Type} [FirstOrder.Language.pcp.Structure A] (d p c : A) : Prop

The bottom word of the domino d has the letter c at the position p.

Equations

• DescriptiveComplexity.Pcp.VAt d p c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.pcpVSym ![d, p, c]

def DescriptiveComplexity.Pcp.UsedU {A : Type} [FirstOrder.Language.pcp.Structure A] (d p : A) : Prop

The position p carries a letter of the top word of the domino d.

Equations

• DescriptiveComplexity.Pcp.UsedU d p = ∃ (c : A), DescriptiveComplexity.Pcp.UAt d p c

def DescriptiveComplexity.Pcp.UsedV {A : Type} [FirstOrder.Language.pcp.Structure A] (d p : A) : Prop

The position p carries a letter of the bottom word of the domino d.

Equations

• DescriptiveComplexity.Pcp.UsedV d p = ∃ (c : A), DescriptiveComplexity.Pcp.VAt d p c

Well-formedness

Little is required of an instance, and all of it is first-order: the order symbol is a linear order, and each of the two word relations is functional in the position. Functionality is the only shape condition, and it cannot be dispensed with – without it a “word” would carry a set of letters at some position rather than a letter, and the letters that the two concatenations of a solution must agree on would not be determined by the instance. Nothing is required of the dominoes: an element outside dom may carry whatever letters it likes, since no solution ever names it.

structure DescriptiveComplexity.Pcp.IsWF (A : Type) [FirstOrder.Language.pcp.Structure A] : Prop

Well-formedness of a Post correspondence system: the order symbol is a linear order, and each domino carries at most one letter at each position of each of its two words.

• ord_refl (x : A) : Ord x x

  The order of the positions is reflexive.

• ord_trans (x y z : A) : Ord x y → Ord y z → Ord x z

  The order of the positions is transitive.

• ord_antisymm (x y : A) : Ord x y → Ord y x → x = y

  The order of the positions is antisymmetric.

• ord_total (x y : A) : Ord x y ∨ Ord y x

  The order of the positions is total.

• uAt_fun (d p c c' : A) : UAt d p c → UAt d p c' → c = c'

  A top word has at most one letter at each position.

• vAt_fun (d p c c' : A) : VAt d p c → VAt d p c' → c = c'

  A bottom word has at most one letter at each position.

The words of a domino

The word of a domino is the sequence of its letters, read in the order of the positions carrying them. The enumeration of those positions is an existential rather than a construction, so that the definition needs no finiteness of the universe: a strictly increasing list whose members are exactly the used positions, together with the letters at them.

def DescriptiveComplexity.Pcp.IsWordU {A : Type} [FirstOrder.Language.pcp.Structure A] (d : A) (w : List A) : Prop

The top word of the domino d is w: some strictly increasing list enumerates exactly the positions used by the top word of d, and w carries the letters at them.

Equations

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

def DescriptiveComplexity.Pcp.IsWordV {A : Type} [FirstOrder.Language.pcp.Structure A] (d : A) (w : List A) : Prop

The bottom word of the domino d is w, as in DescriptiveComplexity.Pcp.IsWordU.

Equations

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

The problem

def DescriptiveComplexity.Pcp.PcpOn (A : Type) [FirstOrder.Language.pcp.Structure A] : Prop

The system has a match: the instance is well-formed and there is a nonempty sequence of dominoes whose top words and whose bottom words have the same concatenation.

Equations

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

Isomorphism-invariance

Everything the semantics reads is a relation of the instance, so an isomorphism transports it: the sequence of dominoes and the two lists of words are carried over by List.map, and the enumerations of the positions with them. Only one direction is proved; the converse is the same statement at the inverse isomorphism.

theorem DescriptiveComplexity.Pcp.ord_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (x y : A) : Ord x y ↔ Ord (e x) (e y)

theorem DescriptiveComplexity.Pcp.ordLt_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (x y : A) : OrdLt x y ↔ OrdLt (e x) (e y)

theorem DescriptiveComplexity.Pcp.domG_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d : A) : DomG d ↔ DomG (e d)

theorem DescriptiveComplexity.Pcp.uAt_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d p c : A) : UAt d p c ↔ UAt (e d) (e p) (e c)

theorem DescriptiveComplexity.Pcp.vAt_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d p c : A) : VAt d p c ↔ VAt (e d) (e p) (e c)

theorem DescriptiveComplexity.Pcp.usedU_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d p : A) : UsedU d p ↔ UsedU (e d) (e p)

theorem DescriptiveComplexity.Pcp.usedV_equiv {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d p : A) : UsedV d p ↔ UsedV (e d) (e p)

The same transports read backwards, at the inverse isomorphism: the shape every field of DescriptiveComplexity.Pcp.isWF_map needs.

theorem DescriptiveComplexity.Pcp.ord_equiv' {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (x y : B) : Ord x y ↔ Ord (e.symm x) (e.symm y)

theorem DescriptiveComplexity.Pcp.uAt_equiv' {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d p c : B) : UAt d p c ↔ UAt (e.symm d) (e.symm p) (e.symm c)

theorem DescriptiveComplexity.Pcp.vAt_equiv' {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (d p c : B) : VAt d p c ↔ VAt (e.symm d) (e.symm p) (e.symm c)

theorem DescriptiveComplexity.Pcp.isWF_map {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (h : IsWF A) : IsWF B

Well-formedness transports along an isomorphism.

Transporting lists

Two small facts about lists, stated for arbitrary relations because the words and the sequence of dominoes need them at four different instances: a sorted list stays sorted under a map preserving the order, and List.Forall₂ is functorial.

theorem DescriptiveComplexity.Pcp.pairwise_map_of {α β : Type} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (hf : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} : List.Pairwise R l → List.Pairwise S (List.map f l)

theorem DescriptiveComplexity.Pcp.forall₂_map_map {α β γ δ : Type} {R : α → β → Prop} {S : γ → δ → Prop} (f : α → γ) (g : β → δ) (hfg : ∀ (a : α) (b : β), R a b → S (f a) (g b)) {l₁ : List α} {l₂ : List β} : List.Forall₂ R l₁ l₂ → List.Forall₂ S (List.map f l₁) (List.map g l₂)

theorem DescriptiveComplexity.Pcp.isWordU_map {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) {d : A} {w : List A} (h : IsWordU d w) : IsWordU (e d) (List.map (⇑e) w)

The top word of a domino transports along an isomorphism.

theorem DescriptiveComplexity.Pcp.isWordV_map {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) {d : A} {w : List A} (h : IsWordV d w) : IsWordV (e d) (List.map (⇑e) w)

The bottom word of a domino transports along an isomorphism.

theorem DescriptiveComplexity.Pcp.pcpOn_map {A B : Type} [FirstOrder.Language.pcp.Structure A] [FirstOrder.Language.pcp.Structure B] (e : FirstOrder.Language.pcp.Equiv A B) (h : PcpOn A) : PcpOn B

The problem transports along an isomorphism (one direction; the converse is this statement at e.symm).

def DescriptiveComplexity.PCP : DecisionProblem FirstOrder.Language.pcp

PCP: Post's correspondence problem – has this list of domino pairs a match? (Post 1946) The second problem of the catalog whose certificate is unbounded in the instance, and the first whose certificate is a sequence rather than a structure.

Equations

• DescriptiveComplexity.PCP = { Holds := fun (A : Type) (x : FirstOrder.Language.pcp.Structure A) => DescriptiveComplexity.Pcp.PcpOn A, iso_invariant := @DescriptiveComplexity.PCP._proof_1 }