Documentation

DescriptiveComplexity.Problems.Pcp.Hardness.History

Computation histories as dominoes #

The combinatorial core of the RE-hardness of DescriptiveComplexity.PCP: a string-rewriting system has a derivation from its start word to the halting word exactly when a certain list of domino pairs has a match. Nothing here mentions a structure or a formula – the first-order side reads this file's DescriptiveComplexity.Pcp.History.HasMatch off an instance.

The system #

A rewriting system is a relation Rule between words over an alphabet Γ; one step (DescriptiveComplexity.Pcp.History.Step) replaces a left-hand side by a right-hand side somewhere in the word, and DescriptiveComplexity.Pcp.History.Derives is its reflexive-transitive closure. The question the dominoes answer is whether the start word C₀ derives the one-letter word [halt].

The dominoes, and the two things the construction has to arrange #

A match is read left to right as a queue: the unmatched overhang is a word, each domino consumes its top from the front of the overhang and appends its bottom at the back, and the whole history ⊳C₀#C₁#…#Cₙ# is spelt out by the bottom words one configuration ahead of the top words. Two things have to be arranged for that reading to be forced.

The match must start with the start domino. Every word is decorated (DescriptiveComplexity.Pcp.History.starL puts a star before each letter, DescriptiveComplexity.Pcp.History.starR after each), so every top begins with star and every bottom begins with a letter that is not star – except the start domino's, which begins with star as well. Since the first domino of a match has its two words beginning alike, it can only be that one. This is why every right-hand side of a rule is required to be nonempty (DescriptiveComplexity.Pcp.History.Ok): a domino with an empty bottom would escape the argument, and it is exactly the domino the undecorated construction needs to close the match. Here the closing domino swallows halt, the separator and the dia in one piece instead, and its bottom is the single letter dia.
The start domino must not reappear. Its top is the marker tri, which no other domino writes, so it can never be consumed again.

The alignment is then algebra: starL and starR are homomorphisms, and starL w ++ [star] = star :: starR w is the half-letter offset that makes the top and the bottom of a match spell the same word.

The decorated alphabet #

inductive DescriptiveComplexity.Pcp.History.Letter (Γ : Type) :

The alphabet of the domino words: the letters of the rewriting system, the separator between two configurations of a history, the decoration star, the marker tri opening a history and the marker dia closing a match.

sym {Γ : Type} : Γ → Letter Γ
A letter of the rewriting system.
sep {Γ : Type} : Letter Γ
The separator between two configurations.
star {Γ : Type} : Letter Γ
The decoration, which forces the alignment of a match.
tri {Γ : Type} : Letter Γ
The opening marker, which forces the first domino of a match.
dia {Γ : Type} : Letter Γ
The closing marker.

Instances For

Dependency graph

theorem DescriptiveComplexity.Pcp.History.absurd_of_ne {Γ : Type} {P : Prop} {a b : Letter Γ} (h : a = b) (hne : a ≠ b := by simp) :

P

Two different constructors of the alphabet are never equal; the shape in which the case analyses below need it.

Dependency graph

def DescriptiveComplexity.Pcp.History.symW {Γ : Type} (w : List Γ) :

List (Letter Γ)

A word of the rewriting system, as a word of the alphabet above.

Equations

DescriptiveComplexity.Pcp.History.symW w = List.map DescriptiveComplexity.Pcp.History.Letter.sym w

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.symW_nil {Γ : Type} :

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.symW_cons {Γ : Type} (a : Γ) (w : List Γ) :

