Piecewise testable languages

A language is piecewise k-testable when membership of a word depends only on the set of its subsequences of length at most k. These are the piecewise testable events of Simon.

Main definitions

• subseqSet k w: the subsequences of w of length at most k.
• Language.IsPiecewiseTestable: membership in the language factors through subseqSet k.

Main results

• subseqSet_append_congr: words with the same subsequences of length at most k still have the same ones after concatenation.
• subseqSet_flatten_replicate_succ: k + 1 copies of a word have the same subsequences of length at most k as k copies.
• Language.IsPiecewiseTestable.isStarFree: over a finite alphabet, piecewise testable languages are star-free.

References

• [Sim75]

def subseqSet {α : Type u_1} (k : ℕ) (w : List α) : Set (List α)

The subsequences of w of length at most k. The bound is at most k, not exactly k, so that words shorter than k stay distinguishable.

Equations

• subseqSet k w = {s : List α | s.Sublist w ∧ s.length ≤ k}

@[simp]

theorem mem_subseqSet {α : Type u_1} {k : ℕ} {s w : List α} : s ∈ subseqSet k w ↔ s.Sublist w ∧ s.length ≤ k

theorem subseqSet_eq_iff {α : Type u_1} {k : ℕ} {w₁ w₂ : List α} (heq : subseqSet k w₁ = subseqSet k w₂) {s : List α} (hlen : s.length ≤ k) : s.Sublist w₁ ↔ s.Sublist w₂

Words with the same subseqSet k have the same subsequences of length at most k.

theorem subseqSet_append_congr {α : Type u_1} {k : ℕ} {u₁ u₂ v₁ v₂ : List α} (hu : subseqSet k u₁ = subseqSet k u₂) (hv : subseqSet k v₁ = subseqSet k v₂) : subseqSet k (u₁ ++ v₁) = subseqSet k (u₂ ++ v₂)

Sharing subseqSet k is preserved by concatenation, since a subsequence of u ++ v splits as a subsequence of u followed by one of v.

theorem List.sublist_flatten_replicate_of_length_le {α : Type u_1} {w : List α} {m : ℕ} {s : List α} : s.length ≤ m → s.Sublist (replicate (m + 1) w).flatten → s.Sublist (replicate m w).flatten

A subsequence of m + 1 copies of w that is no longer than m misses one of the copies, so it is a subsequence of m copies.

theorem subseqSet_flatten_replicate_succ {α : Type u_1} (k : ℕ) (w : List α) : subseqSet k (List.replicate (k + 1) w).flatten = subseqSet k (List.replicate k w).flatten

k + 1 copies of a word have the same subsequences of length at most k as k copies.

theorem finite_range_subseqSet {α : Type u_1} [Finite α] (k : ℕ) : (Set.range (subseqSet k)).Finite

Over a finite alphabet subseqSet k takes finitely many values.

def Language.IsPiecewiseTestable {α : Type u_1} (L : Language α) (k : ℕ) : Prop

A language is piecewise k-testable when membership factors through the set subseqSet k of subsequences of length at most k.

Equations

• L.IsPiecewiseTestable k = Function.FactorsThrough (fun (x : List α) => x ∈ L) (subseqSet k)

theorem Language.IsPiecewiseTestable.compl {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsPiecewiseTestable k) : Lᶜ.IsPiecewiseTestable k

theorem Language.IsPiecewiseTestable.inter {α : Type u_1} {L M : Language α} {k : ℕ} (hL : L.IsPiecewiseTestable k) (hM : M.IsPiecewiseTestable k) : (L ⊓ M).IsPiecewiseTestable k

theorem Language.IsPiecewiseTestable.union {α : Type u_1} {L M : Language α} {k : ℕ} (hL : L.IsPiecewiseTestable k) (hM : M.IsPiecewiseTestable k) : (L ⊔ M).IsPiecewiseTestable k

theorem Language.IsPiecewiseTestable.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsPiecewiseTestable k) : L.IsStarFree

Over a finite alphabet piecewise testable languages are star-free.

theorem Language.IsPiecewiseTestable.isRegular {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsPiecewiseTestable k) : L.IsRegular