Strictly piecewise languages (SP_k)

A language L is strictly k-piecewise when membership is determined by which length-k subsequences (scattered, non-contiguous selections) the input contains. Where SL_k constrains adjacent material via contiguous factors, SP_k constrains long-distance co-occurrence via subsequences — so no boundary augmentation is needed (subsequences are blind to position).

Main definitions

• Subregular.SPGrammar α — a set of permitted subsequences; the width k is supplied to language, not baked into the carrier.
• Subregular.SPGrammar.language k — the Language α it generates: every length-k subsequence of w must be permitted.
• Language.IsStrictlyPiecewise L k — L is strictly k-piecewise.

Implementation notes

List.Sublist (<+) is mathlib's non-contiguous "is a subsequence of", exactly the SP primitive.

@[reducible, inline]

abbrev Subregular.SPGrammar (α : Type u_2) : Type u_2

A strictly-piecewise grammar over α: a set of permitted subsequences. 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

• Subregular.SPGrammar α = Set (List α)

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

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

Equations

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

@[simp]

theorem Subregular.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 Subregular.SPGrammar.mem_language_iff_forall_sublists {α : Type u_1} (k : ℕ) (G : SPGrammar α) (w : List α) : w ∈ language k G ↔ ∀ s ∈ w.sublists, s.length = k → s ∈ G

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

@[implicit_reducible]

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

Equations

• Subregular.SPGrammar.decidableMemLanguage k G w = decidable_of_iff (∀ s ∈ w.sublists, s.length = k → s ∈ G) ⋯

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

A language L is strictly k-piecewise iff some SPGrammar α generates it at width k.

Equations

• L.IsStrictlyPiecewise k = ∃ (G : Subregular.SPGrammar α), Subregular.SPGrammar.language k G = L