symW (a :: w) = Letter.sym a :: symW w

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.symW_append {Γ : Type} (w w' : List Γ) :

symW (w ++ w') = symW w ++ symW w'

Dependency graph

theorem DescriptiveComplexity.Pcp.History.sep_not_mem_symW {Γ : Type} (w : List Γ) :

¬Letter.sep ∈ symW w

Dependency graph

def DescriptiveComplexity.Pcp.History.starL {Γ : Type} :

List (Letter Γ) → List (Letter Γ)

The word w decorated on the left: a star before each of its letters.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.starR {Γ : Type} :

List (Letter Γ) → List (Letter Γ)

The word w decorated on the right: a star after each of its letters.

Equations

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.starL_nil {Γ : Type} :

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.starL_cons {Γ : Type} (a : Letter Γ) (w : List (Letter Γ)) :

starL (a :: w) = Letter.star :: a :: starL w

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.starR_nil {Γ : Type} :

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.starR_cons {Γ : Type} (a : Letter Γ) (w : List (Letter Γ)) :

starR (a :: w) = a :: Letter.star :: starR w

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.starL_append {Γ : Type} (w w' : List (Letter Γ)) :

starL (w ++ w') = starL w ++ starL w'

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.starR_append {Γ : Type} (w w' : List (Letter Γ)) :

starR (w ++ w') = starR w ++ starR w'

Dependency graph

theorem DescriptiveComplexity.Pcp.History.starL_star {Γ : Type} (w : List (Letter Γ)) :

starL w ++ [Letter.star ] = Letter.star :: starR w

The half-letter offset: decorating on the left and closing with a star is decorating on the right and opening with one. This one identity is what makes the top and the bottom words of a match spell the same word.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.starL_prefix_cases {Γ : Type} (y z S S' : List (Letter Γ)) :

starL y ++ S = starL z ++ S' → (∃ (t : List (Letter Γ)), z = y ++ t ∧ S = starL t ++ S') ∨ ∃ (t : List (Letter Γ)), y = z ++ t ∧ starL t ++ S = S'

One decorated word is a prefix of the other. Two decorated words opening a common word are comparable, and the longer one continues with the decoration of the difference.

Dependency graph

The rewriting system #

def DescriptiveComplexity.Pcp.History.Step {Γ : Type} (Rule : List Γ → List Γ → Prop) (u v : List Γ) :

One rewriting step: a left-hand side of a rule, somewhere in the word, replaced by its right-hand side.

Equations

DescriptiveComplexity.Pcp.History.Step Rule u v = ∃ (x : List Γ), ∃ (l : List Γ), ∃ (r : List Γ), ∃ (y : List Γ), Rule l r ∧ u = x ++ l ++ y ∧ v = x ++ r ++ y

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.History.Derives {Γ : Type} (Rule : List Γ → List Γ → Prop) :

List Γ → List Γ → Prop

Derivability: any number of rewriting steps.

Equations

DescriptiveComplexity.Pcp.History.Derives Rule = Relation.ReflTransGen (DescriptiveComplexity.Pcp.History.Step Rule)

Instances For

Dependency graph

theorem DescriptiveComplexity.Pcp.History.Step.congr {Γ : Type} {Rule : List Γ → List Γ → Prop} {u v : List Γ} (h : Step Rule u v) (x y : List Γ) :

Step Rule (x ++ u ++ y) (x ++ v ++ y)

Dependency graph

theorem DescriptiveComplexity.Pcp.History.Derives.congr {Γ : Type} {Rule : List Γ → List Γ → Prop} {u v : List Γ} (h : Derives Rule u v) (x y : List Γ) :

Derives Rule (x ++ u ++ y) (x ++ v ++ y)

Dependency graph

inductive DescriptiveComplexity.Pcp.History.ParStep {Γ : Type} (Rule : List Γ → List Γ → Prop) :

List Γ → List Γ → Prop

Simultaneous rewriting: any number of rules applied at once, at disjoint places. It is what the dominoes between two separators perform, and it derives no more than one rule at a time does (DescriptiveComplexity.Pcp.History.ParStep.derives).

nil {Γ : Type} {Rule : List Γ → List Γ → Prop} : ParStep Rule [] []
The empty word rewrites to itself.
keep {Γ : Type} {Rule : List Γ → List Γ → Prop} (a : Γ) {u v : List Γ} : ParStep Rule u v → ParStep Rule (a :: u) (a :: v)
A letter may be kept.
rule {Γ : Type} {Rule : List Γ → List Γ → Prop} {l r u v : List Γ} : Rule l r → ParStep Rule u v → ParStep Rule (l ++ u) (r ++ v)
A rule may be applied.

Instances For

Dependency graph

theorem DescriptiveComplexity.Pcp.History.ParStep.derives {Γ : Type} {Rule : List Γ → List Γ → Prop} {u v : List Γ} (h : ParStep Rule u v) :

Derives Rule u v

Dependency graph

theorem DescriptiveComplexity.Pcp.History.ParStep.snoc_keep {Γ : Type} {Rule : List Γ → List Γ → Prop} {u v : List Γ} (h : ParStep Rule u v) (a : Γ) :

ParStep Rule (u ++ [a]) (v ++ [a])

Dependency graph

theorem DescriptiveComplexity.Pcp.History.ParStep.snoc_rule {Γ : Type} {Rule : List Γ → List Γ → Prop} {u v l r : List Γ} (h : ParStep Rule u v) (hr : Rule l r) :

ParStep Rule (u ++ l) (v ++ r)

Dependency graph

The dominoes #

inductive DescriptiveComplexity.Pcp.History.Dom (Γ : Type) :

A domino of the construction: the one that opens a history, one that copies a letter, one that copies a separator, one per rule, and the one that closes a match.

start {Γ : Type} : Dom Γ
Opens the history, writing the start word.
copy {Γ : Type} : Γ → Dom Γ
Copies a letter into the next configuration.
copySep {Γ : Type} : Dom Γ
Copies the separator between two configurations.
rule {Γ : Type} : List Γ → List Γ → Dom Γ
Applies a rule.
close {Γ : Type} : Dom Γ
Closes the match on the halting configuration.

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.Ok {Γ : Type} (Rule : List Γ → List Γ → Prop) :

Dom Γ → Prop

A domino belongs to the system: only its rule dominoes are constrained, and only by the rule they apply – whose two sides must be nonempty, so that no top and no bottom word is empty.

Equations

DescriptiveComplexity.Pcp.History.Ok Rule (DescriptiveComplexity.Pcp.History.Dom.rule l r) = (Rule l r ∧ l ≠ [] ∧ r ≠ [])
DescriptiveComplexity.Pcp.History.Ok Rule x✝ = True

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.topW {Γ : Type} (halt : Γ) :

Dom Γ → List (Letter Γ)

The top word of a domino.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.botW {Γ : Type} (C₀ : List Γ) :

Dom Γ → List (Letter Γ)

The bottom word of a domino.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.tops {Γ : Type} (halt : Γ) (l : List (Dom Γ)) :

List (Letter Γ)

The word spelt by the top of a list of dominoes.

Equations

DescriptiveComplexity.Pcp.History.tops halt l = (List.map (DescriptiveComplexity.Pcp.History.topW halt) l).flatten

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.bots {Γ : Type} (C₀ : List Γ) (l : List (Dom Γ)) :

List (Letter Γ)

The word spelt by the bottom of a list of dominoes.

Equations

DescriptiveComplexity.Pcp.History.bots C₀ l = (List.map (DescriptiveComplexity.Pcp.History.botW C₀) l).flatten

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.tops_nil {Γ : Type} (halt : Γ) :

tops halt [] = []

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.tops_cons {Γ : Type} (halt : Γ) (d : Dom Γ) (l : List (Dom Γ)) :

tops halt (d :: l) = topW halt d ++ tops halt l

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.bots_nil {Γ : Type} (C₀ : List Γ) :

bots C₀ [] = []

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.bots_cons {Γ : Type} (C₀ : List Γ) (d : Dom Γ) (l : List (Dom Γ)) :

bots C₀ (d :: l) = botW C₀ d ++ bots C₀ l

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.tops_append {Γ : Type} (halt : Γ) (l l' : List (Dom Γ)) :

tops halt (l ++ l') = tops halt l ++ tops halt l'

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.bots_append {Γ : Type} (C₀ : List Γ) (l l' : List (Dom Γ)) :

bots C₀ (l ++ l') = bots C₀ l ++ bots C₀ l'

Dependency graph

def DescriptiveComplexity.Pcp.History.HasMatch {Γ : Type} (Rule : List Γ → List Γ → Prop) (C₀ : List Γ) (halt : Γ) :

The system has a match: a nonempty list of its dominoes whose top words and whose bottom words spell the same word.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

From a derivation to a match #

The dominoes of one rewriting step copy the word on both sides of the rule and apply the rule in the middle, so they consume one configuration and its separator and write the next one and its separator. Chaining them writes the whole history; the start domino opens it and the closing domino swallows the last configuration.

def DescriptiveComplexity.Pcp.History.copies {Γ : Type} (w : List Γ) :

The dominoes copying a word letter by letter.

Equations

DescriptiveComplexity.Pcp.History.copies w = List.map DescriptiveComplexity.Pcp.History.Dom.copy w

Instances For

Dependency graph

theorem DescriptiveComplexity.Pcp.History.ok_copies {Γ : Type} {Rule : List Γ → List Γ → Prop} (w : List Γ) (d : Dom Γ) :

d ∈ copies w → Ok Rule d

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.tops_copies {Γ : Type} {halt : Γ} (w : List Γ) :

tops halt (copies w) = starL (symW w)

Dependency graph

@[simp]

theorem DescriptiveComplexity.Pcp.History.bots_copies {Γ : Type} {C₀ : List Γ} (w : List Γ) :

bots C₀ (copies w) = starR (symW w)

Dependency graph

theorem DescriptiveComplexity.Pcp.History.exists_block {Γ : Type} {Rule : List Γ → List Γ → Prop} {C₀ : List Γ} {halt : Γ} (hne : ∀ (l r : List Γ), Rule l r → l ≠ [] ∧ r ≠ []) {u v : List Γ} (h : Step Rule u v) :

∃ (ds : List (Dom Γ)), (∀ (d : Dom Γ), d ∈ ds → Ok Rule d) ∧ tops halt ds = starL (symW u ++ [Letter.sep ]) ∧ bots C₀ ds = starR (symW v ++ [Letter.sep ])

The dominoes of one step: they consume a configuration and its separator, and write the next configuration and its separator.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.exists_run {Γ : Type} {Rule : List Γ → List Γ → Prop} {C₀ : List Γ} {halt : Γ} (hne : ∀ (l r : List Γ), Rule l r → l ≠ [] ∧ r ≠ []) {u v : List Γ} (h : Derives Rule u v) :

∃ (ds : List (Dom Γ)), ∃ (T : List (Letter Γ)), ∃ (B : List (Letter Γ)), (∀ (d : Dom Γ), d ∈ ds → Ok Rule d) ∧ tops halt ds = starL T ∧ bots C₀ ds = starR B ∧ symW u ++ [Letter.sep ] ++ B = T ++ (symW v ++ [Letter.sep ])

The dominoes of a derivation: they consume every configuration but the last, and write every configuration but the first, so the word they consume and the word they write are the same history read one configuration apart.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.hasMatch_of_derives {Γ : Type} {Rule : List Γ → List Γ → Prop} {C₀ : List Γ} {halt : Γ} (hne : ∀ (l r : List Γ), Rule l r → l ≠ [] ∧ r ≠ []) (h : Derives Rule C₀ [halt]) :

HasMatch Rule C₀ halt

A derivation gives a match.

Dependency graph

From a match to a derivation #

A match is read as a queue: the overhang is a word β # γ, where β is what is left of the configuration being consumed and γ what has been written of the next one, and every domino takes its top off the front of the overhang and puts its bottom at the back. The invariant below says exactly that the queue belongs to a history, and each domino preserves it.

The top word of a domino is the decoration of the word it takes off the queue, followed by what it carries past the queue – nothing, except for the closing domino, which carries the two letters that end a match.

def DescriptiveComplexity.Pcp.History.topUW {Γ : Type} (halt : Γ) :

Dom Γ → List (Letter Γ)

The undecorated word a domino takes off the queue.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.Pcp.History.topRest {Γ : Type} :

Dom Γ → List (Letter Γ)

What a domino carries past the queue.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.Pcp.History.topW_eq {Γ : Type} (halt : Γ) (d : Dom Γ) :

topW halt d = starL (topUW halt d) ++ topRest d

Dependency graph

def DescriptiveComplexity.Pcp.History.Inv {Γ : Type} (Rule : List Γ → List Γ → Prop) (C₀ : List Γ) (z : List (Letter Γ)) :

The queue of a match belongs to a history: it is a configuration reached from the start word, cut in two by the separator, with the part before the cut still to be consumed and the part after it already rewritten.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

theorem DescriptiveComplexity.Pcp.History.sep_mem_queue {Γ : Type} (β γ : List Γ) :

Letter.sep ∈ symW β ++ [Letter.sep ] ++ symW γ

A queue carries a separator.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.mem_queue {Γ : Type} {c : Letter Γ} {β γ : List Γ} (h : c ∈ symW β ++ [Letter.sep ] ++ symW γ) :

c = Letter.sep ∨ ∃ (a : Γ), c = Letter.sym a

A queue carries nothing but letters of the system and the separator.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.prefix_of_align {Γ : Type} {z Y S S' : List (Letter Γ)} (h : starL z ++ S = starL Y ++ S') (hY : ∀ (t : List (Letter Γ)), Y = z ++ t → t = []) :

∃ (t : List (Letter Γ)), z = Y ++ t ∧ starL t ++ S = S'

The word a domino consumes is a prefix of the queue. A top word cannot run past the separator: the only word of the system reaching it is the one the closing domino consumes, and the queue is then exactly that word.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.no_ext_of_sep_notMem {Γ : Type} {Y z : List (Letter Γ)} (hsep : Letter.sep ∈ z) (hY : ¬Letter.sep ∈ Y) (t : List (Letter Γ)) :

Y = z ++ t → t = []

A word without a separator is no extension of a queue.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.topUW_no_ext {Γ : Type} {halt : Γ} {d : Dom Γ} {z : List (Letter Γ)} (hsep : Letter.sep ∈ z) (t : List (Letter Γ)) :

topUW halt d = z ++ t → t = []

No domino consumes more than the queue holds.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.symW_prefix {Γ : Type} {l : List Γ} {t : List (Letter Γ)} {β γ : List Γ} (h : symW l ++ t = symW β ++ [Letter.sep ] ++ symW γ) :

∃ (β' : List Γ), β = l ++ β' ∧ t = symW β' ++ [Letter.sep ] ++ symW γ

Dependency graph

theorem DescriptiveComplexity.Pcp.History.derives_of_align {Γ : Type} {Rule : List Γ → List Γ → Prop} {C₀ : List Γ} {halt : Γ} (l : List (Dom Γ)) (z : List (Letter Γ)) :

(∀ (d : Dom Γ), d ∈ l → Ok Rule d) → starL z ++ [Letter.star ] ++ bots C₀ l = tops halt l → Inv Rule C₀ z → Derives Rule C₀ [halt]

The queue lemma: a list of dominoes whose bottom words, appended to the current overhang, spell what its top words spell, walks the queue from a history to the halting configuration.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.topW_head {Γ : Type} {Rule : List Γ → List Γ → Prop} {d : Dom Γ} (halt : Γ) (hd : Ok Rule d) :

(topW halt d).head? = some Letter.star

A match gives a derivation. The first domino of a match can only be the one that opens a history, since every top word begins with the decoration and no other bottom word does; from there the queue lemma reads the match as a computation.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.topW_ne_nil {Γ : Type} {Rule : List Γ → List Γ → Prop} {d : Dom Γ} (halt : Γ) (hd : Ok Rule d) :

topW halt d ≠ []

Dependency graph

theorem DescriptiveComplexity.Pcp.History.botW_ne_nil {Γ : Type} {Rule : List Γ → List Γ → Prop} {d : Dom Γ} (C₀ : List Γ) (hd : Ok Rule d) :

botW C₀ d ≠ []

Dependency graph

theorem DescriptiveComplexity.Pcp.History.botW_head_ne {Γ : Type} {Rule : List Γ → List Γ → Prop} {d : Dom Γ} (C₀ : List Γ) (hd : Ok Rule d) (hne : d ≠ Dom.start) :

(botW C₀ d).head? ≠ some Letter.star

Only the domino opening a history has a bottom word beginning with the decoration; every other one begins with a letter.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.derives_of_hasMatch {Γ : Type} {Rule : List Γ → List Γ → Prop} {C₀ : List Γ} {halt : Γ} (h : HasMatch Rule C₀ halt) :

Derives Rule C₀ [halt]

A match gives a derivation. The first domino of a match can only be the one that opens a history, since every top word begins with the decoration and no other bottom word does; from there the queue lemma reads the match as a computation.

Dependency graph

theorem DescriptiveComplexity.Pcp.History.hasMatch_iff {Γ : Type} {Rule : List Γ → List Γ → Prop} (hne : ∀ (l r : List Γ), Rule l r → l ≠ [] ∧ r ≠ []) (C₀ : List Γ) (halt : Γ) :

HasMatch Rule C₀ halt ↔ Derives Rule C₀ [halt]

The dominoes decide derivability: the system has a match exactly when its start word derives the halting configuration.

Dependency graph