Decision procedures for regular expressions

InductiveRegular-expression node#✓fully proved

A node of an encoded regular expression over an alphabet \(\alpha\) is one of six kinds: zero, epsilon, a letter \(a \in \alpha\), a sum with arguments \(i, j \in \mathbb{N}\), a product (concatenation) with arguments \(i, j \in \mathbb{N}\), or a star with argument \(i \in \mathbb{N}\), where the arguments are indices of nodes.

inductive RegexNode (α : Type*) where
  | zero
  | epsilon
  | char (a : α)
  | plus (i j : ℕ)
  | comp (i j : ℕ)
  | star (i : ℕ)
Used by 36
Used byEncoded regular expressions · Encodings are lists of nodes · Flags of all nodes · Correctness of the flag pass · Encoding of a regular expression · Postorder encoding after a prefix · The pass computes the Thompson state count of every node · Infiniteness test for encoded regular expressions · One state count per node · Soundness of the grammar of a regular expression · A production of a node only produces words of its language · Node at an index · Regex nodes as a sum type · Productions of a node · Thompson state count of an encoding · The pass counts the states of Thompson's automaton · The equivalence test is primitive recursive · The equivalence search bound is primitive recursive · The Thompson state count of an encoding is primitive recursive · The pass of Thompson state counts is primitive recursive · One step of the Thompson state count is primitive recursive · Regular expression at a node · Appending nodes does not change earlier expressions · Thompson state counts of a node list · Appending a node appends its count · Flags of the next node · One step of the Thompson state count · EQ_REX is decidable · Emptiness of regular expressions is decidable · Infiniteness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · The grammar of an encoded regular expression · The regular expression denoted by an encoding · Every regular expression has an encoding · Completeness of the grammar of an encoded regular expression

StructureEncoded regular expressions#✓fully proved

An encoded regular expression over an alphabet \(\alpha\) is a list of regular-expression nodes, each a constant (\(0\), \(1\) or a letter) or an operator (sum, concatenation or star) whose arguments are node indices; the last node is the root. Any list is allowed: in the semantics, an argument that is not the index of an earlier node reads as \(0\), and the empty list denotes \(0\).

structure EncodedRegex (α : Type*) where
  /-- The nodes. -/
  nodes : List (RegexNode α)
Uses 1 · Used by 42
Statement usesRegular-expression node
Used byEquivalence test · The equivalence test is correct · Search bound for equivalence · Encodings are lists of nodes · Correctness of the flag pass · Encoding of a regular expression · Language of a sentential form · The pass computes the Thompson state count of every node · Infiniteness test for encoded regular expressions · Emptiness test for regular expressions · The grammar generates the language of the expression · Short distinguishing words for encoded regular expressions · Membership test for regular expressions · Soundness of the grammar of a regular expression · A production of a node only produces words of its language · Node at an index · Thompson state count of an encoding · The pass counts the states of Thompson's automaton · The equivalence test is primitive recursive · The equivalence search bound is primitive recursive · The Thompson state count of an encoding is primitive recursive · Regular expression at a node · Appending nodes does not change earlier expressions · Inclusion test · EQ_REX is decidable · Emptiness of regular expressions is decidable · Infiniteness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · The grammar of an encoded regular expression · The regular expression denoted by an encoding · Every regular expression has an encoding · Completeness of the grammar of an encoded regular expression · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words · String constraint atom · Satisfaction of a string atom · Boolean checker for atom satisfaction · Correctness of the Boolean atom checker · Atom satisfaction depends only on its variables · Variables occurring in a string atom

DefinitionNode at an index#✓fully proved

For an encoded regular expression \(e\) and a natural number \(k\), the node of \(e\) at index \(k\) is the entry at position \(k\) (counting from \(0\)) of its list of nodes, or the zero node when \(k\) is at least the length of the list.

def node (e : EncodedRegex α) (k : ℕ) : RegexNode α :=
  e.nodes.getD k .zero
Uses 2 · Used by 15
Statement usesEncoded regular expressions · Regular-expression node
Used byCorrectness of the flag pass · The pass computes the Thompson state count of every node · Soundness of the grammar of a regular expression · A production of a node only produces words of its language · The pass counts the states of Thompson's automaton · The equivalence test is primitive recursive · Regular expression at a node · Appending nodes does not change earlier expressions · Emptiness of regular expressions is decidable · Infiniteness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · The grammar of an encoded regular expression · Every regular expression has an encoding · Completeness of the grammar of an encoded regular expression

DefinitionRegular expression at a node#✓fully proved

For an encoded regular expression \(e\) and \(k \in \mathbb{N}\), the regular expression at node \(k\) is defined by recursion on \(k\) from the node of \(e\) at index \(k\) (a zero node when \(k\) is past the end): a zero node gives \(0\), an epsilon node gives \(1\), a node for a letter \(a\) gives \(a\), and a sum, product or star node gives the sum, product or star of the regular expressions at its arguments, where an argument that is not smaller than \(k\) reads as \(0\).

def regexAt (e : EncodedRegex α) (k : ℕ) : RegularExpression α :=
  match e.node k with
  | .zero => 0
  | .epsilon => 1
  | .char a => .char a
  | .plus i j => (if _ : i < k then e.regexAt i else 0) + (if _ : j < k then e.regexAt j else 0)
  | .comp i j => (if _ : i < k then e.regexAt i else 0) * (if _ : j < k then e.regexAt j else 0)
  | .star i => .star (if _ : i < k then e.regexAt i else 0)
termination_by k
Uses 3 · Used by 12
Statement usesEncoded regular expressions · Node at an index · Regular-expression node
Used byCorrectness of the flag pass · Language of a sentential form · The pass computes the Thompson state count of every node · The grammar generates the language of the expression · Soundness of the grammar of a regular expression · A production of a node only produces words of its language · The pass counts the states of Thompson's automaton · Appending nodes does not change earlier expressions · Infiniteness of regular expressions is decidable · The regular expression denoted by an encoding · Every regular expression has an encoding · Completeness of the grammar of an encoded regular expression

DefinitionThe regular expression denoted by an encoding#✓fully proved

An encoded regular expression \(e\) with \(n\) nodes denotes the regular expression at its node \(n - 1\), the last node. For \(n = 0\) this is the expression at node \(0\), which lies past the end of the list and is the empty expression \(0\).

def toRegex (e : EncodedRegex α) : RegularExpression α :=
  e.regexAt (e.nodes.length - 1)
