Strictly piecewise languages (SP_k)

A language L is strictly k-piecewise when membership is determined by which subsequences (scattered, non-contiguous selections) of length at most k the input contains. Where SL_k constrains adjacent material via contiguous factors, SP_k constrains long-distance co-occurrence — the subregular class of unbounded-distance phonotactics. The class is the program's vocabulary for the sublist-closed languages of Linglib.Core.Computability.ShuffleIdeal: a language is SP at some width iff it is sublist-closed.

Main definitions

• StrictlyPiecewiseGrammar α: a set of permitted subsequences; the width k is supplied to language, not baked into the carrier.
• StrictlyPiecewiseGrammar.language k: the Language α it generates: every subsequence of w of length at most k must be permitted.
• Language.IsStrictlyPiecewise L k: L is a fixed point of the width-k test with itself as grammar; isStrictlyPiecewise_iff recovers the ∃-grammar form.

Main results

• Language.IsStrictlyPiecewise.mem_of_sublist: SP languages are subsequence-closed.
• Language.IsStrictlyPiecewise.preimage_map: SP languages are closed under inverse images of letter-to-letter maps.
• Language.IsStrictlyPiecewise.succ: SP_k ⊆ SP_(k+1).
• Language.IsStrictlyPiecewise.toIsPiecewiseTestable: SP_k ⊆ PT_k.
• Language.IsStrictlyPiecewise.isStarFree: SP_k ⊆ SF over a finite alphabet.
• Language.isStrictlyPiecewise_avoid: shuffle-ideal complements are SP.
• Language.exists_isStrictlyPiecewise_iff_isSublistClosed: SP at some width is exactly sublist-closure.

Implementation notes

List.Sublist (<+) is mathlib's non-contiguous "is a subsequence of", exactly the SP primitive. Unlike SL no boundary augmentation is needed, since subsequences are blind to position; the "≤ k" (rather than "exactly k") bound is instead what keeps words shorter than k distinguishable, matching subseqSet.

References

• [RHB+10]

@[reducible, inline]

abbrev StrictlyPiecewiseGrammar (α : Type u_1) : Type u_1

A strictly-piecewise grammar over α is a set of permitted subsequences. Unlike SL grammars it uses no boundary alphabet, since subsequences are insensitive to position. The width k is an argument of language.

Equations

• StrictlyPiecewiseGrammar α = Set (List α)

def StrictlyPiecewiseGrammar.language {α : Type u_1} (k : ℕ) (G : StrictlyPiecewiseGrammar α) : Language α

The language generated at width k consists of the strings whose every subsequence of length at most k is permitted.

Equations

• StrictlyPiecewiseGrammar.language k G = {w : List α | ∀ (s : List α), s.length ≤ k → s.Sublist w → s ∈ G}

@[simp]

theorem StrictlyPiecewiseGrammar.mem_language {α : Type u_1} (k : ℕ) (G : StrictlyPiecewiseGrammar α) (w : List α) : w ∈ language k G ↔ ∀ (s : List α), s.length ≤ k → s.Sublist w → s ∈ G

theorem StrictlyPiecewiseGrammar.mem_language_of_sublist {α : Type u_1} {k : ℕ} {G : StrictlyPiecewiseGrammar α} {v w : List α} (hvw : v.Sublist w) (hw : w ∈ language k G) : v ∈ language k G

SP languages are subsequence-closed: deleting symbols cannot create a subsequence that was not already there.

theorem StrictlyPiecewiseGrammar.language_inter {α : Type u_1} (k : ℕ) (G₁ G₂ : StrictlyPiecewiseGrammar α) : language k (G₁ ∩ G₂) = language k G₁ ⊓ language k G₂

Conjoining grammars conjoins their languages.

