Shuffle ideals and sublist-closed languages

The shuffle ideal of a word w is the language {v | w <+ v} of words containing w as a subsequence, and a language is sublist-closed when it is downward closed under the sublist order. This file proves that shuffle ideals are regular, and that over a finite alphabet a sublist-closed language is the complement of finitely many shuffle ideals (by Higman's lemma [Hig52]) and hence regular (Haines' theorem).

Main definitions

• Language.shuffleIdeal w: the words containing w as a subsequence.
• Language.IsSublistClosed L: L is downward closed under <+.
• List.maxMatch w x: the length of the longest prefix of w occurring as a subsequence of x.

Main results

• Language.isRegular_shuffleIdeal: shuffle ideals are regular.
• Language.IsSublistClosed.exists_finset_compl_eq_biSup_shuffleIdeal: the finite forbidden basis.
• Language.IsSublistClosed.isRegular: Haines' theorem.

Shuffle ideals

def Language.shuffleIdeal {α : Type u_1} (w : List α) : Language α

The shuffle ideal of w: the words admitting w as a subsequence. Also called the principal shuffle ideal of w, or the simple language Σ*a₁Σ* ⋯ aₙΣ* over w = a₁ ⋯ aₙ in the piecewise-testable literature.

Equations

• Language.shuffleIdeal w = {v : List α | w.Sublist v}

@[simp]

theorem Language.mem_shuffleIdeal {α : Type u_1} {v w : List α} : v ∈ shuffleIdeal w ↔ w.Sublist v

theorem Language.self_mem_shuffleIdeal {α : Type u_1} (w : List α) : w ∈ shuffleIdeal w

@[simp]

theorem Language.shuffleIdeal_nil {α : Type u_1} : shuffleIdeal [] = ⊤

theorem Language.shuffleIdeal_append {α : Type u_1} (w v : List α) : shuffleIdeal (w ++ v) = shuffleIdeal w * shuffleIdeal v

shuffleIdeal carries concatenation to language product.

theorem Language.shuffleIdeal_singleton {α : Type u_1} (a : α) : shuffleIdeal [a] = ⊤ * {[a]} * ⊤

theorem Language.top_mul_shuffleIdeal {α : Type u_1} (w : List α) : ⊤ * shuffleIdeal w = shuffleIdeal w

Shuffle ideals are two-sided ideals: they absorb ⊤ on either side.

theorem Language.shuffleIdeal_mul_top {α : Type u_1} (w : List α) : shuffleIdeal w * ⊤ = shuffleIdeal w

theorem Language.shuffleIdeal_cons {α : Type u_1} (a : α) (w : List α) : shuffleIdeal (a :: w) = ⊤ * {[a]} * shuffleIdeal w

theorem Language.shuffleIdeal_eq_prod {α : Type u_1} (w : List α) : shuffleIdeal w = ⊤ * (List.map (fun (a : α) => {[a]} * ⊤) w).prod

The classical regular-expression description of the shuffle ideal of a₁ ⋯ aₙ: Σ*a₁Σ* ⋯ aₙΣ*.

theorem Language.shuffleIdeal_le_shuffleIdeal {α : Type u_1} {v w : List α} : shuffleIdeal w ≤ shuffleIdeal v ↔ v.Sublist w

theorem Language.shuffleIdeal_injective {α : Type u_1} : Function.Injective shuffleIdeal

Sublist-closed languages

def Language.IsSublistClosed {α : Type u_1} (L : Language α) : Prop

A language is sublist-closed when deleting symbols never leaves it.

Equations

• L.IsSublistClosed = ∀ ⦃v w : List α⦄, v.Sublist w → w ∈ L → v ∈ L

theorem Language.IsSublistClosed.mem_compl_of_sublist {α : Type u_1} {L : Language α} (hL : L.IsSublistClosed) {v w : List α} (hvw : v.Sublist w) (hv : v ∈ Lᶜ) : w ∈ Lᶜ

theorem Language.isSublistClosed_compl_shuffleIdeal {α : Type u_1} (w : List α) : (shuffleIdeal w)ᶜ.IsSublistClosed

theorem Language.isSublistClosed_iff_shuffleIdeal_le {α : Type u_1} {L : Language α} : L.IsSublistClosed ↔ ∀ w ∈ Lᶜ, shuffleIdeal w ≤ Lᶜ

theorem Language.isSublistClosed_top {α : Type u_1} : ⊤.IsSublistClosed

theorem Language.isSublistClosed_bot {α : Type u_1} : ⊥.IsSublistClosed

