Cookies disclaimer

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.

[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.

Task 1

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 |

Task 2

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

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

Task 3

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

Download Files

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"


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

Template File

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

Check File

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

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

Template File

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

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

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

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

Terms and Conditions