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 [RHB+10]. 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

• SPGrammar α: a set of permitted subsequences; the width k is supplied to language, not baked into the carrier.
• SPGrammar.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.succ: SP_k ⊆ SP_(k+1).
• Language.IsStrictlyPiecewise.toIsPiecewiseTestable: SP_k ⊆ PT_k.
• Language.isStrictlyPiecewise_avoid: shuffle-ideal complements are SP.
• Language.exists_isStrictlyPiecewise_iff_isSublistClosed: SP at some width is exactly sublist-closure [RHB+10].

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.

@[reducible, inline]

abbrev SPGrammar (α : Type u_1) : Type u_1

A strictly-piecewise grammar over α: a set of permitted subsequences [RHB+10]. Unlike SL grammars no boundary alphabet is used — subsequences are insensitive to position. The width k is supplied to language, not baked into the carrier.

Equations

• SPGrammar α = Set (List α)

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

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

Equations

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

@[simp]

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

theorem SPGrammar.mem_language_of_sublist {α : Type u_1} {k : ℕ} {G : SPGrammar α} {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 SPGrammar.language_inter {α : Type u_1} (k : ℕ) (G₁ G₂ : SPGrammar α) : language k (G₁ ∩ G₂) = language k G₁ ⊓ language k G₂

Conjoining grammars conjoins their languages.

theorem SPGrammar.mem_language_iff_forall_mem_sublistsLen {α : Type u_1} (k : ℕ) (G : SPGrammar α) (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 SPGrammar.decidableMemLanguage {α : Type u_1} (k : ℕ) (G : SPGrammar α) [DecidablePred fun (x : List α) => x ∈ G] (w : List α) : Decidable (w ∈ language k G)

Equations

• SPGrammar.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 = (SPGrammar.language k L = L)

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

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

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

Avoiding one pattern: 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)

SP_k ⊆ SP_(k+1): widening the window loses nothing.

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

SP_k ⊆ PT_k: the strictly-piecewise test ("every subsequence of length at most k is permitted") depends only on subseqSet k.

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.