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. PT_k is the Boolean closure of SP_k, the piecewise analogue of locally testable over strictly local.

Main definitions

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

Main results

• Language.IsStrictlyPiecewise.toIsPiecewiseTestable — SP_k ⊆ PT_k.
• Closure under complement comes from Function.FactorsThrough.comp_left.

def Subregular.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

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

@[simp]

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

theorem Subregular.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.

def Language.IsPiecewiseTestable {α : Type u_1} (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) (Subregular.subseqSet k)

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

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

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

SP_k ⊆ PT_k: the strictly-piecewise test ("every length-k subsequence is permitted") depends only on the set of subsequences of that length.