Piecewise testable languages (PT_k)

A language is piecewise k-testable when its membership depends only on the set of length-≤ k subsequences (scattered subwords) of the input [Sim75] — i.e. membership factors through the map subseqSet k, the piecewise analogue of locally testable.

Main definitions

• subseqSet k w: the subsequences of w of length ≤ k.
• Language.IsPiecewiseTestable L k: Function.FactorsThrough (· ∈ L) (subseqSet k).

Main results

• subseqSet_append_congr: sharing subseqSet k is a congruence for concatenation.
• Language.IsPiecewiseTestable.compl / .inter / .union: boolean closure.
• Language.IsPiecewiseTestable.isRegular: over a finite alphabet PT languages are regular.

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

The subsequences of w of length at most k. The "≤ k" (rather than "exactly k") bound is what keeps strings shorter than k 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₂

Subsequences of length at most k are interchangeable across strings sharing their subseqSet k. The ratchet for proving piecewise testability from a predicate depending only on length-≤ k subsequence presence.

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 a congruence for concatenation: a subsequence of u ++ v splits as a subsequence of u followed by one of v, each transferable separately.

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

Over a finite alphabet subseqSet k takes finitely many values: the piecewise congruence has finite index.

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

A language is piecewise k-testable: membership factors through the length-≤ k subsequence set subseqSet k.

Equations

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

theorem Language.isPiecewiseTestable_iff {α : Type u_2} {L : Language α} {k : ℕ} : L.IsPiecewiseTestable k ↔ ∀ (w₁ w₂ : List α), subseqSet k w₁ = subseqSet k w₂ → (w₁ ∈ L ↔ w₂ ∈ L)

Pointwise form: strings with equal subseqSet k are L-equivalent.

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

Piecewise testable languages are closed under complement.

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

Piecewise testable languages are closed under intersection.

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

Piecewise testable languages are closed under union.

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

Over a finite alphabet piecewise testable languages are regular: left quotients factor through the finitely many values of subseqSet k.