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

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

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

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

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

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

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.

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