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 @cite{rogers-pullum-2011} @cite{lambert-2022}. Whereas SL_k constrains adjacent material via factors (contiguous infixes), SP_k constrains long-distance co-occurrence via subsequences.

Why subsequences (not factors)

The two locality dimensions in the subregular hierarchy are adjacency-based (SL/LT/LTT, captured by contiguous k-factors) and precedence-based (SP/SP-tier, captured by k-element subsequences). A long-distance phonological pattern such as sibilant harmony — sasi but not saʃi — is naturally SP_2: the forbidden length-2 subsequence is [s, ʃ] (and its reverse), regardless of intervening material.

No boundary augmentation is needed for SP: subsequences are blind to position and to symbols not in the subsequence itself, so leading and trailing markers add no information. This is the canonical convention in Heinz's SP work @cite{heinz-rogers-2010}.

Main definitions

• SPGrammar k α — a positive k-piecewise grammar over alphabet α.
• SPGrammar.lang — the Language α it generates: every length-k subsequence of w must be permitted.
• IsStrictlyPiecewise k L — the property that a Language α is strictly k-piecewise.

The relation List.Sublist (<+) is mathlib's "is a (non-contiguous) subsequence of" — exactly what SP needs.

structure Core.Computability.Subregular.SPGrammar (k : ℕ) (α : Type u_2) : Type u_2

A strictly k-piecewise grammar over α: a set of permitted length-k subsequences. Unlike SL grammars, no boundary alphabet is used — subsequences are insensitive to position.

• permitted : Set (List α)

  The set of permitted length-k subsequences.

theorem Core.Computability.Subregular.SPGrammar.ext {k : ℕ} {α : Type u_2} {x y : SPGrammar k α} (permitted : x.permitted = y.permitted) : x = y

theorem Core.Computability.Subregular.SPGrammar.ext_iff {k : ℕ} {α : Type u_2} {x y : SPGrammar k α} : x = y ↔ x.permitted = y.permitted

@[implicit_reducible]

instance Core.Computability.Subregular.SPGrammar.instInhabited {α : Type u_1} {k : ℕ} : Inhabited (SPGrammar k α)

Equations

• Core.Computability.Subregular.SPGrammar.instInhabited = { default := { permitted := Set.univ } }

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

The language generated by an SP grammar: strings whose every length-k subsequence is permitted.

Equations

• G.lang w = ∀ (s : List α), s.length = k → s.Sublist w → s ∈ G.permitted

@[simp]

theorem Core.Computability.Subregular.SPGrammar.mem_lang {α : Type u_1} {k : ℕ} (G : SPGrammar k α) (w : List α) : w ∈ G.lang ↔ ∀ (s : List α), s.length = k → s.Sublist w → s ∈ G.permitted

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

A language L is strictly k-piecewise iff some SPGrammar k α generates exactly L.

Equations

• Core.Computability.Subregular.IsStrictlyPiecewise k L = ∃ (G : Core.Computability.Subregular.SPGrammar k α), G.lang = L

theorem Core.Computability.Subregular.SPGrammar.isStrictlyPiecewise_lang {α : Type u_1} {k : ℕ} (G : SPGrammar k α) : IsStrictlyPiecewise k G.lang

Every SP grammar witnesses IsStrictlyPiecewise for its language.

theorem Core.Computability.Subregular.SPGrammar.mem_lang_iff_forall_sublists {α : Type u_1} {k : ℕ} (G : SPGrammar k α) (w : List α) : w ∈ G.lang ↔ ∀ s ∈ w.sublists, s.length = k → s ∈ G.permitted

SP membership reduces to a check against List.sublists. Used by the decidable-membership instance below and by cross-framework comparisons that need a decide-friendly characterisation.

@[implicit_reducible]

instance Core.Computability.Subregular.SPGrammar.decidableMemLang {α : Type u_1} {k : ℕ} (G : SPGrammar k α) [DecidablePred fun (x : List α) => x ∈ G.permitted] (w : List α) : Decidable (w ∈ G.lang)

Equations

• G.decidableMemLang w = decidable_of_iff (∀ s ∈ w.sublists, s.length = k → s ∈ G.permitted) ⋯