Uses 3 · Used by 14
Statement usesEncoded regular expressions · Regular expression at a node · Regular-expression node
Used byThe equivalence test is correct · The grammar generates the language of the expression · Short distinguishing words for encoded regular expressions · The pass counts the states of Thompson's automaton · EQ_REX is decidable · Emptiness of regular expressions is decidable · Infiniteness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · Every regular expression has an encoding · Membership atom of the PCP encoding checks index words · Satisfaction of a string atom · Correctness of the Boolean atom checker · Atom satisfaction depends only on its variables

TheoremAppending nodes does not change earlier expressions#✓fully proved

Let \(l\) and \(m\) be lists of regular-expression nodes and let \(k\) be smaller than the length of \(l\). Then the regular expression at node \(k\) of the encoding with nodes \(l\) followed by \(m\) equals the regular expression at node \(k\) of the encoding with nodes \(l\).

theorem regexAt_append {l m : List (RegexNode α)} {k : ℕ} (hk : k < l.length) :
    (⟨l ++ m⟩ : EncodedRegex α).regexAt k = (⟨l⟩ : EncodedRegex α).regexAt k
Uses 4 · Used by 3
Statement usesEncoded regular expressions · Regular expression at a node · Regular-expression node
Proof usesNode at an index
Used byCorrectness of the flag pass · The pass computes the Thompson state count of every node · Every regular expression has an encoding

DefinitionPostorder encoding after a prefix#✓fully proved

For a regular expression \(r\) and a list \(l\) of nodes, the nodes of \(r\) are appended after \(l\) in postorder, by recursion on \(r\). For \(0\), \(1\) and a letter \(a\), append the single node \(0\), \(1\) or \(a\). For a sum \(s + t\) (respectively a concatenation \(st\)), append the nodes of \(s\) after \(l\), giving \(l_1\), then the nodes of \(t\) after \(l_1\), giving \(l_2\), then a sum (respectively concatenation) node with arguments \(|l_1| - 1\) and \(|l_2| - 1\). For a star \(s^*\), append the nodes of \(s\) after \(l\), giving \(l_1\), then a star node with argument \(|l_1| - 1\). The root of \(r\) is the last node.

Cslib.Language.EncodedRegex.flattenAux · 15 lines 
def flattenAux : RegularExpression α → List (RegexNode α) → List (RegexNode α)
  | .zero, l => l ++ [.zero]
  | .epsilon, l => l ++ [.epsilon]
  | .char a, l => l ++ [.char a]
  | .plus r s, l =>
      let l₁ := flattenAux r l
      let l₂ := flattenAux s l₁
      l₂ ++ [.plus (l₁.length - 1) (l₂.length - 1)]
  | .comp r s, l =>
      let l₁ := flattenAux r l
      let l₂ := flattenAux s l₁
      l₂ ++ [.comp (l₁.length - 1) (l₂.length - 1)]
  | .star r, l =>
      let l₁ := flattenAux r l
      l₁ ++ [.star (l₁.length - 1)]
Uses 1 · Used by 2
Statement usesRegular-expression node
Used byEncoding of a regular expression · Every regular expression has an encoding

DefinitionEncoding of a regular expression#✓fully proved

The encoding of a regular expression \(r\) is the list of nodes obtained by appending the nodes of \(r\) in postorder after the empty list, so that the root of \(r\) is the last node.

def flatten (r : RegularExpression α) : EncodedRegex α :=
  ⟨flattenAux r []⟩
Uses 3 · Used by 4
Statement usesEncoded regular expressions · Postorder encoding after a prefix · Regular-expression node
Used byEvery regular expression has an encoding · PCP encoding as a one-variable string constraint · PCP is characterized by string-constraint satisfiability: · Membership atom of the PCP encoding checks index words

TheoremEvery regular expression has an encoding#✓fully proved

For every regular expression \(r\) over an alphabet \(\alpha\), the encoded regular expression obtained by flattening \(r\) (listing the nodes of its subexpressions in postorder, so that the root of \(r\) is the last node) denotes \(r\).

theorem toRegex_flatten (r : RegularExpression α) : (flatten r).toRegex = r
Uses 8 · Used by 1
Statement usesEncoding of a regular expression · The regular expression denoted by an encoding
Proof usesEncoded regular expressions · Postorder encoding after a prefix · Node at an index · Regular expression at a node · Appending nodes does not change earlier expressions · Regular-expression node
Used byMembership atom of the PCP encoding checks index words

DefinitionFlags of the empty language#✓fully proved

The flag triple of the empty language is \((\mathrm{false}, \mathrm{false}, \mathrm{false})\); the three flags of a language say whether it is nonempty, whether it has a nonempty word, and whether it is infinite. This triple is also read for an argument of a node that is not an earlier node.

def zeroFlags : Bool × Bool × Bool :=
  (false, false, false)
Used by 4
Used byCorrectness of the flag pass · Infiniteness test for encoded regular expressions · Flags of the next node · Infiniteness of regular expressions is decidable

DefinitionFlags of a sum#✓fully proved

For triples of booleans \(b = (b_1, b_2, b_3)\) and \(c = (c_1, c_2, c_3)\), the flags of the sum are \((b_1 \lor c_1, b_2 \lor c_2, b_3 \lor c_3)\).

If \(b\) and \(c\) record whether languages \(L\) and \(M\) are nonempty, contain a nonempty word and are infinite, then the flags of the sum record the same for their union \(L \cup M\).

def plusFlags (b c : Bool × Bool × Bool) : Bool × Bool × Bool :=
  (b.1 || c.1, b.2.1 || c.2.1, b.2.2 || c.2.2)
Used by 3
Used byCorrectness of the flag pass · Flags of the next node · Infiniteness of regular expressions is decidable

DefinitionFlags of a concatenation#✓fully proved

For triples of Booleans \(b = (b_1, b_2, b_3)\) and \(c = (c_1, c_2, c_3)\), the flags of the product are \((b_1 \land c_1,\ (b_2 \land c_1) \lor (b_1 \land c_2),\ (b_3 \land c_1) \lor (b_1 \land c_3))\).

If \(b\) and \(c\) record whether languages \(L\) and \(M\) are nonempty, contain a nonempty word, and are infinite, the result records the same for \(LM\): in particular \(LM\) is infinite when one factor is infinite and the other nonempty.

def compFlags (b c : Bool × Bool × Bool) : Bool × Bool × Bool :=
  (b.1 && c.1, b.2.1 && c.1 || b.1 && c.2.1, b.2.2 && c.1 || b.1 && c.2.2)
Used by 3
Used byCorrectness of the flag pass · Flags of the next node · Infiniteness of regular expressions is decidable

DefinitionFlags of a star#✓fully proved

Given a triple of Booleans \((b_1, b_2, b_3)\), the flags of its star are \((\mathrm{true}, b_2, b_2)\). Read as the flags (nonempty, has a nonempty word, infinite) of a language, a star is always nonempty, and it has a nonempty word, and is infinite, exactly when the argument has a nonempty word.