theorem Language.IsSublistClosed.inf {α : Type u_1} {L M : Language α} (hL : L.IsSublistClosed) (hM : M.IsSublistClosed) : (L ⊓ M).IsSublistClosed

theorem Language.IsSublistClosed.sup {α : Type u_1} {L M : Language α} (hL : L.IsSublistClosed) (hM : M.IsSublistClosed) : (L ⊔ M).IsSublistClosed

theorem Language.isSublistClosed_iInf {α : Type u_1} {ι : Sort u_2} {L : ι → Language α} (h : ∀ (i : ι), (L i).IsSublistClosed) : (⨅ (i : ι), L i).IsSublistClosed

theorem Language.isSublistClosed_iSup {α : Type u_1} {ι : Sort u_2} {L : ι → Language α} (h : ∀ (i : ι), (L i).IsSublistClosed) : (⨆ (i : ι), L i).IsSublistClosed

Greedy matching

def List.maxMatch {α : Type u_1} [DecidableEq α] (w x : List α) : ℕ

The length of the longest prefix of w occurring as a subsequence of x.

Equations

• w.maxMatch x = Nat.findGreatest (fun (m : ℕ) => (List.take m w).Sublist x) w.length

theorem List.maxMatch_le {α : Type u_1} [DecidableEq α] (w x : List α) : w.maxMatch x ≤ w.length

theorem List.take_maxMatch_sublist {α : Type u_1} [DecidableEq α] (w x : List α) : (take (w.maxMatch x) w).Sublist x

theorem List.le_maxMatch {α : Type u_1} [DecidableEq α] {w x : List α} {j : ℕ} (hj : j ≤ w.length) (h : (take j w).Sublist x) : j ≤ w.maxMatch x

theorem List.sublist_append_iff_drop_maxMatch {α : Type u_1} [DecidableEq α] (w x v : List α) : w.Sublist (x ++ v) ↔ (drop (w.maxMatch x) w).Sublist v

Greedy matching is optimal: w scatters into x ++ v exactly when the part of w left over after its longest x-matchable prefix scatters into v.

Regularity of shuffle ideals

theorem Language.leftQuotient_shuffleIdeal {α : Type u_1} [DecidableEq α] (w x : List α) : (shuffleIdeal w).leftQuotient x = shuffleIdeal (List.drop (w.maxMatch x) w)

theorem Language.isRegular_shuffleIdeal {α : Type u_1} (w : List α) : (shuffleIdeal w).IsRegular

A shuffle ideal is regular: its left quotients are the shuffle ideals of the suffixes of w, of which there are at most |w| + 1, so Myhill–Nerode applies.

The finite forbidden basis

theorem Language.IsSublistClosed.exists_finset_compl_eq_biSup_shuffleIdeal {α : Type u_1} {L : Language α} [Finite α] (hL : L.IsSublistClosed) : ∃ (F : Finset (List α)), Lᶜ = ⨆ m ∈ F, shuffleIdeal m

Finite forbidden basis: over a finite alphabet a sublist-closed language is avoidance of finitely many forbidden subsequences — the finite-basis property of well-quasi-orders (WellQuasiOrdered.exists_finset_eq_biUnion) at Higman's lemma.

theorem DFA.accepts_eq_biSup_shuffleIdeal {α : Type u_1} {σ : Type u_2} (M : DFA α σ) [Fintype σ] (h : ∀ ⦃v w : List α⦄, v.Sublist w → v ∈ M.accepts → w ∈ M.accepts) : M.accepts = ⨆ w ∈ {w : List α | w ∈ M.accepts ∧ w.length ≤ Fintype.card σ}, Language.shuffleIdeal w

Effective basis: a superlist-closed language recognised by a DFA is generated by its members of length at most the state count, with no appeal to Higman's lemma — pumping a shortest long member yields a shorter member below it.

Haines' theorem

theorem Language.isRegular_bot {α : Type u_1} : ⊥.IsRegular

theorem Language.isRegular_biSup {α : Type u_1} {ι : Type u_2} (F : Finset ι) {f : ι → Language α} (hf : ∀ i ∈ F, (f i).IsRegular) : (⨆ i ∈ F, f i).IsRegular

theorem Language.IsSublistClosed.isRegular {α : Type u_1} {L : Language α} [Finite α] (hL : L.IsSublistClosed) : L.IsRegular

Haines' theorem: over a finite alphabet every sublist-closed language is regular. It is the complement of the finitely many shuffle ideals of its minimal forbidden subsequences, and each of those is regular.