Regular expressions with squaring

DefinitionKleene star of a bitstring language#✓fully proved

For a set \(S\) of bitstrings, its Kleene star is the set of all concatenations \(u_1 u_2 \cdots u_k\), for \(k \ge 0\), of bitstrings \(u_1, \dots, u_k \in S\); the empty concatenation (\(k = 0\)) is the empty bitstring.

def starLang (S : Set (List Bool)) : Set (List Bool) :=
  {w | ∃ l : List (List Bool), w = l.flatten ∧ ∀ u ∈ l, u ∈ S}

Used by 1

Used byEvaluation of postfix regular expressions with squaring

DefinitionConcatenation of bitstring languages#✓fully proved

For sets \(S\) and \(T\) of bitstrings, their concatenation is the set of all bitstrings \(uv\) with \(u \in S\) and \(v \in T\).

def concatLang (S T : Set (List Bool)) : Set (List Bool) :=
  {w | ∃ u v, w = u ++ v ∧ u ∈ S ∧ v ∈ T}

Used by 1

Used byEvaluation of postfix regular expressions with squaring

DefinitionEvaluation of postfix regular expressions with squaring#✓fully proved

A list of natural-number tokens is evaluated from left to right on a given stack of languages of bitstrings. Token \(0\) pushes the empty language, token \(1\) pushes the language containing only the empty bitstring, and tokens \(2\) and \(3\) push the languages containing only the one-letter bitstring false, respectively true. Token \(4\) pops the top language \(S\) and the language \(T\) below it and pushes the concatenation \(TS\); token \(5\) pops \(S\) and \(T\) in the same way and pushes \(T \cup S\); token \(6\) pops \(S\) and pushes its Kleene star; token \(7\) pops \(S\) and pushes its square \(SS\). When the tokens run out, the evaluation returns the language on the stack if the stack holds exactly one language. It fails if the stack holds any other number of languages at the end, if a token is larger than \(7\), or if an operator token finds too few languages on the stack.

noncomputable def evalPostfix : List ℕ → List (Set (List Bool)) → Option (Set (List Bool))
  | [], [S] => some S
  | [], _ => none
  | 0 :: rest, stack => evalPostfix rest (∅ :: stack)
  | 1 :: rest, stack => evalPostfix rest ({[]} :: stack)
  | 2 :: rest, stack => evalPostfix rest ({[false]} :: stack)
  | 3 :: rest, stack => evalPostfix rest ({[true]} :: stack)
  | 4 :: rest, S :: T :: stack => evalPostfix rest (concatLang T S :: stack)
  | 5 :: rest, S :: T :: stack => evalPostfix rest (Set.union T S :: stack)
  | 6 :: rest, S :: stack => evalPostfix rest (starLang S :: stack)
  | 7 :: rest, S :: stack => evalPostfix rest (concatLang S S :: stack)
  | _, _ => none

Uses 2 · Used by 1

Statement usesConcatenation of bitstring languages · Kleene star of a bitstring language

Used byUniversality of postfix regular expressions with squaring

DefinitionUniversality of postfix regular expressions with squaring#✓fully proved

This is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of lists of natural numbers, to a token list whose evaluation as a postfix regular expression with squaring, started on the empty stack, succeeds and returns the set of all bitstrings. A bitstring that does not decode to a list of natural numbers is rejected.

noncomputable def regexUnivDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := List ℕ) x with
  | some toks => decide (evalPostfix toks [] = some Set.univ)
  | none => false

Uses 10 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Evaluation of postfix regular expressions with squaring · Decision problems

Used byRegular expressions with squaring: universality is EXPSPACE-complete

TheoremRegular expressions with squaring: universality is EXPSPACE-complete#●ready to prove

The universality problem for postfix regular expressions with squaring belongs to \(\mathsf{EXPSPACE}\), and every decision problem in \(\mathsf{EXPSPACE}\) reduces to it by a polynomial-time many-one reduction. Here the universality problem accepts a bitstring exactly when it decodes to a list of natural-number tokens whose postfix evaluation, started on the empty stack, returns the set of all bitstrings.

public theorem_wanted regex_squaring_expspace_complete :
    regexUnivDec ∈ EXPSPACE ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ EXPSPACE → Cslib.CookLevin.PolyManyOneRed L regexUnivDec

Sources

• A. R. Meyer and L. J. Stockmeyer, "The equivalence problem for regular expressions with squaring requires exponential space", Proceedings of the Thirteenth Annual Symposium on Switching and Automata Theory (1972), 125-129. (The exponential-time word problem in Stockmeyer- Meyer (STOC 1973) is membership, not universality.)

Uses 5

Statement usesThe class EXPSPACE · Polynomial-time many-one reduction · Universality of postfix regular expressions with squaring · Complexity classes · Decision problems

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.