def starFlags (b : Bool × Bool × Bool) : Bool × Bool × Bool :=
  (true, b.2.1, b.2.1)
Used by 3
Used byCorrectness of the flag pass · Flags of the next node · Infiniteness of regular expressions is decidable

DefinitionFlags of the next node#✓fully proved

Given the list \(A\) of flag triples of the nodes before it, the flag triple of a node is \((\mathrm{false}, \mathrm{false}, \mathrm{false})\) for a zero node, \((\mathrm{true}, \mathrm{false}, \mathrm{false})\) for an epsilon node and \((\mathrm{true}, \mathrm{true}, \mathrm{false})\) for a letter node. For a sum, product or star node it is the flags of a sum, product or star applied to the entries of \(A\) at its arguments, where an argument that is not an index of \(A\) reads as \((\mathrm{false}, \mathrm{false}, \mathrm{false})\).

def stepFlags (acc : List (Bool × Bool × Bool)) : RegexNode α → Bool × Bool × Bool
  | .zero => zeroFlags
  | .epsilon => (true, false, false)
  | .char _ => (true, true, false)
  | .plus i j => plusFlags (acc.getD i zeroFlags) (acc.getD j zeroFlags)
  | .comp i j => compFlags (acc.getD i zeroFlags) (acc.getD j zeroFlags)
  | .star i => starFlags (acc.getD i zeroFlags)
Uses 5 · Used by 3
Statement usesFlags of a concatenation · Flags of a sum · Flags of a star · Flags of the empty language · Regular-expression node
Used byFlags of all nodes · Correctness of the flag pass · Infiniteness of regular expressions is decidable

DefinitionFlags of all nodes#✓fully proved

For a list of nodes \(n_0, \dots, n_{m-1}\), the flags \(f_0, \dots, f_{m-1}\) are computed in one left-to-right pass: \(f_k\) is the step flags of node \(n_k\) computed from the flags \(f_0, \dots, f_{k-1}\) of the nodes before it.

def flags (l : List (RegexNode α)) : List (Bool × Bool × Bool) :=
  l.foldl (fun acc n => acc ++ [stepFlags acc n]) []
Uses 2 · Used by 3
Statement usesFlags of the next node · Regular-expression node
Used byCorrectness of the flag pass · Infiniteness test for encoded regular expressions · Infiniteness of regular expressions is decidable

DefinitionFlags of a language#✓fully proved

A triple of Booleans \((b_1, b_2, b_3)\) describes a language \(L\) when \(b_1\) is true exactly when \(L\) is nonempty, \(b_2\) is true exactly when \(L\) contains a nonempty word, and \(b_3\) is true exactly when \(L\) is infinite.

def FlagsOK (b : Bool × Bool × Bool) (L : Language α) : Prop :=
  (b.1 = true ↔ ∃ w, w ∈ L) ∧ (b.2.1 = true ↔ ∃ w ∈ L, w ≠ []) ∧ (b.2.2 = true ↔ L.Infinite)
Used by 1
Used byCorrectness of the flag pass

TheoremCorrectness of the flag pass#✓fully proved

For a list \(l\) of nodes and a natural number \(k\), let \(f_k\) be the entry at position \(k\) of the flags of \(l\), or the zero flags \((\mathrm{false}, \mathrm{false}, \mathrm{false})\) if \(k\) is at least the length of \(l\). Then \(f_k\) describes the language of the regular expression at node \(k\) of the encoding \(l\) when \(k\) is less than the length of \(l\), and describes the empty language otherwise.

theorem flagsOK_flags (l : List (RegexNode α)) :
    ∀ k, FlagsOK ((flags l).getD k zeroFlags)
      (if k < l.length then (⟨l⟩ : EncodedRegex α).regexAt k else 0).matches'
Uses 12 · Used by 1
Statement usesEncoded regular expressions · Flags of a language · Flags of all nodes · Regular expression at a node · Flags of the empty language · Regular-expression node
Proof usesFlags of a concatenation · Node at an index · Flags of a sum · Appending nodes does not change earlier expressions · Flags of a star · Flags of the next node
Used byInfiniteness of regular expressions is decidable

DefinitionInfiniteness test for encoded regular expressions#✓fully proved

Let \(e\) be an encoded regular expression with nodes \(n_0, \dots, n_{m-1}\), and let \(f_0, \dots, f_{m-1}\) be the flags of all nodes of \(e\), the triples of Booleans computed in one left-to-right pass over the nodes. The infiniteness test of \(e\) is the third component of \(f_{m-1}\), the flag triple of the last node (the root); when \(e\) has no nodes it is false.

The three flags of a node say whether its language is nonempty, contains a nonempty word and is infinite, so the test returns true exactly when the language of \(e\) is infinite.

def infiniteB (e : EncodedRegex α) : Bool :=
  ((flags e.nodes).getD (e.nodes.length - 1) zeroFlags).2.2
Uses 4 · Used by 1
Statement usesEncoded regular expressions · Flags of all nodes · Flags of the empty language · Regular-expression node
Used byInfiniteness of regular expressions is decidable

DefinitionProductions of a sum node#✓fully proved

For natural numbers \(k\), \(i\) and \(j\), the productions of a sum node \(k\) with arguments \(i\) and \(j\) are the unit production \(k \to i\) if \(i < k\), followed by the unit production \(k \to j\) if \(j < k\) (and nothing else). Nonterminals are node indices.

def plusRules (k i j : ℕ) : List (ℕ × List (ℕ ⊕ α)) :=
  (if i < k then [(k, [.inl i])] else []) ++ (if j < k then [(k, [.inl j])] else [])
Used by 6
Used byProductions of a node · The equivalence test is primitive recursive · Emptiness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · Completeness of the grammar of an encoded regular expression

DefinitionProductions of a concatenation node#✓fully proved

For natural numbers \(k\), \(i\) and \(j\), the productions of a concatenation node \(k\) with arguments \(i\) and \(j\) are the single production \(k \to i\,j\) (nonterminal \(i\) followed by nonterminal \(j\)) when \(i < k\) and \(j < k\), and there are none otherwise.

def compRules (k i j : ℕ) : List (ℕ × List (ℕ ⊕ α)) :=
  if i < k ∧ j < k then [(k, [.inl i, .inl j])] else []
Used by 6
Used byProductions of a node · The equivalence test is primitive recursive · Emptiness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · Completeness of the grammar of an encoded regular expression

DefinitionProductions of a star node#✓fully proved

For natural numbers \(k\) and \(i\), the productions of a star node \(k\) with argument \(i\) are \(k \to \varepsilon\), followed by \(k \to i\,k\) if \(i < k\) (and nothing else). Nonterminals are node indices.

