I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

The Post correspondence problem (PCP) is a well-known undecidable problem with a very simple definition. We are given a number of cards with two strings, one in the upper half of the card and one in the lower half. We are allowed to use as many instances of each card as we want. The question is, can we arrange a sequence of cards in such a way that the strings in the upper and the lower half of the arrangement match? Such an arrangement is called a solution of the PCP and can be given as a sequence of card indices.

Show that all solutions for the following instance can be described by the regex `(0 | 21)+`

.

```
0: 1: 2:
|d| |d | |abc|
|d| |cd| |ab |
```

Show that the following problem instance does not have a solution.

```
0: 1: 2:
|ab | |baa| |aba|
|aba| |aa | |baa|
```

Show that the PCP is trivially decidable if we restrict the alphabet to a single letter. That is, prove that there is a solution if and only if there exist a card whose upper half is as least as long as its lower half and a card for which it is the other way round.

[Thanks to the problem author Simon Wimmer, and the translators Kevin Kappelmann (Lean) and Anton Trunov (Coq).]

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin paragraph ‹Definition of PCP› type_synonym 'a pcp = "('a list × 'a list) list" definition is_solution :: "'a pcp ⇒ nat list ⇒ bool" where "is_solution pcp xs ≡ xs ≠ [] ∧ set xs ⊆ {0..<length pcp} ∧ concat (map (fst o nth pcp) xs) = concat (map (snd o nth pcp) xs)" definition "has_solution pcp ≡ ∃xs. is_solution pcp xs" paragraph ‹Task 1› definition "pcp1 ≡ [(''d'', ''d''), (''d'', ''cd''), (''abc'', ''ab'')]" paragraph ‹Task 2› definition "pcp2 ≡ [(''ab'', ''aba''), (''baa'', ''aa''), (''aba'', ''baa'')]" paragraph ‹Task 3› definition "is_valid pcp ≡ ∀(a, b) ∈ set pcp. a ≠ [] ∧ b ≠ []" end

theory Template imports Defs begin paragraph ‹Task 1› theorem task1: "is_solution pcp1 xs ⟷ (∃xxs. xs ≠ [] ∧ concat xxs = xs ∧ set xxs ⊆ {[0], [2, 1]})" sorry paragraph ‹Task 2› theorem task2: "¬ has_solution pcp2" sorry paragraph ‹Task 3› theorem task3: assumes "is_valid pcp" "∀(x,y) ∈ set pcp. set x = {a} ∧ set y = {a}" shows "has_solution pcp ⟷ (∃ (x1, y1) ∈ set pcp. ∃ (x2, y2) ∈ set pcp. length x1 ≥ length y1 ∧ length x2 ≤ length y2)" sorry end

theory Check imports Submission begin theorem task1: "is_solution pcp1 xs ⟷ (∃xxs. xs ≠ [] ∧ concat xxs = xs ∧ set xxs ⊆ {[0], [2, 1]})" by (rule Submission.task1) theorem task2: "¬ has_solution pcp2" by (rule Submission.task2) theorem task3: assumes "is_valid pcp" "∀(x,y) ∈ set pcp. set x = {a} ∧ set y = {a}" shows "has_solution pcp ⟷ (∃ (x1, y1) ∈ set pcp. ∃ (x2, y2) ∈ set pcp. length x1 ≥ length y1 ∧ length x2 ≤ length y2)" using assms by (rule Submission.task3) end

Download Files
### Definitions File

### Template File

From Coq Require Export List. Export ListNotations. Definition subset {A} (xs ys : list A) : Prop := forall x, In x xs -> In x ys. (** Definition of PCP *) Definition pcp (A : Type) := list (list A * list A). Definition is_solution {A : Type} (pcp : pcp A) (xs : list nat) : Prop := xs <> [] /\ (forall x, In x xs -> x < length pcp) /\ flat_map (fun i => fst (nth i pcp ([],[]))) xs = flat_map (fun i => snd (nth i pcp ([],[]))) xs. Definition has_solution {A} (pcp : pcp A) := exists xs, is_solution pcp xs. From Coq Require String Ascii. Open Scope string_scope. Import String Ascii. Section Util. Fixpoint explode (s : string) : list ascii := match s with | EmptyString => [] | String ch rest => ch :: explode rest end. End Util. (** Task 1 *) Definition pcp1 := map (fun '(s, t) => (explode s, explode t)) [("d", "d"); ("d", "cd"); ("abc", "ab")]. (** Task 2 *) Definition pcp2 := map (fun '(s, t) => (explode s, explode t)) [("ab", "aba"); ("baa", "aa"); ("aba", "baa")]. (** Task 3 *) Definition is_valid {A} (pcp : pcp A) := forall a b, In (a,b) pcp -> a <> [] /\ b <> [].

From Coq Require Import List Ascii Arith. Require Import Defs. Open Scope char_scope. (** Task 1 *) Theorem task1 xs : is_solution pcp1 xs <-> exists xss, xs <> [] /\ concat xss = xs /\ subset xss [[0]; [2; 1]]. Proof. Admitted. (** Task 2 *) Theorem task2: ~ has_solution pcp2. Proof. Admitted. (** Task 3 *) Theorem task3 A pcp (a : A) : is_valid pcp -> (forall xs ys, In (xs,ys) pcp -> (forall x, In x xs -> x = a) /\ (forall y, In y ys -> y = a)) -> has_solution pcp <-> exists x1 y1 x2 y2, In (x1, y1) pcp /\ In (x2, y2) pcp /\ length x1 >= length y1 /\ length x2 <= length y2. Proof. Admitted.

