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.

# [2019-Aug] PCP

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).]

## Resources

### Definitions 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"

definition
"pcp1 ≡ [(''d'', ''d''), (''d'', ''cd''), (''abc'', ''ab'')]"

definition
"pcp2 ≡ [(''ab'', ''aba''), (''baa'', ''aa''), (''aba'', ''baa'')]"

definition
"is_valid pcp ≡ ∀(a, b) ∈ set pcp. a ≠ [] ∧ b ≠ []"

end```

### Template File

```theory Template
imports Defs
begin

"is_solution pcp1 xs ⟷ (∃xxs. xs ≠ [] ∧ concat xxs = xs ∧ set xxs ⊆ {[0], [2, 1]})"
sorry

"¬ has_solution pcp2"
sorry

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```

### Check File

```theory Check
imports Submission
begin

"is_solution pcp1 xs ⟷ (∃xxs. xs ≠ [] ∧ concat xxs = xs ∧ set xxs ⊆ {[0], [2, 1]})"

"¬ has_solution pcp2"

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)"

end```

### Definitions 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.

Definition
pcp1 := map (fun '(s, t) => (explode s, explode t))
[("d", "d"); ("d", "cd"); ("abc", "ab")].

Definition
pcp2 := map (fun '(s, t) => (explode s, explode t))
[("ab", "aba"); ("baa", "aa"); ("aba", "baa")].

Definition
is_valid {A} (pcp : pcp A) := forall a b, In (a,b) pcp -> a <> [] /\ b <> [].```

### Template File

```From Coq Require Import List Ascii Arith.
Require Import Defs.
Open Scope char_scope.

is_solution pcp1 xs <->
exists xss, xs <> [] /\ concat xss = xs /\ subset xss [[0]; [2; 1]].
Proof.

~ has_solution pcp2.
Proof.

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.

### Definitions 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']
)
]```

### Template File

```import logic.unique
import .defs

∀ l, pcp1.is_solution l
↔ l ≠ [] ∧ ∃ l', list.join l' = l ∧ l'.map (list.map fin.val) ⊆ {[0], [2, 1]} :=
sorry

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```

### Check File

```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]} :=