def starRules (k i : ℕ) : List (ℕ × List (ℕ ⊕ α)) :=
  (k, []) :: (if i < k then [(k, [.inl i, .inl k])] else [])
Used by 6
Used byProductions of a node · The equivalence test is primitive recursive · Emptiness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · Completeness of the grammar of an encoded regular expression

DefinitionProductions of a node#✓fully proved

For a natural number \(k\) and a node \(n\), the productions of node \(k\) are the following encoded productions, all with left-hand side \(k\), where nonterminal \(i\) stands for node \(i\): none if \(n\) is the zero node; \(k \to \varepsilon\) if \(n\) is the empty-word node; \(k \to a\) if \(n\) is the character \(a\); if \(n\) is a sum with arguments \(i\) and \(j\), the unit production \(k \to i\) when \(i < k\) and the unit production \(k \to j\) when \(j < k\); if \(n\) is a product with arguments \(i\) and \(j\), the production \(k \to i\,j\) when \(i < k\) and \(j < k\); if \(n\) is a star with argument \(i\), the production \(k \to \varepsilon\) together with \(k \to i\,k\) when \(i < k\).

def nodeRules (k : ℕ) : RegexNode α → List (ℕ × List (ℕ ⊕ α))
  | .zero => []
  | .epsilon => [(k, [])]
  | .char a => [(k, [.inr a])]
  | .plus i j => plusRules k i j
  | .comp i j => compRules k i j
  | .star i => starRules k i
Uses 4 · Used by 8
Statement usesProductions of a concatenation node · Productions of a sum node · Productions of a star node · Regular-expression node
Used bySoundness of the grammar of a regular expression · A production of a node only produces words of its language · The equivalence test is primitive recursive · Emptiness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · The grammar of an encoded regular expression · Completeness of the grammar of an encoded regular expression

DefinitionThe grammar of an encoded regular expression#✓fully proved

For an encoded regular expression \(e\) with \(n\) nodes, its grammar is the encoded context-free grammar with start nonterminal \(n - 1\) (truncated subtraction, so \(0\) when \(n = 0\)), in which nonterminal \(k\) stands for node \(k\). Its productions are, for each node \(k < n\): none if node \(k\) is \(0\); \(k \to \varepsilon\) if it is \(\varepsilon\); if it is the letter \(a\), the production \(k \to a\); if it is the sum of nodes \(i\) and \(j\), the productions \(k \to i\) (when \(i < k\)) and \(k \to j\) (when \(j < k\)); if it is the product of nodes \(i\) and \(j\), the production \(k \to i\,j\) (when \(i < k\) and \(j < k\)); and if it is the star of node \(i\), the productions \(k \to \varepsilon\) and \(k \to i\,k\) (when \(i < k\)). There are no other productions.

def toGrammar (e : EncodedRegex α) : EncodedCFG α :=
  ⟨e.nodes.length - 1, (List.range e.nodes.length).flatMap fun k => nodeRules k (e.node k)⟩
Uses 5 · Used by 12
Statement usesEncoded context-free grammars · Encoded regular expressions · Node at an index · Productions of a node · Regular-expression node
Used byThe equivalence test is correct · Emptiness test for regular expressions · The grammar generates the language of the expression · Membership test for regular expressions · Soundness of the grammar of a regular expression · The equivalence test is primitive recursive · Inclusion test · Emptiness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · Completeness of the grammar of an encoded regular expression · Correctness of the Boolean atom checker

DefinitionLanguage of a sentential form#✓fully proved

For an encoded regular expression \(e\), the language of a sentential form \(X_1 \cdots X_n\) (terminals in \(\alpha\), nonterminals in \(\mathbb{N}\)) is the product \(L_1 \cdots L_n\), where \(L_i\) is \(\{a\}\), the language of the one-letter word \(a\), when \(X_i\) is the terminal \(a\), and the language of the regular expression at node \(k\) of \(e\) when \(X_i\) is the nonterminal \(k\). The empty form has language \(\{\varepsilon\}\).

def formLang (e : EncodedRegex α) : List (Symbol α ℕ) → Language α
  | [] => 1
  | .terminal a :: u => {[a]} * e.formLang u
  | .nonterminal k :: u => (e.regexAt k).matches' * e.formLang u
Uses 2 · Used by 3
Statement usesEncoded regular expressions · Regular expression at a node
Used byThe grammar generates the language of the expression · Soundness of the grammar of a regular expression · A production of a node only produces words of its language

TheoremA production of a node only produces words of its language#✓fully proved

Let \(e\) be an encoded regular expression, \(k\) a natural number and \(x\) one of the productions of node \(k\) built from the node of \(e\) at index \(k\). If a word \(w\) belongs to the language of the right-hand side of \(x\) (the concatenation, over its symbols, of \(\{a\}\) for a terminal \(a\) and of the language of the regular expression at node \(i\) for a nonterminal \(i\)), then \(w\) belongs to the language of the regular expression at node \(k\).

theorem mem_matches_of_mem_nodeRules {e : EncodedRegex α} {k : ℕ} {x : ℕ × List (ℕ ⊕ α)}
    {w : List α} (hx : x ∈ nodeRules k (e.node k))
    (hw : w ∈ e.formLang (x.2.map EncodedCFG.decodeSymbol)) : w ∈ (e.regexAt k).matches'
Uses 7 · Used by 1
Statement usesDecoding a grammar symbol · Encoded regular expressions · Language of a sentential form · Node at an index · Productions of a node · Regular expression at a node
Proof usesRegular-expression node
Used bySoundness of the grammar of a regular expression

TheoremSoundness of the grammar of a regular expression#✓fully proved

Let \(e\) be an encoded regular expression. If a sentential form \(u\) of the context-free grammar of \(e\) yields a terminal word \(w\), then \(w\) belongs to the language of \(u\): the concatenation, over the symbols of \(u\), of \(\{a\}\) for a terminal \(a\) and of the language of the regular expression at node \(k\) for a nonterminal \(k\).

theorem mem_formLang_of_yields {e : EncodedRegex α} {u : List (Symbol α e.toGrammar.toCFG.NT)}
    {w : List α}
    (h : Yields e.toGrammar.toCFG u w) : w ∈ e.formLang u
Uses 12 · Used by 1
Statement usesGrammar denoted by an encoding · Encoded regular expressions · Language of a sentential form · The grammar of an encoded regular expression · Yield of a sentential form
Proof usesEncoded context-free grammars · Decoding a production · A production of a node only produces words of its language · Node at an index · Productions of a node · Regular expression at a node · Regular-expression node
Used byThe grammar generates the language of the expression

TheoremCompleteness of the grammar of an encoded regular expression#✓fully proved

Let \(\alpha\) be an alphabet with decidable equality, \(e\) an encoded regular expression over \(\alpha\) and \(k\) a natural number. Every word in the language of the regular expression at node \(k\) of \(e\) is yielded by the sentential form consisting of the single nonterminal \(k\) in the context-free grammar of \(e\).

theorem yields_of_mem_matches {e : EncodedRegex α} :
    ∀ k {w : List α}, w ∈ (e.regexAt k).matches' → Yields e.toGrammar.toCFG [.nonterminal k] w
Uses 17 · Used by 1
Statement usesGrammar denoted by an encoding · Encoded regular expressions · Regular expression at a node · The grammar of an encoded regular expression · Yield of a sentential form
Proof usesEncoded context-free grammars · Decoding a production · Decoding a grammar symbol · Productions of a concatenation node · Node at an index · Productions of a node · Productions of a sum node · Productions of a star node · Regular-expression node · Concatenation of yields · Splitting a yield over a concatenation · Yield through one production
Used byThe grammar generates the language of the expression

TheoremThe grammar generates the language of the expression#✓fully proved

For every encoded regular expression \(e\), the language of the context-free grammar of \(e\) (one nonterminal per node, the root as start symbol) equals the language of the regular expression that \(e\) denotes.

theorem language_toGrammar (e : EncodedRegex α) : e.toGrammar.language = e.toRegex.matches'
Uses 12 · Used by 5
Statement usesLanguage of an encoded grammar · Encoded regular expressions · The grammar of an encoded regular expression · The regular expression denoted by an encoding
Proof usesEncoded context-free grammars · Grammar denoted by an encoding · Language of a sentential form · Soundness of the grammar of a regular expression · Regular expression at a node · Completeness of the grammar of an encoded regular expression · Yield of a sentential form · Language membership through yields
Used byThe equivalence test is correct · Emptiness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable · Correctness of the Boolean atom checker

DefinitionMembership test for regular expressions#✓fully proved

For an encoded regular expression \(e\) and a word \(w\), the test returns the answer of the membership test for encoded context-free grammars on the word \(w\) and the grammar of \(e\), which has one nonterminal per node and the root as start symbol.

def memB (e : EncodedRegex α) (w : List α) : Bool :=
  e.toGrammar.memLanguageB w
Uses 3 · Used by 6
Statement usesThe membership test for context-free grammars · Encoded regular expressions · The grammar of an encoded regular expression
Used byEquivalence test · The equivalence test is correct · The equivalence test is primitive recursive · Membership for regular expressions is decidable · Boolean checker for atom satisfaction · Correctness of the Boolean atom checker

DefinitionEmptiness test for regular expressions#✓fully proved

For an encoded regular expression \(e\), the test returns the answer of the emptiness test for encoded context-free grammars on the grammar of \(e\), which has one nonterminal per node and the root as start symbol.

def isEmptyB (e : EncodedRegex α) : Bool :=
  e.toGrammar.isEmptyB
Uses 3 · Used by 1
Statement usesThe emptiness test for context-free grammars · Encoded regular expressions · The grammar of an encoded regular expression
Used byEmptiness of regular expressions is decidable

DefinitionInclusion test#✓fully proved

For an encoded regular expression \(e\) and an encoded DFA \(D\), the inclusion test returns the Boolean computed by the CFG ⊆ DFA inclusion test on the grammar of \(e\) and the automaton \(D\).

def subsetB (e : EncodedRegex α) (D : Cslib.Automata.EncodedDFA α) : Bool :=
  EncodedCFG.subsetB e.toGrammar D
Uses 4 · Used by 1
Statement usesEncoded DFA · The inclusion test for a grammar and a DFA · Encoded regular expressions · The grammar of an encoded regular expression
Used byInclusion of a regular language in a DFA language is decidable

DefinitionRegex nodes as a sum type#✓fully proved

The bijection between the nodes of encoded regular expressions over \(\alpha\) and \(1 \oplus 1 \oplus \alpha \oplus (\mathbb{N} \times \mathbb{N}) \oplus (\mathbb{N} \times \mathbb{N}) \oplus \mathbb{N}\), where \(1\) is the one-point type, that sends the zero node and the empty-word node to the first and second copies of \(1\), a character node \(a\) to \(a\), a sum node with arguments \(i, j\) to \((i, j)\) in the first copy of \(\mathbb{N} \times \mathbb{N}\), a product node with arguments \(i, j\) to \((i, j)\) in the second, and a star node with argument \(i\) to \(i\).

Cslib.Language.EncodedRegex.nodeEquiv · 17 lines 
def nodeEquiv : RegexNode α ≃ Unit ⊕ Unit ⊕ α ⊕ (ℕ × ℕ) ⊕ (ℕ × ℕ) ⊕ ℕ where
  toFun
    | .zero => .inl ()
    | .epsilon => .inr (.inl ())
    | .char a => .inr (.inr (.inl a))
    | .plus i j => .inr (.inr (.inr (.inl (i, j))))
    | .comp i j => .inr (.inr (.inr (.inr (.inl (i, j)))))
    | .star i => .inr (.inr (.inr (.inr (.inr i))))
  invFun
    | .inl _ => .zero
    | .inr (.inl _) => .epsilon
    | .inr (.inr (.inl a)) => .char a
    | .inr (.inr (.inr (.inl p))) => .plus p.1 p.2
    | .inr (.inr (.inr (.inr (.inl p)))) => .comp p.1 p.2
    | .inr (.inr (.inr (.inr (.inr i)))) => .star i
  left_inv n := by cases n <;> rfl
  right_inv s := by rcases s with _ | _ | _ | ⟨_, _⟩ | ⟨_, _⟩ | _ <;> rfl
Uses 1 · Used by 10
Statement usesRegular-expression node
Used byThe equivalence test is primitive recursive · The equivalence search bound is primitive recursive · The Thompson state count of an encoding is primitive recursive · The pass of Thompson state counts is primitive recursive · One step of the Thompson state count is primitive recursive · EQ_REX is decidable · Emptiness of regular expressions is decidable · Infiniteness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable

DefinitionEncodings are lists of nodes#✓fully proved

The map sending an encoded regular expression over \(\alpha\) to its list of nodes is a bijection onto the lists of regular-expression nodes over \(\alpha\); its inverse wraps a list of nodes as an encoding.

def equivList : EncodedRegex α ≃ List (RegexNode α) where
  toFun e := e.nodes
  invFun l := ⟨l⟩
  left_inv _ := rfl
  right_inv _ := rfl
Uses 2 · Used by 8
Statement usesEncoded regular expressions · Regular-expression node
Used byThe equivalence test is primitive recursive · The equivalence search bound is primitive recursive · The Thompson state count of an encoding is primitive recursive · EQ_REX is decidable · Emptiness of regular expressions is decidable · Infiniteness of regular expressions is decidable · Inclusion of a regular language in a DFA language is decidable · Membership for regular expressions is decidable

TheoremMembership for regular expressions is decidable#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive coding by natural numbers. The set of pairs \((e, w)\) of an encoded regular expression \(e\) over \(\alpha\) and a word \(w\) over \(\alpha\) such that \(w\) belongs to the language of the regular expression denoted by \(e\) is decidable by a multi-stack machine.

theorem tm2Decidable_mem_matches :
    TM2Decidable fun p : EncodedRegex α × List α => p.2 ∈ p.1.toRegex.matches'
Sources
  • Sipser, Introduction to the Theory of Computation, Theorem 4.3 (\(A_{\mathsf{REX}}\)).
Uses 27
Statement usesDecidability by multi-stack machines · Encoded regular expressions · Encodings are lists of nodes · Regex nodes as a sum type · The regular expression denoted by an encoding · Regular-expression node
Proof usesPredicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Encoded context-free grammars · Encoded grammars as pairs · Items found by the membership procedure · Candidate items for membership · Language of an encoded grammar · The membership test for context-free grammars · Correctness of the membership test · One round of the membership procedure · Start positions of a right-hand side · Fitting a symbol at a position · Productions of a concatenation node · The grammar generates the language of the expression · Membership test for regular expressions · Node at an index · Productions of a node · Productions of a sum node · Productions of a star node · The grammar of an encoded regular expression

TheoremEmptiness of regular expressions is decidable#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive encoding, the property of an encoded regular expression over \(\alpha\) that the language it denotes is empty (E_REX) is decidable by a multi-stack machine.

theorem tm2Decidable_matches_eq_zero :
    TM2Decidable fun e : EncodedRegex α => e.toRegex.matches' = 0
Uses 25
Statement usesDecidability by multi-stack machines · Encoded regular expressions · Encodings are lists of nodes · Regex nodes as a sum type · The regular expression denoted by an encoding · Regular-expression node
Proof usesPredicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Encoded context-free grammars · Encoded grammars as pairs · One round of the generating-nonterminal computation · Generating nonterminals · The emptiness test for context-free grammars · Correctness of the emptiness test · Language of an encoded grammar · Acceptable productions · Productions of a concatenation node · Emptiness test for regular expressions · The grammar generates the language of the expression · Node at an index · Productions of a node · Productions of a sum node · Productions of a star node · The grammar of an encoded regular expression

TheoremInfiniteness of regular expressions is decidable#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive encoding, the property of an encoded regular expression over \(\alpha\) that the language it denotes is infinite is decidable by a multi-stack machine.

theorem tm2Decidable_matches_infinite :
    TM2Decidable fun e : EncodedRegex α => e.toRegex.matches'.Infinite
Uses 18
Statement usesDecidability by multi-stack machines · Encoded regular expressions · Encodings are lists of nodes · Regex nodes as a sum type · The regular expression denoted by an encoding · Regular-expression node
Proof usesPredicates with a primitive recursive decision procedure are computable · Multi-stack decidable predicates are exactly the computable predicates · Flags of a concatenation · Flags of all nodes · Correctness of the flag pass · Infiniteness test for encoded regular expressions · Node at an index · Flags of a sum · Regular expression at a node · Flags of a star · Flags of the next node · Flags of the empty language

TheoremInclusion of a regular language in a DFA language is decidable#✓fully proved

Let \(\alpha\) be an alphabet with decidable equality and a primitive recursive coding by natural numbers. The set of pairs \((e, D)\) of an encoded regular expression \(e\) over \(\alpha\) and an encoded DFA \(D\) over \(\alpha\) such that the language of the regular expression denoted by \(e\) is contained in the language of \(D\) is decidable by a multi-stack machine.

theorem tm2Decidable_matches_le :
    TM2Decidable fun p : EncodedRegex α × Cslib.Automata.EncodedDFA α =>
      p.1.toRegex.matches' ≤ p.2.language
Uses 36
Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines · Encoded regular expressions · Encodings are lists of nodes · Regex nodes as a sum type · The regular expression denoted by an encoding · Regular-expression node
Proof usesComplement of an encoded DFA · Assembling an encoded DFA is primitive recursive · The transition function of encoded DFAs is primitive recursive · States of an encoded DFA · Transition function of an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates · Encoded context-free grammars · Items found for a grammar and a DFA · Candidate items for a grammar and a DFA · Start states of a right-hand side in a DFA · One round of the item search against a DFA · Whether a symbol fits at a DFA state · Encoded grammars as pairs · The intersection-emptiness test for a grammar and a DFA · Language of an encoded grammar · The inclusion test for a grammar and a DFA · Correctness of the inclusion test · Productions of a concatenation node · The grammar generates the language of the expression · Node at an index · Productions of a node · Productions of a sum node · Productions of a star node · Inclusion test · The grammar of an encoded regular expression

TheoremShort distinguishing words#✓fully proved

Two regular expressions \(r\) and \(s\) denote the same language if and only if every word of length less than \(2^{n(r) + n(s)}\), where \(n\) denotes the Thompson state count, is matched by \(r\) exactly when it is matched by \(s\).

The bound is the number of states of the product of the subset-construction DFAs of the Thompson automata.

theorem matches'_eq_iff_forall_length_lt {r s : RegularExpression α} :
    r.matches' = s.matches' ↔ ∀ w : List α, w.length < 2 ^ (numStates r + numStates s) →
      (w ∈ r.matches' ↔ w ∈ s.matches')
Uses 6 · Used by 1
Statement usesThompson state count
Proof usesStates of Thompson's automaton · Correctness of Thompson's construction · Number of states of Thompson's automaton · Thompson's construction · Symmetric difference of two DFAs
Used byShort distinguishing words for encoded regular expressions

DefinitionOne step of the Thompson state count#✓fully proved

Let \(c = (c_0, \dots, c_{m-1})\) be a list of natural numbers, and read \(c_i\) as \(0\) when \(i \ge m\). The Thompson state count of a regular-expression node from \(c\) is \(0\) for the node \(0\), \(1\) for the node \(\varepsilon\), \(2\) for a letter, \(c_i + c_j\) for a sum node and for a concatenation node with arguments \(i\) and \(j\), and \(c_i + 1\) for a star node with argument \(i\).

When \(c\) holds the counts of the nodes before the node, this is the number of states of Thompson's automaton of its expression; an argument that is not an earlier node counts \(0\), as the expression \(0\) does.

def stepStates (acc : List ℕ) : RegexNode α → ℕ
  | .zero => 0
  | .epsilon => 1
  | .char _ => 2
  | .plus i j => acc.getD i 0 + acc.getD j 0
  | .comp i j => acc.getD i 0 + acc.getD j 0
  | .star i => acc.getD i 0 + 1
Uses 1 · Used by 6
Statement usesRegular-expression node
Used byThe pass computes the Thompson state count of every node · One state count per node · The pass of Thompson state counts is primitive recursive · One step of the Thompson state count is primitive recursive · Thompson state counts of a node list · Appending a node appends its count

DefinitionThompson state counts of a node list#✓fully proved

For a list \(l\) of regular-expression nodes, the list of Thompson state counts of \(l\) is computed in one left-to-right pass: starting from the empty list, each node \(n\) of \(l\) in turn appends the count of \(n\) computed from the list of counts built so far.

def stateCounts (l : List (RegexNode α)) : List ℕ :=
  l.foldl (fun acc n => acc ++ [stepStates acc n]) []
Uses 2 · Used by 7
Statement usesOne step of the Thompson state count · Regular-expression node
Used byThe pass computes the Thompson state count of every node · One state count per node · Thompson state count of an encoding · The pass counts the states of Thompson's automaton · The Thompson state count of an encoding is primitive recursive · The pass of Thompson state counts is primitive recursive · Appending a node appends its count

DefinitionThompson state count of an encoding#✓fully proved

The number of Thompson states of an encoded regular expression \(e\) is the entry of the state counts of the nodes of \(e\) at the last node, the root (read as \(0\) when \(e\) has no nodes).

It equals the number of states of Thompson's automaton of the expression that \(e\) denotes.

def numThompsonStates (e : EncodedRegex α) : ℕ :=
  (stateCounts e.nodes).getD (e.nodes.length - 1) 0
Uses 3 · Used by 5
Statement usesEncoded regular expressions · Thompson state counts of a node list · Regular-expression node
Used bySearch bound for equivalence · Short distinguishing words for encoded regular expressions · The pass counts the states of Thompson's automaton · The equivalence search bound is primitive recursive · The Thompson state count of an encoding is primitive recursive

TheoremOne state count per node#✓fully proved

For every list \(l\) of nodes of encoded regular expressions, the list of state counts of \(l\) has the same length as \(l\).

theorem length_stateCounts (l : List (RegexNode α)) : (stateCounts l).length = l.length
Uses 3 · Used by 1
Statement usesThompson state counts of a node list · Regular-expression node
Proof usesOne step of the Thompson state count
Used byThe pass computes the Thompson state count of every node

TheoremAppending a node appends its count#✓fully proved

For every list \(l\) of regular-expression nodes and every node \(n\), let \(l'\) be the list \(l\) with \(n\) appended at the end. Then the list of Thompson state counts of \(l'\) is the list of counts of \(l\) followed by one more entry, the count of \(n\) computed from the counts of \(l\).

theorem stateCounts_append_singleton (l : List (RegexNode α)) (n : RegexNode α) :
    stateCounts (l ++ [n]) = stateCounts l ++ [stepStates (stateCounts l) n]
Uses 3 · Used by 1
Statement usesThompson state counts of a node list · One step of the Thompson state count · Regular-expression node
Used byThe pass computes the Thompson state count of every node

TheoremThe pass computes the Thompson state count of every node#✓fully proved

For every list \(l\) of nodes and every index \(k\), the entry at index \(k\) of the state counts of \(l\) (read as \(0\) past the end of the list) equals the Thompson state count of the regular expression at node \(k\) of the encoding with nodes \(l\) when \(k\) is less than the length of \(l\), and \(0\) otherwise.

theorem getD_stateCounts (l : List (RegexNode α)) :
    ∀ k, (stateCounts l).getD k 0 =
      Thompson.numStates (if k < l.length then (⟨l⟩ : EncodedRegex α).regexAt k else 0)
Uses 10 · Used by 1
Statement usesThompson state count · Encoded regular expressions · Regular expression at a node · Thompson state counts of a node list · Regular-expression node
Proof usesOne state count per node · Node at an index · Appending nodes does not change earlier expressions · Appending a node appends its count · One step of the Thompson state count
Used byThe pass counts the states of Thompson's automaton

TheoremThe pass counts the states of Thompson's automaton#✓fully proved

For every encoded regular expression \(e\), the number of Thompson states of \(e\) computed by the pass over its nodes equals the Thompson state count of the regular expression that \(e\) denotes.

This holds even when the expression tree is exponentially larger than the node list.

theorem numThompsonStates_eq (e : EncodedRegex α) :
    e.numThompsonStates = Thompson.numStates e.toRegex
Uses 9 · Used by 1
Statement usesThompson state count · Encoded regular expressions · Thompson state count of an encoding · The regular expression denoted by an encoding
Proof usesThe pass computes the Thompson state count of every node · Node at an index · Regular expression at a node · Thompson state counts of a node list · Regular-expression node
Used byShort distinguishing words for encoded regular expressions

DefinitionSearch bound for equivalence#✓fully proved

For encoded regular expressions \(e_1\) and \(e_2\), the search bound is \(2^{m + n}\), where \(m\) and \(n\) are the numbers of Thompson states of \(e_1\) and \(e_2\), each computed by one pass over the nodes of the encoding.

def eqBound (e₁ e₂ : EncodedRegex α) : ℕ :=
  2 ^ (e₁.numThompsonStates + e₂.numThompsonStates)
Uses 2 · Used by 5
Statement usesEncoded regular expressions · Thompson state count of an encoding
Used byEquivalence test · The equivalence test is correct · Short distinguishing words for encoded regular expressions · The equivalence test is primitive recursive · The equivalence search bound is primitive recursive

TheoremShort distinguishing words for encoded regular expressions#✓fully proved

Let \(e_1\) and \(e_2\) be encoded regular expressions over an alphabet \(\alpha\), and let \(B\) be their search bound for equivalence. The regular expressions denoted by \(e_1\) and \(e_2\) match the same language if and only if every word \(w\) over \(\alpha\) of length less than \(B\) is matched by the expression denoted by \(e_1\) exactly when it is matched by the expression denoted by \(e_2\).

theorem matches'_eq_iff_forall_length_lt {e₁ e₂ : EncodedRegex α} :
    e₁.toRegex.matches' = e₂.toRegex.matches' ↔ ∀ w : List α, w.length < eqBound e₁ e₂ →
      (w ∈ e₁.toRegex.matches' ↔ w ∈ e₂.toRegex.matches')
Uses 7 · Used by 1
Statement usesEncoded regular expressions · Search bound for equivalence · The regular expression denoted by an encoding
Proof usesShort distinguishing words · Thompson state count · Thompson state count of an encoding · The pass counts the states of Thompson's automaton
Used byThe equivalence test is correct

