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