theorem StrictlyPiecewiseGrammar.language_preimage_map {α : Type u_1} {β : Type u_2} (k : ℕ) (G : StrictlyPiecewiseGrammar α) (f : β → α) : language k (List.map f ⁻¹' G) = List.map f ⁻¹' language k G

The grammar of the subsequences whose images are permitted generates the preimage of the language under a letter-to-letter map.

theorem StrictlyPiecewiseGrammar.mem_language_iff_forall_mem_sublistsLen {α : Type u_1} (k : ℕ) (G : StrictlyPiecewiseGrammar α) (w : List α) : w ∈ language k G ↔ ∀ j ≤ k, ∀ s ∈ List.sublistsLen j w, s ∈ G

SP membership reduces to a check against List.sublistsLen — a decide-friendly characterisation used by the decidable-membership instance below.

@[instance_reducible]

instance StrictlyPiecewiseGrammar.decidableMemLanguage {α : Type u_1} (k : ℕ) (G : StrictlyPiecewiseGrammar α) [DecidablePred fun (x : List α) => x ∈ G] (w : List α) : Decidable (w ∈ language k G)

Equations

• StrictlyPiecewiseGrammar.decidableMemLanguage k G w = decidable_of_iff' (∀ j ≤ k, ∀ s ∈ List.sublistsLen j w, s ∈ G) ⋯

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

A language L is strictly k-piecewise when the width-k subsequence test with L itself as the permitted set recovers L — the canonical-grammar fixed point; isStrictlyPiecewise_iff recovers the ∃-grammar form.

Equations

• L.IsStrictlyPiecewise k = (StrictlyPiecewiseGrammar.language k L = L)

theorem Language.isStrictlyPiecewise_iff {α : Type u_1} {L : Language α} {k : ℕ} : L.IsStrictlyPiecewise k ↔ ∃ (G : StrictlyPiecewiseGrammar α), StrictlyPiecewiseGrammar.language k G = L

Some grammar generates L at width k iff L is its own grammar.

theorem Language.IsStrictlyPiecewise.preimage_map {α : Type u_1} {L : Language α} {k : ℕ} {β : Type u_2} (h : L.IsStrictlyPiecewise k) (f : β → α) : IsStrictlyPiecewise (List.map f ⁻¹' L) k

Strictly piecewise languages are closed under inverse images of letter-to-letter maps.

theorem Language.IsStrictlyPiecewise.mem_of_sublist {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsStrictlyPiecewise k) {v w : List α} (hvw : v.Sublist w) (hw : w ∈ L) : v ∈ L

SP languages are subsequence-closed.

theorem Language.IsStrictlyPiecewise.nil_mem {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsStrictlyPiecewise k) {w : List α} (hw : w ∈ L) : [] ∈ L

A nonempty SP language contains the empty word.

theorem Language.isStrictlyPiecewise_avoid {α : Type u_1} {k : ℕ} {p : List α} (hp : p.length ≤ k) : (shuffleIdeal p)ᶜ.IsStrictlyPiecewise k

The complement of a shuffle ideal is strictly k-piecewise as soon as the forbidden pattern fits in the window.

theorem Language.IsStrictlyPiecewise.succ {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsStrictlyPiecewise k) : L.IsStrictlyPiecewise (k + 1)

Widening the window loses nothing, SP_k ⊆ SP_(k+1).

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

The strictly-piecewise test, that every subsequence of length at most k is permitted, depends only on subseqSet k, so SP_k ⊆ PT_k.

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

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

theorem Language.isPiecewiseTestable_compl_shuffleIdeal {α : Type u_1} {k : ℕ} {p : List α} (hp : p.length ≤ k) : (shuffleIdeal p)ᶜ.IsPiecewiseTestable k

Avoiding one pattern that fits in the window is piecewise testable.

theorem Language.isPiecewiseTestable_shuffleIdeal {α : Type u_1} {k : ℕ} {p : List α} (hp : p.length ≤ k) : (shuffleIdeal p).IsPiecewiseTestable k

Containing one pattern that fits in the window is piecewise testable.

theorem Language.exists_isStrictlyPiecewise_iff_isSublistClosed {α : Type u_1} {L : Language α} [Finite α] : (∃ (k : ℕ), L.IsStrictlyPiecewise k) ↔ L.IsSublistClosed

A language is strictly piecewise at some width iff it is sublist-closed [RHB+10]. Backwards, L is its own grammar at the width bounding the finite forbidden basis, so that any word outside L is already refuted by a basis word it contains.