Lax251941.PostCorrespondence

The Post correspondence problem

concepts/Lax251941/PostCorrespondence.lean · lax-251941

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

An instance of the Post correspondence problem is a finite collection of dominos $[t / b]$ , each carrying a top string $t$ and a bottom string $b$ over some alphabet. A match is a nonempty sequence of dominos from the collection, repetitions allowed, such that reading off the top strings gives the same string as reading off the bottom strings. The problem asks whether a given instance has a match (Sipser, Section 5.2; Post 1946).

The same problem in index form, as the book Transducers uses it: an instance is a finite list of pairs of strings $(u_1, v_1), \ldots, (u_n, v_n)$ over the alphabet $\mathbb{N}$ , and it is solvable if some nonempty sequence of indices $i_1 \cdots i_k$ satisfies

u_{i_1} \cdots u_{i_k} = v_{i_1} \cdots v_{i_k}.

Lean source view on GitHub

1	import Mathlib.Data.List.Basic
2
3	/-!
4	---
5	title: The Post correspondence problem
6	type: definition
7	---
8	An instance of the Post correspondence problem is a finite collection of
9	dominos $[t / b]$ , each carrying a top string $t$ and a bottom string $b$ over
10	some alphabet. A match is a nonempty sequence of dominos from the collection,
11	repetitions allowed, such that reading off the top strings gives the same string
12	as reading off the bottom strings. The problem asks whether a given instance has
13	a match (Sipser, Section 5.2; Post 1946).
14
15	The same problem in index form, as the book Transducers uses it: an
16	instance is a finite list of pairs of strings $(u_1, v_1), \ldots, (u_n, v_n)$
17	over the alphabet $\mathbb{N}$ , and it is solvable if some nonempty sequence of
18	indices $i_1 \cdots i_k$ satisfies
19	$u_{i_1} \cdots u_{i_k} = v_{i_1} \cdots v_{i_k}.$
20
21	# Formalization notes
22
23	`Inst α` is a list of dominos over any alphabet `α`; `IsMatch P s` says that the
24	nonempty list `s` of dominos, each belonging to `P`, has equal top and bottom
25	strings, and `HasMatch P` that some match exists. `Solvable` is the index form
26	over `ℕ`: `conc ws idx` concatenates the strings of `ws` selected by the indices
27	(an index out of range selects the empty string, but the definition requires
28	every index to be in range). The two forms carry the same information — choose
29	an index for each domino, or read a domino off each index — and both are stated
30	as undecidable.
31	-/
32
33	namespace Lax251941.PostCorrespondence
34
35	/-- A domino: a top string and a bottom string. -/
36	abbrev Domino (α : Type*) := List α × List α
37
38	/-- An instance of the Post correspondence problem: a finite list of dominos. -/
39	abbrev Inst (α : Type*) := List (Domino α)
40
41	/-- The string read off the top halves of a sequence of dominos. -/
42	def topStr {α : Type*} (s : List (Domino α)) : List α := (s.map Prod.fst).flatten
43
44	/-- The string read off the bottom halves of a sequence of dominos. -/
45	def botStr {α : Type*} (s : List (Domino α)) : List α := (s.map Prod.snd).flatten
46
47	/-- `s` is a match of the instance `P`: a nonempty sequence of dominos of `P`
48	whose top string equals its bottom string. -/
49	def IsMatch {α : Type*} (P : Inst α) (s : List (Domino α)) : Prop :=
50	s ≠ [] ∧ (∀ d ∈ s, d ∈ P) ∧ topStr s = botStr s
51
52	/-- The instance `P` has a match. -/
53	def HasMatch {α : Type*} (P : Inst α) : Prop := ∃ s, IsMatch P s
54
55	/-- An instance in index form: a finite list of pairs of strings over `ℕ`. -/
56	abbrev Instance := List (List ℕ × List ℕ)
57
58	/-- The concatenation of the strings of `ws` selected by a list of indices. -/
59	def conc (ws : List (List ℕ)) (idx : List ℕ) : List ℕ :=
60	(idx.map (fun i => ws.getD i [])).flatten
61
62	/-- An instance is solvable if some nonempty sequence of indices makes the two
63	concatenations equal. -/
64	def Solvable (P : Instance) : Prop :=
65	∃ idx : List ℕ, idx ≠ [] ∧ (∀ i ∈ idx, i < P.length) ∧
66	conc (P.map Prod.fst) idx = conc (P.map Prod.snd) idx
67
68	end Lax251941.PostCorrespondence
69

Formalization notes

$Inst α$ is a list of dominos over any alphabet $α$ ; $IsMatch P s$ says that the nonempty list $s$ of dominos, each belonging to $P$ , has equal top and bottom strings, and $HasMatch P$ that some match exists. $Solvable$ is the index form over $ℕ$ : $conc ws idx$ concatenates the strings of $ws$ selected by the indices (an index out of range selects the empty string, but the definition requires every index to be in range). The two forms carry the same information — choose an index for each domino, or read a domino off each index — and both are stated as undecidable.

Builds on

none

Used by

From Mathlib

Mathlib.Data.List.Basic

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

The Post correspondence problem

Flags

Flag this concept