DefinitionEquivalence test#✓fully proved

Over a finite alphabet with decidable equality and a fixed enumeration of its letters, the equivalence test of two encoded regular expressions \(e_1\) and \(e_2\) returns true exactly when, for every length \(n\) less than the search bound of \(e_1\) and \(e_2\) and every word \(w\) of length \(n\), the membership test gives the same answer for \(e_1\) on \(w\) as for \(e_2\) on \(w\).

def eqB (e₁ e₂ : EncodedRegex α) : Bool :=
  (List.range (eqBound e₁ e₂)).all fun n =>
    (EncodedDFA.wordsOfLength n).all fun w => e₁.memB w == e₂.memB w
Uses 4 · Used by 3
Statement usesWords of a given length · Encoded regular expressions · Search bound for equivalence · Membership test for regular expressions
Used byThe equivalence test is correct · The equivalence test is primitive recursive · EQ_REX is decidable

TheoremThe equivalence test is correct#✓fully proved

Over a finite alphabet with decidable equality and a fixed enumeration of its letters, for all encoded regular expressions \(e_1\) and \(e_2\), the equivalence test returns true on \(e_1\) and \(e_2\) if and only if the regular expressions that \(e_1\) and \(e_2\) denote have the same language.

theorem eqB_iff {e₁ e₂ : EncodedRegex α} :
    eqB e₁ e₂ = true ↔ e₁.toRegex.matches' = e₂.toRegex.matches'
Uses 12 · Used by 1
Statement usesEncoded regular expressions · Equivalence test · The regular expression denoted by an encoding
Proof usesWords of a given length · Language of an encoded grammar · The membership test for context-free grammars · Correctness of the membership test · Search bound for equivalence · The grammar generates the language of the expression · Short distinguishing words for encoded regular expressions · Membership test for regular expressions · The grammar of an encoded regular expression
Used byEQ_REX is decidable

TheoremOne step of the Thompson state count is primitive recursive#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive encoding, the map sending a list \(c\) of natural numbers and a regular-expression node over \(\alpha\) to the Thompson state count of the node computed from \(c\) is primitive recursive.

theorem primrec_stepStates : Primrec₂ (stepStates (α := α))
Uses 3 · Used by 1
Statement usesRegex nodes as a sum type · One step of the Thompson state count · Regular-expression node
Used byThe pass of Thompson state counts is primitive recursive

TheoremThe pass of Thompson state counts is primitive recursive#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive encoding, the map sending a list of regular-expression nodes over \(\alpha\) to the list of their Thompson state counts, computed in one left-to-right pass, is primitive recursive.

theorem primrec_stateCounts : Primrec (stateCounts (α := α))
Uses 5 · Used by 1
Statement usesRegex nodes as a sum type · Thompson state counts of a node list · Regular-expression node
Proof usesOne step of the Thompson state count is primitive recursive · One step of the Thompson state count
Used byThe Thompson state count of an encoding is primitive recursive

TheoremThe Thompson state count of an encoding is primitive recursive#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive encoding, the number of states of Thompson's automaton of an encoded regular expression over \(\alpha\), computed by one pass over its nodes, is a primitive recursive function of the encoding.

theorem primrec_numThompsonStates : Primrec (numThompsonStates (α := α))
Uses 7 · Used by 1
Statement usesEncoded regular expressions · Encodings are lists of nodes · Regex nodes as a sum type · Thompson state count of an encoding · Regular-expression node
Proof usesThe pass of Thompson state counts is primitive recursive · Thompson state counts of a node list
Used byThe equivalence search bound is primitive recursive

TheoremThe equivalence search bound is primitive recursive#✓fully proved

For an alphabet \(\alpha\) with a primitive recursive encoding, the search bound \(2^{m+n}\) for equivalence of two encoded regular expressions over \(\alpha\), where \(m\) and \(n\) are the numbers of states of Thompson's automata of the two expressions, is a primitive recursive function of the pair of encoded expressions.

theorem primrec_eqBound : Primrec₂ (eqBound (α := α))
Uses 7 · Used by 1
Statement usesEncoded regular expressions · Search bound for equivalence · Encodings are lists of nodes · Regex nodes as a sum type · Regular-expression node
Proof usesThompson state count of an encoding · The Thompson state count of an encoding is primitive recursive
Used byThe equivalence test is primitive recursive

TheoremThe equivalence test is primitive recursive#✓fully proved

Over a primitively encodable finite alphabet with decidable equality and a fixed enumeration of its letters, the equivalence test, as a function of two encoded regular expressions, is primitive recursive.

theorem primrec_eqB [DecidableEq α] [FinEnum α] : Primrec₂ (eqB (α := α))
Uses 24 · Used by 1
Statement usesEncoded regular expressions · Equivalence test · Encodings are lists of nodes · Regex nodes as a sum type · Regular-expression node
Proof usesWords of a given length · Boolean membership test for lists of natural numbers · Encoded context-free grammars · Encoded grammars as pairs · Items found by the membership procedure · Candidate items for membership · The membership test for context-free grammars · One round of the membership procedure · Start positions of a right-hand side · Fitting a symbol at a position · Productions of a concatenation node · Search bound for equivalence · Membership test for regular expressions · Node at an index · Productions of a node · Productions of a sum node · The equivalence search bound is primitive recursive · Productions of a star node · The grammar of an encoded regular expression
Used byEQ_REX is decidable

TheoremEQ_REX is decidable#✓fully proved

Let \(\alpha\) be a finite alphabet with a primitive recursive encoding. Then equivalence of encoded regular expressions over \(\alpha\) is decidable by a multi-stack machine: some multi-stack machine decides, for a pair \((e_1, e_2)\) of encoded regular expressions over \(\alpha\), whether the regular expressions that \(e_1\) and \(e_2\) denote have the same language.

This is the regular-expression analogue of Sipser, Theorem 4.5 (EQ_DFA). It is proved by bounded search: the membership decider is run on both expressions for every word shorter than a bound computed from them, and the answers are compared.

theorem tm2Decidable_matches_eq [Finite α] :
    TM2Decidable fun p : EncodedRegex α × EncodedRegex α =>
      p.1.toRegex.matches' = p.2.toRegex.matches'
Uses 11
Statement usesDecidability by multi-stack machines · Encoded regular expressions · Encodings are lists of nodes · Regex nodes as a sum type · The regular expression denoted by an encoding · Regular-expression node
Proof usesPredicates with a primitive recursive decision procedure are computable · Multi-stack decidable predicates are exactly the computable predicates · Equivalence test · The equivalence test is correct · The equivalence test is primitive recursive
55 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.