Post's correspondence problem
Lax624099.PostCorrespondence · concepts/Lax624099/PostCorrespondence.lean · lax-624099
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A Post correspondence system is a finite structure whose elements are dominoes, letters and positions at once: a unary relation marks the dominoes, two ternary relations give the letter of the top word and of the bottom word of a domino at a position, and a binary relation is a linear order on the positions. The top word of a domino is the sequence of its letters at the positions it uses, in the order of the positions, and likewise the bottom word. The system has a match when it is well-formed and some nonempty sequence of dominoes has the same concatenation of top words and of bottom words, the problem of Post (1946). PCP is the decision problem of the structures isomorphic to a system with a match.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.List.Forall2 |
| 2 | import Mathlib.ModelTheory.Semantics |
| 3 | import Mathlib.ModelTheory.Complexity |
| 4 | import Mathlib.Tactic.FinCases |
| 5 | import Lax904597.Classes |
| 6 | import Lax624099.Problems |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Post's correspondence problem |
| 11 | type: definition |
| 12 | --- |
| 13 | A Post correspondence system is a finite structure whose elements are |
| 14 | dominoes, letters and positions at once: a unary relation marks the |
| 15 | dominoes, two ternary relations give the letter of the top word and of the |
| 16 | bottom word of a domino at a position, and a binary relation is a linear |
| 17 | order on the positions. The top word of a domino is the sequence of its |
| 18 | letters at the positions it uses, in the order of the positions, and |
| 19 | likewise the bottom word. The system has a match when it is well-formed and |
| 20 | some nonempty sequence of dominoes has the same concatenation of top words |
| 21 | and of bottom words, the problem of Post (1946). PCP is the decision problem of the structures |
| 22 | isomorphic to a system with a match. |
| 23 | -/ |
| 24 | |
| 25 | namespace Lax624099.PostCorrespondence |
| 26 | |
| 27 | open FirstOrder |
| 28 | |
| 29 | open FirstOrder.Language |
| 30 | |
| 31 | /-- Relation symbols of the language of Post correspondence systems. -/ |
| 32 | inductive pcpRel : ℕ → Type |
| 33 | /-- `le x y`: the order of the positions. -/ |
| 34 | | le : pcpRel 2 |
| 35 | /-- `dom d`: the element `d` is one of the dominoes. -/ |
| 36 | | dom : pcpRel 1 |
| 37 | /-- `uAt d p c`: the top word of the domino `d` has the letter `c` at the |
| 38 | position `p`. -/ |
| 39 | | uAt : pcpRel 3 |
| 40 | /-- `vAt d p c`: the bottom word of the domino `d` has the letter `c` at the |
| 41 | position `p`. -/ |
| 42 | | vAt : pcpRel 3 |
| 43 | deriving DecidableEq |
| 44 | |
| 45 | /-- The relational vocabulary of Post correspondence systems: marked dominoes |
| 46 | carrying two words each, over a universe ordered by the order of the positions |
| 47 | of those words. -/ |
| 48 | def pcp : Language := |
| 49 | ⟨fun _ => Empty, pcpRel⟩ |
| 50 | |
| 51 | instance instIsRelationalPcp : IsRelational pcp := |
| 52 | fun _ => ⟨fun f => Empty.elim f⟩ |
| 53 | |
| 54 | /-- The order symbol of the positions. -/ |
| 55 | abbrev pcpLeSym : pcp.Relations 2 := .le |
| 56 | |
| 57 | /-- The symbol marking the dominoes. -/ |
| 58 | abbrev pcpDomSym : pcp.Relations 1 := .dom |
| 59 | |
| 60 | /-- The symbol giving the letters of the top words. -/ |
| 61 | abbrev pcpUSym : pcp.Relations 3 := .uAt |
| 62 | |
| 63 | /-- The symbol giving the letters of the bottom words. -/ |
| 64 | abbrev pcpVSym : pcp.Relations 3 := .vAt |
| 65 | |
| 66 | open FirstOrder |
| 67 | |
| 68 | open Language Structure |
| 69 | |
| 70 | namespace Pcp |
| 71 | |
| 72 | section Reading |
| 73 | |
| 74 | variable {A : Type} [pcp.Structure A] |
| 75 | |
| 76 | /-- `x` precedes `y` in the order of the positions. -/ |
| 77 | def Ord (x y : A) : Prop := RelMap pcpLeSym ![x, y] |
| 78 | |
| 79 | /-- `x` strictly precedes `y` in the order of the positions. -/ |
| 80 | def OrdLt (x y : A) : Prop := Ord x y ∧ x ≠ y |
| 81 | |
| 82 | /-- The element `d` is one of the dominoes. -/ |
| 83 | def DomG (d : A) : Prop := RelMap pcpDomSym ![d] |
| 84 | |
| 85 | /-- The top word of the domino `d` has the letter `c` at the position `p`. -/ |
| 86 | def UAt (d p c : A) : Prop := RelMap pcpUSym ![d, p, c] |
| 87 | |
| 88 | /-- The bottom word of the domino `d` has the letter `c` at the position |
| 89 | `p`. -/ |
| 90 | def VAt (d p c : A) : Prop := RelMap pcpVSym ![d, p, c] |
| 91 | |
| 92 | /-- The position `p` carries a letter of the top word of the domino `d`. -/ |
| 93 | def UsedU (d p : A) : Prop := ∃ c, UAt d p c |
| 94 | |
| 95 | /-- The position `p` carries a letter of the bottom word of the domino `d`. -/ |
| 96 | def UsedV (d p : A) : Prop := ∃ c, VAt d p c |
| 97 | |
| 98 | end Reading |
| 99 | |
| 100 | /-- **Well-formedness of a Post correspondence system**: the order symbol is a |
| 101 | linear order, and each domino carries at most one letter at each position of |
| 102 | each of its two words. -/ |
| 103 | structure IsWF (A : Type) [pcp.Structure A] : Prop where |
| 104 | /-- The order of the positions is reflexive. -/ |
| 105 | ord_refl : ∀ x : A, Ord x x |
| 106 | /-- The order of the positions is transitive. -/ |
| 107 | ord_trans : ∀ x y z : A, Ord x y → Ord y z → Ord x z |
| 108 | /-- The order of the positions is antisymmetric. -/ |
| 109 | ord_antisymm : ∀ x y : A, Ord x y → Ord y x → x = y |
| 110 | /-- The order of the positions is total. -/ |
| 111 | ord_total : ∀ x y : A, Ord x y ∨ Ord y x |
| 112 | /-- A top word has at most one letter at each position. -/ |
| 113 | uAt_fun : ∀ d p c c' : A, UAt d p c → UAt d p c' → c = c' |
| 114 | /-- A bottom word has at most one letter at each position. -/ |
| 115 | vAt_fun : ∀ d p c c' : A, VAt d p c → VAt d p c' → c = c' |
| 116 | |
| 117 | section Words |
| 118 | |
| 119 | variable {A : Type} [pcp.Structure A] |
| 120 | |
| 121 | /-- **The top word of the domino `d` is `w`**: some strictly increasing list |
| 122 | enumerates exactly the positions used by the top word of `d`, and `w` carries |
| 123 | the letters at them. -/ |
| 124 | def IsWordU (d : A) (w : List A) : Prop := |
| 125 | ∃ ps : List A, ps.Pairwise OrdLt ∧ (∀ p, p ∈ ps ↔ UsedU d p) ∧ List.Forall₂ (UAt d) ps w |
| 126 | |
| 127 | /-- **The bottom word of the domino `d` is `w`**, as in |
| 128 | `DescriptiveComplexity.Pcp.IsWordU`. -/ |
| 129 | def IsWordV (d : A) (w : List A) : Prop := |
| 130 | ∃ ps : List A, ps.Pairwise OrdLt ∧ (∀ p, p ∈ ps ↔ UsedV d p) ∧ List.Forall₂ (VAt d) ps w |
| 131 | |
| 132 | end Words |
| 133 | |
| 134 | /-- **The system has a match**: the instance is well-formed and there is a |
| 135 | nonempty sequence of dominoes whose top words and whose bottom words have the |
| 136 | same concatenation. -/ |
| 137 | def PcpOn (A : Type) [pcp.Structure A] : Prop := |
| 138 | IsWF A ∧ ∃ (l : List A) (us vs : List (List A)), |
| 139 | l ≠ [] ∧ (∀ d ∈ l, DomG d) ∧ |
| 140 | List.Forall₂ IsWordU l us ∧ List.Forall₂ IsWordV l vs ∧ us.flatten = vs.flatten |
| 141 | |
| 142 | end Pcp |
| 143 | |
| 144 | open Lax904597.Problems Lax624099.Problems |
| 145 | |
| 146 | /-- PCP: does the Post correspondence system have a match? -/ |
| 147 | def PCP : DecisionProblem pcp := |
| 148 | DecisionProblem.ofPred Pcp.PcpOn |
| 149 | |
| 150 | end Lax624099.PostCorrespondence |
| 151 |
Builds on
Used by
Lax624099.CodeHaltingInvarianceLax624099.CodehaltRECompleteLax624099.FiniteSatisfiabilityInvarianceLax624099.FinsatRECompleteLax624099.HaltingInvarianceLax624099.HaltingUndecidableLax624099.HaltRECompleteLax624099.NPSubsetRELax624099.PcpRECompleteLax624099.PcpUndecidableLax624099.PostCorrespondenceInvarianceLax624099.REClosureLax624099.ReductionsComputableLax624099.REFiniteLax624099.REHardUndecidableLax624099.REIsRecursivelyEnumerableLax624099.RENeCoRELax624099.Trakhtenbrot
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments