Closure properties of regular languages

DefinitionMaximal length of the image of a letter#✓fully proved

For a map \(\varphi\) from a finite alphabet \(T\) to words over \(T'\), the bound is the maximum of the lengths \(|\varphi(a)|\) over all letters \(a \in T\) (and \(0\) when \(T\) is empty).

def bound : ℕ :=
  Finset.univ.sup fun a => (φ a).length
Used by 7
Used byNext state while spelling out a letter's image · Soundness of the homomorphic-image ε-NFA · Homomorphic images of regular languages over finite alphabets are regular · Finishing a letter's image in the image ε-NFA · Spelling out a letter's image in the image ε-NFA · The ε-NFA for the homomorphic image · States of the homomorphic-image ε-NFA

AbbreviationStates of the homomorphic-image ε-NFA#✓fully proved

Let \(T\) be a finite alphabet, let \(\varphi\) map letters of \(T\) to words over \(T'\), let \(\sigma\) be a set (the states of a DFA), and let \(N\) be the maximum of the lengths \(|\varphi(a)|\) over \(a \in T\). The states of the ε-NFA form the disjoint union of \(\sigma\) and the set of triples \((q, a, i)\) with \(q \in \sigma\), \(a \in T\) and \(0 \le i < N\).

abbrev State (σ : Type*) : Type _ :=
  σ ⊕ (σ × T × Fin (bound φ))
Uses 1 · Used by 6
Statement usesMaximal length of the image of a letter
Used byNext state while spelling out a letter's image · Soundness of the homomorphic-image ε-NFA · Homomorphic images of regular languages over finite alphabets are regular · Finishing a letter's image in the image ε-NFA · Spelling out a letter's image in the image ε-NFA · The ε-NFA for the homomorphic image

DefinitionNext state while spelling out a letter's image#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(T\) with transition function \(\delta\), and let \(\varphi\) map each letter of \(T\) to a word over \(T'\). For a state \(q\) of \(M\), a letter \(a\) and a natural number \(i\), the state reached after emitting position \(i\) (counted from \(0\)) of \(\varphi(a)\) from \(q\) is the intermediate state \((q, a, i + 1)\) of the ε-NFA if \(i + 1 < |\varphi(a)|\), and the state \(\delta(q, a)\) of \(M\) otherwise.

def advance (q : σ) (a : T) (i : ℕ) : State φ σ :=
  if h : i + 1 < (φ a).length then .inr (q, a, ⟨i + 1, lt_of_lt_of_le h (length_le_bound φ a)⟩)
  else .inl (M.step q a)
Uses 2 · Used by 4
Statement usesStates of the homomorphic-image ε-NFA · Maximal length of the image of a letter
Used bySoundness of the homomorphic-image ε-NFA · Finishing a letter's image in the image ε-NFA · Spelling out a letter's image in the image ε-NFA · The ε-NFA for the homomorphic image

DefinitionThe ε-NFA for the homomorphic image#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(T\) with start state \(q_0\), transition function \(\delta\) and accepting states \(F\), let \(\varphi\) map letters of \(T\) to words over \(T'\), and let \(N\) be the maximum of the lengths \(|\varphi(a)|\) over \(a \in T\). The ε-NFA over \(T'\) has as states the states of \(M\) together with the triples \((q, a, i)\) with \(q\) a state of \(M\), \(a \in T\) and \(0 \le i < N\). Write \(\mathrm{next}(q, a, i)\) for \((q, a, i + 1)\) if \(i + 1 < |\varphi(a)|\) and for \(\delta(q, a)\) otherwise. From a state \(q\) of \(M\), reading \(b\) leads to \(\mathrm{next}(q, a, 0)\) for each letter \(a\) whose image starts with \(b\), and an ε-move leads to \(\delta(q, a)\) for each letter \(a\) with \(\varphi(a)\) empty. From \((q, a, i)\), reading \(b\) leads to \(\mathrm{next}(q, a, i)\) if the letter of \(\varphi(a)\) at position \(i\) (counted from \(0\)) is \(b\), and there are no ε-moves. The only start state is \(q_0\) and the accepting states are those in \(F\).

def εnfa : εNFA T' (State φ σ) where
  step
    | .inl q, some b => {s | ∃ a, (φ a)[0]? = some b ∧ s = advance φ M q a 0}
    | .inr (q, a, i), some b => {s | (φ a)[i.val]? = some b ∧ s = advance φ M q a i}
    | .inl q, none => {s | ∃ a, φ a = [] ∧ s = .inl (M.step q a)}
    | .inr _, none => ∅
  start := {.inl M.start}
  accept := {s | ∃ q ∈ M.accept, s = .inl q}
Uses 3 · Used by 4
Statement usesStates of the homomorphic-image ε-NFA · Next state while spelling out a letter's image · Maximal length of the image of a letter
Used bySoundness of the homomorphic-image ε-NFA · Homomorphic images of regular languages over finite alphabets are regular · Finishing a letter's image in the image ε-NFA · Spelling out a letter's image in the image ε-NFA

DefinitionEdge labels for a letter's image#✓fully proved

For a map \(\varphi\) from letters of \(T\) to words over \(T'\) and a letter \(a\), the label sequence of \(a\) is a single ε-label when \(\varphi(a)\) is empty, and otherwise the letters of \(\varphi(a)\) in order, each as a non-ε label.

def code (a : T) : List (Option T') :=
  if φ a = [] then [none] else (φ a).map some
Used by 2
Used byHomomorphic images of regular languages over finite alphabets are regular · Spelling out a letter's image in the image ε-NFA

TheoremFinishing a letter's image in the image ε-NFA#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(T\) with transition function \(\delta\), and let \(\varphi\) map letters of \(T\) to words over \(T'\). For every state \(q\) of \(M\), letter \(a\) and natural number \(i\), the ε-NFA of \(M\) and \(\varphi\) has a path to the state \(\delta(q, a)\) of \(M\) from the state \((q, a, i + 1)\) if \(i + 1 < |\varphi(a)|\), and from \(\delta(q, a)\) otherwise, whose labels are the letters of \(\varphi(a)\) after position \(i\) (positions counted from \(0\)), in order and all non-ε.

theorem isPath_advance (q : σ) (a : T) :
    ∀ i, (εnfa φ M).IsPath (advance φ M q a i) (.inl (M.step q a))
      (((φ a).drop (i + 1)).map some)
Uses 4 · Used by 1
Statement usesStates of the homomorphic-image ε-NFA · Next state while spelling out a letter's image · Maximal length of the image of a letter · The ε-NFA for the homomorphic image
Used bySpelling out a letter's image in the image ε-NFA

TheoremSpelling out a letter's image in the image ε-NFA#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(T\) with transition function \(\delta\), and let \(\varphi\) map letters of \(T\) to words over \(T'\). For every state \(q\) of \(M\) and letter \(a\), the ε-NFA of \(M\) and \(\varphi\) has a path from the state \(q\) to the state \(\delta(q, a)\) whose label sequence is a single ε-label if \(\varphi(a)\) is empty, and the letters of \(\varphi(a)\) in order, all non-ε, otherwise.

theorem isPath_code (q : σ) (a : T) :
    (εnfa φ M).IsPath (.inl q) (.inl (M.step q a)) (code φ a)
Uses 6 · Used by 1
Statement usesStates of the homomorphic-image ε-NFA · Maximal length of the image of a letter · Edge labels for a letter's image · The ε-NFA for the homomorphic image
Proof usesNext state while spelling out a letter's image · Finishing a letter's image in the image ε-NFA
Used byHomomorphic images of regular languages over finite alphabets are regular

TheoremSoundness of the homomorphic-image ε-NFA#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(T\) with start state \(q_0\), and let \(\varphi\) map letters of \(T\) to words over \(T'\); for a word \(w\) over \(T\), write \(\varphi(w)\) for the concatenation of the images of its letters. Suppose the ε-NFA of \(M\) and \(\varphi\) has a path from the state \(q_0\) of \(M\) to a state \(u\), with label sequence \(x\), and let \(\bar x\) be the word formed by the non-ε labels of \(x\). If \(u\) is a state \(q\) of \(M\), then there is a word \(w\) over \(T\) on which \(M\) reaches \(q\) from \(q_0\) and \(\varphi(w) = \bar x\). If \(u\) is the intermediate state \((q, a, i)\), then there is a word \(w\) over \(T\) on which \(M\) reaches \(q\) from \(q_0\) and \(\varphi(w)\) followed by the first \(i\) letters of \(\varphi(a)\) (all of \(\varphi(a)\) if it is shorter) equals \(\bar x\).

theorem exists_of_isPath (x : List (Option T')) :
    ∀ u, (εnfa φ M).IsPath (.inl M.start) u x →
      (∀ q, u = .inl q → ∃ w, M.eval w = q ∧ (w.map φ).flatten = x.reduceOption) ∧
      (∀ q a i, u = .inr (q, a, i) →
        ∃ w, M.eval w = q ∧ (w.map φ).flatten ++ (φ a).take i = x.reduceOption)
Uses 4 · Used by 1
Statement usesStates of the homomorphic-image ε-NFA · Maximal length of the image of a letter · The ε-NFA for the homomorphic image
Proof usesNext state while spelling out a letter's image
Used byHomomorphic images of regular languages over finite alphabets are regular

TheoremHomomorphic images of regular languages over finite alphabets are regular#✓fully proved

Let \(T\) be a finite alphabet, \(T'\) an arbitrary (possibly infinite) alphabet, and \(\varphi\) a map from \(T\) to words over \(T'\), extended to words by \(\varphi(a_1 \cdots a_n) = \varphi(a_1) \cdots \varphi(a_n)\). If \(L\) is a regular language over \(T\), then its image \(\{\varphi(w) : w \in L\}\) is a regular language over \(T'\).

theorem IsRegular.homImage {T T' : Type*} [Finite T] {L : Language T} (hL : L.IsRegular)
    (φ : T → List T') : Language.IsRegular ((fun w => (w.map φ).flatten) '' L)
Uses 6
Proof usesStates of the homomorphic-image ε-NFA · Maximal length of the image of a letter · Edge labels for a letter's image · Soundness of the homomorphic-image ε-NFA · Spelling out a letter's image in the image ε-NFA · The ε-NFA for the homomorphic image

DefinitionDFA for the right quotient by a language#✓fully proved

Given a DFA \(M\) over an alphabet \(T\) with state set \(\sigma\) and a language \(R\) over \(T\), this is the DFA with the same states, transition function and start state as \(M\), whose accepting states are the states \(q\) from which some word of \(R\) leads \(M\) to an accepting state of \(M\).

The accepting set is defined by quantifying over \(R\), so it is not computable in general.

def rightDFA (R : Language T) : DFA T σ :=
  ⟨M.step, M.start, {q | ∃ y ∈ R, M.evalFrom q y ∈ M.accept}⟩
Used by 1
Used byRegular languages are closed under right quotients by arbitrary languages

DefinitionNFA for the left quotient by a language#✓fully proved

Given a DFA \(M\) over an alphabet \(T\) with state set \(\sigma\) and a language \(R\) over \(T\), this is the NFA with state set \(\sigma\) and the same accepting states as \(M\), in which from a state \(q\) on a letter \(a\) the only possible move is to the state \(M\) reaches from \(q\) on \(a\), and whose start states are the states that \(M\) reaches from its start state on the words of \(R\).

The set of start states is defined by quantifying over \(R\), so it is not computable in general.

def leftNFA (R : Language T) : NFA T σ where
  step q a := {M.step q a}
  start := {q | ∃ x ∈ R, M.eval x = q}
  accept := M.accept
Used by 1
Used byRegular languages are closed under left quotients by arbitrary languages

TheoremRegular languages are closed under right quotients by arbitrary languages#✓fully proved

If \(L\) is a regular language over an alphabet \(T\) and \(R\) is any language over \(T\), then the right quotient \(\{x \mid \exists y \in R,\ xy \in L\}\) of \(L\) by \(R\) is regular.

theorem IsRegular.rightQuotientSet {L : Language T} (hL : L.IsRegular) (R : Language T) :
    Language.IsRegular ({x | ∃ y ∈ R, x ++ y ∈ L} : Language T)
Uses 1
Proof usesDFA for the right quotient by a language

TheoremRegular languages are closed under left quotients by arbitrary languages#✓fully proved

If \(L\) is a regular language over an alphabet \(T\) and \(R\) is any language over \(T\), then the left quotient \(\{y \mid \exists x \in R,\ xy \in L\}\) of \(L\) by \(R\) is regular.

theorem IsRegular.leftQuotientSet {L : Language T} (hL : L.IsRegular) (R : Language T) :
    Language.IsRegular ({y | ∃ x ∈ R, x ++ y ∈ L} : Language T)
Uses 1
Proof usesNFA for the left quotient by a language

InductiveShuffle of two words#✓fully proved

The relation "\(w\) is a shuffle of \(u\) and \(v\)" on words over \(\alpha\) is defined inductively: the empty word is a shuffle of the empty word and the empty word, and if \(w\) is a shuffle of \(u\) and \(v\), then for every letter \(a\) the word \(aw\) is a shuffle of \(au\) and \(v\), and a shuffle of \(u\) and \(av\). Thus \(w\) interleaves the letters of \(u\) and of \(v\), keeping their order within each word.

inductive IsShuffle : List α → List α → List α → Prop
  | nil : IsShuffle [] [] []
  | left {u v w : List α} (a : α) : IsShuffle u v w → IsShuffle (a :: u) v (a :: w)
  | right {u v w : List α} (a : α) : IsShuffle u v w → IsShuffle u (a :: v) (a :: w)
Used by 2
Used byShuffle of two languages · The shuffle of two regular languages is regular

DefinitionShuffle of two languages#✓fully proved

For languages \(L\) and \(M\) over \(\alpha\), the shuffle of \(L\) and \(M\) is the language of all words \(w\) over \(\alpha\) such that \(w\) is a shuffle of some word \(u \in L\) and some word \(v \in M\), that is, \(w\) interleaves \(u\) and \(v\).

def shuffle (L M : Language α) : Language α :=
  {w | ∃ u ∈ L, ∃ v ∈ M, IsShuffle u v w}
Uses 1 · Used by 1
Statement usesShuffle of two words
Used byThe shuffle of two regular languages is regular

DefinitionCyclic shift of a language#✓fully proved

For a language \(L\) over \(\alpha\), the cyclic shift of \(L\) is the language of all words \(yx\) over \(\alpha\) such that \(xy \in L\) for some words \(x\) and \(y\); that is, the language of all rotations of the words of \(L\).

def cyclicShift (L : Language α) : Language α :=
  {w | ∃ x y, x ++ y ∈ L ∧ w = y ++ x}
Used by 1
Used byThe cyclic shifts of the words of a regular language form a regular language

DefinitionShuffle automaton of two DFAs#✓fully proved

Let \(M\) and \(N\) be DFAs over \(\alpha\) with state types \(\sigma\) and \(\tau\), start states \(s_M\) and \(s_N\), sets of accepting states \(F_M\) and \(F_N\), and transition functions \(\delta_M\) and \(\delta_N\). Their shuffle automaton is the NFA over \(\alpha\) with state type \(\sigma \times \tau\), the single start state \((s_M, s_N)\) and accepting states \(F_M \times F_N\), which on a letter \(a\) moves from a state \((p, q)\) to the two states \((\delta_M(p, a), q)\) and \((p, \delta_N(q, a))\).

def shuffleNFA : NFA α (σ × τ) where
  step s a := {(M.step s.1 a, s.2), (s.1, N.step s.2 a)}
  start := {(M.start, N.start)}
  accept := M.accept ×ˢ N.accept
Used by 1
Used byThe shuffle of two regular languages is regular

DefinitionWords leading a DFA from a state into a set of states#✓fully proved

For a DFA \(M\) over \(\alpha\) with state type \(\sigma\), a state \(p \in \sigma\) and a set \(S \subseteq \sigma\) of states, this is the language of all words \(w\) over \(\alpha\) such that the run of \(M\) started in \(p\) on \(w\) ends in a state of \(S\).

def fromTo (p : σ) (S : Set σ) : Language α :=
  {w | M.evalFrom p w ∈ S}
Used by 1
Used byThe cyclic shifts of the words of a regular language form a regular language

TheoremThe shuffle of two regular languages is regular#✓fully proved

The shuffle of two regular languages is regular.

theorem IsRegular.shuffle {L M : Language α} (hL : L.IsRegular) (hM : M.IsRegular) :
    (Cslib.Language.shuffle L M).IsRegular
Uses 3
Statement usesShuffle of two languages
Proof usesShuffle of two words · Shuffle automaton of two DFAs

TheoremThe cyclic shifts of the words of a regular language form a regular language#✓fully proved

The cyclic shifts of the words of a regular language form a regular language.

theorem IsRegular.cyclicShift {L : Language α} (hL : L.IsRegular) :
    (Cslib.Language.cyclicShift L).IsRegular
Uses 2
Statement usesCyclic shift of a language
Proof usesWords leading a DFA from a state into a set of states

DefinitionSubstitution of languages for letters#✓fully proved

Let \(L\) be a language over an alphabet \(T\), and let \(s\) assign to each letter \(a \in T\) a language \(s(a)\) over an alphabet \(T'\). The substitution of \(s\) into \(L\) is the language over \(T'\) of all words \(y_1 y_2 \cdots y_n\) for which there is a word \(a_1 a_2 \cdots a_n \in L\) with \(y_i \in s(a_i)\) for every \(i\).

def substitution (L : Language T) (s : T → Language T') : Language T' :=
  {y | ∃ x ∈ L, y ∈ (x.map s).prod}
Used by 3
Used byContext-free languages are closed under substitution by context-free languages · Intended languages of the substitution grammar · Regular languages are closed under substitution over a finite alphabet

DefinitionThe ε-NFA for a substitution#✓fully proved

Let \(M\) be a DFA over \(T\) with states \(\sigma\), and for each letter \(a \in T\) let \(N_a\) be a DFA over \(T'\) with states \(\tau_a\). This ε-NFA over \(T'\) has as states the states \(q\) of \(M\) and the triples \((q, a, p)\) with \(q\) a state of \(M\), \(a \in T\) and \(p\) a state of \(N_a\), read as the state \(p\) of the copy of \(N_a\) entered from \(q\). A state \(q\) of \(M\) has an ε-move to \((q, a, s_a)\) for every \(a \in T\), where \(s_a\) is the start state of \(N_a\), and no letter moves. A state \((q, a, p)\) moves on a letter \(b\) to \((q, a, \delta_a(p, b))\), where \(\delta_a\) is the transition function of \(N_a\), and has an ε-move, to the state \(\delta_M(q, a)\) of \(M\), exactly when \(p\) is an accepting state of \(N_a\); here \(\delta_M\) is the transition function of \(M\). The start state is the start state of \(M\), and the accepting states are the accepting states of \(M\).

def εnfa : εNFA T' (σ ⊕ (σ × Σ a, τ a)) where
  step
    | .inl q, none => {s | ∃ a, s = .inr (q, ⟨a, (N a).start⟩)}
    | .inl _, some _ => ∅
    | .inr (q, ⟨a, p⟩), some b => {.inr (q, ⟨a, (N a).step p b⟩)}
    | .inr (q, ⟨a, p⟩), none => {s | p ∈ (N a).accept ∧ s = .inl (M.step q a)}
  start := {.inl M.start}
  accept := {s | ∃ q ∈ M.accept, s = .inl q}
Used by 3
Used bySoundness of the paths of the substitution ε-NFA · Paths inside one copy of a letter automaton · Regular languages are closed under substitution over a finite alphabet

TheoremPaths inside one copy of a letter automaton#✓fully proved

Let \(M\) be a DFA over \(T\), and for each letter \(a \in T\) let \(N_a\) be a DFA over \(T'\). For every state \(q\) of \(M\), letter \(a \in T\), state \(p\) of \(N_a\) and word \(y\) over \(T'\), the ε-NFA built from \(M\) and the \(N_a\) has a path reading the letters of \(y\), with no ε-moves, from the state \(p\) of the copy of \(N_a\) entered from \(q\) to the state of the same copy that \(N_a\) reaches from \(p\) on \(y\).

theorem isPath_run (q : σ) (a : T) (p : τ a) (y : List T') :
    (εnfa M N).IsPath (.inr (q, ⟨a, p⟩)) (.inr (q, ⟨a, (N a).evalFrom p y⟩)) (y.map some)
Uses 1 · Used by 1
Statement usesThe ε-NFA for a substitution
Used byRegular languages are closed under substitution over a finite alphabet

DefinitionDetour labels#✓fully proved

For a word \(y = b_1 \cdots b_n\) over \(T'\), the detour labels of \(y\) are the sequence of ε-NFA labels \(\varepsilon, b_1, \ldots, b_n, \varepsilon\): an ε-move, the letters of \(y\) in order, and a final ε-move.

They label the detour that the substitution ε-NFA takes through a copy of the automaton for one letter.

def detour (y : List T') : List (Option T') :=
  none :: (y.map some ++ [none])
Used by 1
Used byRegular languages are closed under substitution over a finite alphabet

TheoremSoundness of the paths of the substitution ε-NFA#✓fully proved

Let \(M\) be a DFA over \(T\) with start state \(q_0\), and for each letter \(a \in T\) let \(N_a\) be a DFA over \(T'\), with accepted language \(L(N_a)\); for a word \(w = a_1 \cdots a_n\) over \(T\) write \(L_w = L(N_{a_1}) \cdots L(N_{a_n})\), which is \(\{\varepsilon\}\) when \(w\) is empty. Let \(x\) be a sequence of labels, each a letter of \(T'\) or \(\varepsilon\), let \(\bar x\) be the word over \(T'\) obtained from \(x\) by deleting the \(\varepsilon\)'s, and suppose the ε-NFA built from \(M\) and the \(N_a\) has a path reading \(x\) from the state \(q_0\) of \(M\) to a state \(u\). If \(u\) is a state \(q\) of \(M\), then there is a word \(w\) over \(T\) such that \(M\) reaches \(q\) from \(q_0\) on \(w\) and \(\bar x \in L_w\). If \(u\) is the state \(p\) of the copy of \(N_a\) entered from the state \(q\) of \(M\), then there are a word \(w\) over \(T\) such that \(M\) reaches \(q\) from \(q_0\) on \(w\), a word \(y_1 \in L_w\) and a word \(y_2\) over \(T'\) such that \(\bar x = y_1 y_2\) and \(N_a\) reaches \(p\) from its start state on \(y_2\).

theorem exists_of_isPath (x : List (Option T')) :
    ∀ u, (εnfa M N).IsPath (.inl M.start) u x →
      (∀ q, u = .inl q →
        ∃ w, M.eval w = q ∧ x.reduceOption ∈ (w.map fun a => (N a).accepts).prod) ∧
      (∀ q a p, u = .inr (q, ⟨a, p⟩) →
        ∃ w, M.eval w = q ∧ ∃ y₁ ∈ (w.map fun a => (N a).accepts).prod, ∃ y₂,
          x.reduceOption = y₁ ++ y₂ ∧ (N a).evalFrom (N a).start y₂ = p)
Uses 1 · Used by 1
Statement usesThe ε-NFA for a substitution
Used byRegular languages are closed under substitution over a finite alphabet

TheoremRegular languages are closed under substitution over a finite alphabet#✓fully proved

Let \(T\) be a finite alphabet and \(T'\) any alphabet. If \(L\) is a regular language over \(T\) and \(s(a)\) is a regular language over \(T'\) for every letter \(a \in T\), then the substitution of \(s\) into \(L\) is a regular language over \(T'\).

theorem IsRegular.substitution {T T' : Type*} [Finite T] {L : Language T} (hL : L.IsRegular)
    {s : T → Language T'} (hs : ∀ a, (s a).IsRegular) :
    (Cslib.Language.substitution L s).IsRegular
Uses 5
Statement usesSubstitution of languages for letters
Proof usesDetour labels · Soundness of the paths of the substitution ε-NFA · Paths inside one copy of a letter automaton · The ε-NFA for a substitution
26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.