PCP characterization of a string-constraint family

AbbreviationAlphabet for the PCP encoding#✓fully proved

The alphabet for the PCP encoding: dominoes (as index letters) and plain letters.

abbrev BlockSym (α : Type*) := Post.Domino α ⊕ α

Uses 1 · Used by 12

Statement usesDomino (Post correspondence problem)

Used byDomino named by a one-letter block · Bottom morphism of the PCP encoding · Domino as an index letter · Regular language of domino index words · Bottom morphism applied to an index word · Top morphism applied to an index word · Flattening a list of one-letter blocks · Membership in the domino index-word language · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words · Top morphism of the PCP encoding

AbbreviationDomino as an index letter#✓fully proved

A domino as an index letter.

abbrev dominoLetter (d : Post.Domino α) : BlockSym α := Sum.inl d

Uses 2 · Used by 1

Statement usesAlphabet for the PCP encoding · Domino (Post correspondence problem)

Used byFlattening a list of one-letter blocks

DefinitionTop morphism of the PCP encoding#✓fully proved

The top morphism: a domino letter maps to its top word as plain letters; plain letters map to [] (they never occur in an index word).

def topFun : BlockSym α → List (BlockSym α)
  | Sum.inl d => d.1.map Sum.inr
  | Sum.inr _ => []

Uses 2 · Used by 3

Statement usesAlphabet for the PCP encoding · Domino (Post correspondence problem)

Used byTop morphism applied to an index word · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability:

DefinitionBottom morphism of the PCP encoding#✓fully proved

The bottom morphism.

def botFun : BlockSym α → List (BlockSym α)
  | Sum.inl d => d.2.map Sum.inr
  | Sum.inr _ => []

Uses 2 · Used by 3

Statement usesAlphabet for the PCP encoding · Domino (Post correspondence problem)

Used byBottom morphism applied to an index word · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability:

DefinitionRegular language of domino index words#✓fully proved

The regular language of index words: concatenations of domino letters.

def dominoRegex (P : List (Post.Domino α)) : RegularExpression (BlockSym α) :=
  RegularExpression.star ((P.map fun d => RegularExpression.char (Sum.inl d)).sum)

Uses 2 · Used by 4

Statement usesAlphabet for the PCP encoding · Domino (Post correspondence problem)

Used byMembership in the domino index-word language · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words

DefinitionPCP encoding as a one-variable string constraint#✓fully proved

The PCP encoding as a string constraint over one variable.

def pcpConstraint (P : List (Post.Domino α)) : Formula (BlockSym α) (Fin 1) :=
  Formula.and
    (Formula.atom (Atom.mem (Term.var 0) (EncodedRegex.flatten (dominoRegex P))))
    (Formula.and
      (Formula.atom (Atom.eq (Term.hom topFun (Term.var 0))
        (Term.hom botFun (Term.var 0))))
      (Formula.atom (Atom.lenGe (Term.var 0) 1)))

Uses 10 · Used by 1

Statement usesString constraint atom · Alphabet for the PCP encoding · String formulas · String term over variables · Bottom morphism of the PCP encoding · Regular language of domino index words · Top morphism of the PCP encoding · Domino (Post correspondence problem) · Encoded regular expressions · Encoding of a regular expression

Used byPCP is characterized by string-constraint satisfiability:

DefinitionDomino named by a one-letter block#✓fully proved

The domino named by a one-letter block; junk ([], []) otherwise.

def blockDomino (b : List (BlockSym α)) : Post.Domino α :=
  match b with
  | [Sum.inl d] => d
  | _ => ([], [])

Uses 2 · Used by 1

Statement usesAlphabet for the PCP encoding · Domino (Post correspondence problem)

Used byPCP is characterized by string-constraint satisfiability:

TheoremMembership in a sum of regular expressions#✓fully proved

Membership in a sum of regular expressions.

theorem mem_sum_matches {rs : List (RegularExpression α)} {w : List α} :
    w ∈ (rs.sum).matches' ↔ ∃ r ∈ rs, w ∈ r.matches'

Used by 1

Used byMembership in the domino index-word language

TheoremMembership in the domino index-word language#✓fully proved

Membership in the index-word language: the word is a concatenation of domino letters.

theorem mem_dominoRegex {P : List (Post.Domino α)} {w : List (BlockSym α)} :
    w ∈ (dominoRegex P).matches' ↔
      ∃ bs : List (List (BlockSym α)), w = bs.flatten ∧
        ∀ b ∈ bs, ∃ d ∈ P, b = [Sum.inl d]

Uses 4 · Used by 1

Statement usesAlphabet for the PCP encoding · Regular language of domino index words · Domino (Post correspondence problem)

Proof usesMembership in a sum of regular expressions

Used byPCP is characterized by string-constraint satisfiability:

TheoremMembership atom of the PCP encoding checks index words#✓fully proved

The membership atom of the encoding checks index-word membership.

theorem sat_mem_dominoRegex {σ : Fin 1 → List (BlockSym α)}
    {P : List (Post.Domino α)} :
    SatAtom σ (Atom.mem (Term.var 0) (EncodedRegex.flatten (dominoRegex P))) ↔
      σ 0 ∈ (dominoRegex P).matches'

Uses 10 · Used by 1

Statement usesString constraint atom · Alphabet for the PCP encoding · Satisfaction of a string atom · String term over variables · Regular language of domino index words · Domino (Post correspondence problem) · Encoded regular expressions · Encoding of a regular expression

Proof usesThe regular expression denoted by an encoding · Every regular expression has an encoding

Used byPCP is characterized by string-constraint satisfiability:

TheoremTop morphism applied to an index word#✓fully proved

The top morphism applied to an index word.

theorem flatMap_topFun {w : List (BlockSym α)} {s : List (Post.Domino α)}
    (hw : w = s.map Sum.inl) : w.flatMap topFun = (Post.top s).map Sum.inr

Uses 4 · Used by 1

Statement usesAlphabet for the PCP encoding · Top morphism of the PCP encoding · Domino (Post correspondence problem) · Top word of a sequence of dominoes

Used byPCP is characterized by string-constraint satisfiability:

TheoremBottom morphism applied to an index word#✓fully proved

The bottom morphism applied to an index word.

theorem flatMap_botFun {w : List (BlockSym α)} {s : List (Post.Domino α)}
    (hw : w = s.map Sum.inl) : w.flatMap botFun = (Post.bottom s).map Sum.inr

Uses 4 · Used by 1

Statement usesAlphabet for the PCP encoding · Bottom morphism of the PCP encoding · Domino (Post correspondence problem) · Bottom word of a domino sequence

Used byPCP is characterized by string-constraint satisfiability:

TheoremFlattening a list of one-letter blocks#✓fully proved

Flattening a list of one-letter blocks.

theorem map_inl_flatten (s : List (Post.Domino α)) :
    s.map dominoLetter = (s.map (fun d => [dominoLetter d])).flatten

Uses 3 · Used by 1

Statement usesAlphabet for the PCP encoding · Domino as an index letter · Domino (Post correspondence problem)

Used byPCP is characterized by string-constraint satisfiability:

TheoremPCP is characterized by string-constraint satisfiability:#✓fully proved

For each PCP instance P, PCP P holds iff the encoding constraint is satisfiable. This is a semantic characterization, not a computable reduction to a formula-indexed satisfiability predicate (see the module header).

theorem pcp_iff_stringSat (P : List (Post.Domino α)) :
    Post.PCP P ↔ ∃ σ : Fin 1 → List (BlockSym α), Sat σ (pcpConstraint P)

Uses 24

Statement usesAlphabet for the PCP encoding · Satisfaction of a string formula · PCP encoding as a one-variable string constraint · Domino (Post correspondence problem) · The Post correspondence problem

Proof usesString constraint atom · String formulas · Satisfaction of a string atom · String term over variables · Domino named by a one-letter block · Bottom morphism of the PCP encoding · Regular language of domino index words · Evaluation of a string term under an assignment · Bottom morphism applied to an index word · Top morphism applied to an index word · Flattening a list of one-letter blocks · Membership in the domino index-word language · Membership atom of the PCP encoding checks index words · Top morphism of the PCP encoding · PCP solution · Bottom word of a domino sequence · Top word of a sequence of dominoes · Encoded regular expressions · Encoding of a regular expression

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.