Download Files
### Definitions File

### Template File

### Check File

-- Lean version: 3.4.2 -- Mathlib version: 2019-07-31 abbreviation pcp (α : Type*) := list (list α × list α) namespace pcp variable {α : Type*} def is_solution (p : pcp α) (l : list $ fin p.length) : Prop := l ≠ [] ∧ list.join (l.map (λ n, (p.nth_le _ n.is_lt).fst)) = list.join (l.map (λ n, (p.nth_le _ n.is_lt).snd)) def has_solution (p : pcp α) : Prop := ∃ l, p.is_solution l def non_empty_cards (p : pcp α) : Prop := ∀ (a b : list α), (a, b) ∈ p → a ≠ [] ∧ b ≠ [] end pcp def pcp1 : pcp char := [ ( ['d'], ['d'] ), ( ['d'], ['c', 'd'] ), ( ['a', 'b', 'c'], ['a', 'b'] ) ] def pcp2 : pcp char := [ ( ['a', 'b'], ['a', 'b', 'a'] ), ( ['b', 'a', 'a'], ['a', 'a'] ), ( ['a', 'b', 'a'], ['b', 'a', 'a'] ) ] def pcp3 : pcp char := [ ( ['a', 'b'], ['a', 'b', 'a'] ), ( ['b', 'a', 'a'], ['a', 'a'] ), ( ['a', 'b', 'a'], ['b', 'a', 'a'] ) ]

import logic.unique import .defs theorem task1 : ∀ l, pcp1.is_solution l ↔ l ≠ [] ∧ ∃ l', list.join l' = l ∧ l'.map (list.map fin.val) ⊆ {[0], [2, 1]} := sorry theorem task2 : ¬pcp2.has_solution := sorry theorem task3 {α : Type*} [unique α] {p : pcp α} (non_empty_cards : p.non_empty_cards) : p.has_solution ↔ ∃ (a1 b1 a2 b2 : list α), (a1, b1) ∈ p ∧ (a2, b2) ∈ p ∧ a1.length ≥ b1.length ∧ a2.length ≤ b2.length := sorry

import logic.unique import .defs import .submission theorem goal1 : ∀ l, pcp1.is_solution l ↔ l ≠ [] ∧ ∃ l', list.join l' = l ∧ l'.map (list.map fin.val) ⊆ {[0], [2, 1]} := task1 theorem goal2 : ¬pcp2.has_solution := task2 theorem goal3 {α : Type*} [unique α] {p : pcp α} (non_empty_cards : p.non_empty_cards) : p.has_solution ↔ ∃ (a1 b1 a2 b2 : list α), (a1, b1) ∈ p ∧ (a2, b2) ∈ p ∧ a1.length ≥ b1.length ∧ a2.length ≤ b2.length := task3 non_empty_cards

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin paragraph ‹Definition of PCP› type_synonym 'a pcp = "('a list × 'a list) list" definition is_solution :: "'a pcp ⇒ nat list ⇒ bool" where "is_solution pcp xs ≡ xs ≠ [] ∧ set xs ⊆ {0..<length pcp} ∧ concat (map (fst o nth pcp) xs) = concat (map (snd o nth pcp) xs)" definition "has_solution pcp ≡ ∃xs. is_solution pcp xs" paragraph ‹Task 1› definition "pcp1 ≡ [(''d'', ''d''), (''d'', ''cd''), (''abc'', ''ab'')]" paragraph ‹Task 2› definition "pcp2 ≡ [(''ab'', ''aba''), (''baa'', ''aa''), (''aba'', ''baa'')]" paragraph ‹Task 3› definition "is_valid pcp ≡ ∀(a, b) ∈ set pcp. a ≠ [] ∧ b ≠ []" end

theory Template imports Defs begin paragraph ‹Task 1› theorem task1: "is_solution pcp1 xs ⟷ (∃xxs. xs ≠ [] ∧ concat xxs = xs ∧ set xxs ⊆ {[0], [2, 1]})" sorry paragraph ‹Task 2› theorem task2: "¬ has_solution pcp2" sorry paragraph ‹Task 3› theorem task3: assumes "is_valid pcp" "∀(x,y) ∈ set pcp. set x = {a} ∧ set y = {a}" shows "has_solution pcp ⟷ (∃ (x1, y1) ∈ set pcp. ∃ (x2, y2) ∈ set pcp. length x1 ≥ length y1 ∧ length x2 ≤ length y2)" sorry end

theory Check imports Submission begin theorem task1: "is_solution pcp1 xs ⟷ (∃xxs. xs ≠ [] ∧ concat xxs = xs ∧ set xxs ⊆ {[0], [2, 1]})" by (rule Submission.task1) theorem task2: "¬ has_solution pcp2" by (rule Submission.task2) theorem task3: assumes "is_valid pcp" "∀(x,y) ∈ set pcp. set x = {a} ∧ set y = {a}" shows "has_solution pcp ⟷ (∃ (x1, y1) ∈ set pcp. ∃ (x2, y2) ∈ set pcp. length x1 ≥ length y1 ∧ length x2 ≤ length y2)" using assms by (rule Submission.task3) end

Terms and Conditions