Word models

A word model is a word as a relational structure: its positions, each carrying the labels of its symbol, related by an ordering of the positions. In the conventional model a symbol is its own one label; in a feature-labelled model, Chandlee, Eyraud, Heinz, Jardine and Rawski's for segments, it carries the values of its features, so that a position of a factor stands for a natural class. Two orderings recover the two strict classes of stringsets as strictly local sets of word models. Under precedence, a factor occurring in a word occurs in the subsequence its occurrence picks out, and a subsequence is itself a factor, its positive diagram, so the strictly local sets are the strictly piecewise stringsets. Under successor, the covering relation of the positions, an occurrence of a k-factor spans fewer than k steps, so it misses one side of any k - 1 symbols, and the strictly local sets of words between their edges are the strictly local stringsets. Relativizing successor to a tier, by restricting a word to its tier positions and taking successor there, gives the successor model of the word's projection, so the strictly local sets of relativized models are the tier-based strictly local stringsets. A set is locally testable when membership depends only on the set of factors; under successor the factors of a word are fixed by the infixes of at most k symbols of the word between its edges, and these by its k-test vector, and under precedence by its subsequences of at most k symbols.

Main definitions

• Subregular.wordLanguage: the signature of word models, a unary relation for each label and an ordering.
• Subregular.Labelling: the labels a symbol carries, itself alone in the conventional model and the values of its features in a feature-labelled one.
• Subregular.WordModel: a word under an ordering of its positions.
• Subregular.anchor: a word between its edges.

Main statements

• Language.isStrictlyLocal_iff_wordModel, Language.isLocallyTestable_iff_wordModel: the strictly local and locally testable stringsets are the strictly local and locally testable sets of words between their edges under successor.
• Language.isStrictlyPiecewise_iff_wordModel, Language.isPiecewiseTestable_iff_wordModel: the strictly piecewise and piecewise testable stringsets are those of words under precedence.
• Language.isTierStrictlyLocal_iff_wordModel: the tier-based strictly local stringsets are the strictly local sets of words under successor relativized to a tier.
• Subregular.WordModel.diagram_occurs_iff_forall₂, Subregular.WordModel.succDiagram_occurs_iff_forall₂: a word's diagram occurs under precedence, respectively successor, exactly in the words with a subsequence, respectively infix, whose positions carry its labels; for words of segments this is subsumption, position by position.

Implementation notes

• An ordering is a relation on the positions passed to WordModel, so precedence is WordModel w (· < ·) and successor WordModel (anchor w) (· ⋖ ·).
• As in Rogers and Lambert's word models, the edges carry their own labels and are not related to themselves. The strictly local stringsets pad a word with k - 1 boundary symbols instead, and the two classes differ only at k = 1, where the word models also forbid every word; the locally testable classes agree at every k.

References

• [RL19]
• [RP11]
• [RHB+10]
• [Lam23]
• [CEH+19]

inductive Subregular.WordRel (α : Type u) : ℕ → Type u

The relation symbols of word models, a unary label for each symbol and a binary ordering.

• label {α : Type u} (a : α) : WordRel α 1
• ord {α : Type u} : WordRel α 2

def Subregular.wordLanguage (α : Type u) : FirstOrder.Language

The signature of word models over α.

Equations

• Subregular.wordLanguage α = { Functions := fun (x : ℕ) => Empty, Relations := Subregular.WordRel α }

instance Subregular.instIsRelationalWordLanguage {α : Type u} : (wordLanguage α).IsRelational

class Subregular.Labelling (β : Type u_1) (P : Type u_2) : Type (max u_1 u_2)

The labels a symbol carries in word models whose unary relations are P.

• labels : β → Set P

  The labels of a symbol.

@[instance_reducible]

instance Subregular.instLabelling (β : Type u_1) : Labelling β β

In the conventional model a symbol is its own one label.

Equations

• Subregular.instLabelling β = { labels := fun (b : β) => {b} }

@[simp]

theorem Subregular.Labelling.labels_self {β : Type u_1} (b : β) : labels b = {b}

def Subregular.WordModel {β : Type u_1} (u : List β) : (Fin u.length → Fin u.length → Prop) → Type

The word model of u under an ordering R of its positions, each position labelled by its symbol.

Equations

• Subregular.WordModel u x✝ = Fin u.length

@[instance_reducible]

instance Subregular.WordModel.instLinearOrder {β : Type u_1} {u : List β} {R : Fin u.length → Fin u.length → Prop} : LinearOrder (WordModel u R)

Equations

• One or more equations did not get rendered due to their size.

def Subregular.WordModel.toFin {β : Type u_1} {u : List β} {R : Fin u.length → Fin u.length → Prop} (i : WordModel u R) : Fin u.length

A position, as an index into the word.

Equations

• i.toFin = i

def Subregular.WordModel.label {β : Type u_1} {u : List β} {R : Fin u.length → Fin u.length → Prop} (i : WordModel u R) : β

The symbol at a position.

Equations

• i.label = u.get i

@[instance_reducible]

instance Subregular.WordModel.instStructureWordLanguage {β : Type u_1} {u : List β} {R : Fin u.length → Fin u.length → Prop} {P : Type u_2} [Labelling β P] : (wordLanguage P).Structure (WordModel u R)

A position satisfies the unary relations of the labels its symbol carries.

Equations

• One or more equations did not get rendered due to their size.

theorem Subregular.WordModel.mem_realizers_of_subset {β : Type u_1} {u u' : List β} {R : Fin u.length → Fin u.length → Prop} {R' : Fin u'.length → Fin u'.length → Prop} {P : Type u_2} [Labelling β P] {n : ℕ} {T : Set ((wordLanguage P).Atom (Fin n))} {v : Fin n → WordModel u R} {v' : Fin n → WordModel u' R'} (hlabel : ∀ (x : Fin n), Labelling.labels (v x).label ⊆ Labelling.labels (v' x).label) (hord : ∀ (x y : Fin n), R (v x) (v y) → R' (v' x) (v' y)) (hv : v ∈ FirstOrder.Language.Atom.realizers (WordModel u R) T) : v' ∈ FirstOrder.Language.Atom.realizers (WordModel u' R') T

An assignment realizes the atoms another does when each of its positions carries the labels of the other's and it keeps the ordering between its variables.

theorem Subregular.WordModel.mem_realizers_of {β : Type u_1} {u u' : List β} {R : Fin u.length → Fin u.length → Prop} {R' : Fin u'.length → Fin u'.length → Prop} {P : Type u_2} [Labelling β P] {n : ℕ} {T : Set ((wordLanguage P).Atom (Fin n))} {v : Fin n → WordModel u R} {v' : Fin n → WordModel u' R'} (hlabel : ∀ (x : Fin n), (v' x).label = (v x).label) (hord : ∀ (x y : Fin n), R (v x) (v y) → R' (v' x) (v' y)) (hv : v ∈ FirstOrder.Language.Atom.realizers (WordModel u R) T) : v' ∈ FirstOrder.Language.Atom.realizers (WordModel u' R') T

An assignment realizes the atoms another does when it reads the same symbols and keeps the ordering between its variables.

Precedence

theorem Subregular.WordModel.factors_subset_of_sublist {α : Type u} {P : Type u_2} {w w' : List α} [Labelling α P] {k : ℕ} (h : w.Sublist w') : (wordLanguage P).factors k (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) ⊆ (wordLanguage P).factors k (WordModel w' fun (x1 x2 : Fin w'.length) => x1 < x2)

The factors of a subsequence occur in the word.

theorem Subregular.WordModel.exists_sublist_of_occurs {α : Type u} {P : Type u_2} {w : List α} [Labelling α P] {k : ℕ} {f : (wordLanguage P).Factor k} (hf : FirstOrder.Language.Factor.Occurs (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) f) : ∃ (s : List α), s.Sublist w ∧ s.length ≤ k ∧ FirstOrder.Language.Factor.Occurs (WordModel s fun (x1 x2 : Fin s.length) => x1 < x2) f

A factor occurring in a word occurs in the subsequence its occurrence picks out, which has no more symbols than the factor has variables.

def Subregular.WordModel.diagram {α : Type u} (P : Type u_3) [Labelling α P] (s : List α) {k : ℕ} (hs : s.length ≤ k) : (wordLanguage P).Factor k

The positive diagram of a word of at most k symbols under precedence, as a k-factor of the labels P: every atom its positions satisfy.

Equations

• Subregular.WordModel.diagram P s hs = { n := s.length, le := hs, atoms := {a : (Subregular.wordLanguage P).Atom (Fin s.length) | a.Realize id}, preconnected := ⋯ }

theorem Subregular.WordModel.diagram_occurs_iff_forall₂ {α : Type u} {P : Type u_2} {w : List α} [Labelling α P] {s : List α} {k : ℕ} (hs : s.length ≤ k) : FirstOrder.Language.Factor.Occurs (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) (diagram P s hs) ↔ ∃ (t : List α), t.Sublist w ∧ List.Forall₂ (fun (a b : α) => Labelling.labels a ⊆ Labelling.labels b) s t

The diagram of a word occurs exactly in the words with a subsequence whose positions carry its labels, position by position.

theorem Subregular.WordModel.diagram_occurs_iff {α : Type u} {w s : List α} {k : ℕ} (hs : s.length ≤ k) : FirstOrder.Language.Factor.Occurs (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) (diagram α s hs) ↔ s.Sublist w

The diagram of a word occurs exactly in the words of which it is a subsequence.

theorem Subregular.WordModel.diagram_singleton_occurs_iff {α : Type u} {P : Type u_2} {w : List α} [Labelling α P] {d : α} {k : ℕ} (hk : [d].length ≤ k) : FirstOrder.Language.Factor.Occurs (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) (diagram P [d] hk) ↔ ∃ x ∈ w, Labelling.labels d ⊆ Labelling.labels x

A one-position diagram occurs exactly in the words with a symbol carrying its labels.

theorem Subregular.WordModel.factors_subset_of_subseqSet_subset {α : Type u} {w w' : List α} {k : ℕ} (h : subseqSet k w ⊆ subseqSet k w') : (wordLanguage α).factors k (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) ⊆ (wordLanguage α).factors k (WordModel w' fun (x1 x2 : Fin w'.length) => x1 < x2)

The factors of a word under precedence are those of its subsequences of at most k symbols.

theorem Subregular.WordModel.factors_eq_iff_subseqSet {α : Type u} {w w' : List α} {k : ℕ} : (wordLanguage α).factors k (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) = (wordLanguage α).factors k (WordModel w' fun (x1 x2 : Fin w'.length) => x1 < x2) ↔ subseqSet k w = subseqSet k w'

Two words have the same factors under precedence exactly when they have the same subsequences of at most k symbols.

Feature-labelled models

A position may carry several properties, the values of features, as in Chandlee, Eyraud, Heinz, Jardine and Rawski's unconventional models. A word of partial valuations ι → Flat V, such as a word of segments, has a unary relation for each feature value, holding at the positions with that value, so a position never has two values of one feature and may have none. Under precedence the diagram of such a word occurs exactly in the words with a subsequence lying above it position by position, and a natural class is a one-position factor.

@[instance_reducible]

instance Subregular.WordModel.instLabellingForallFlatProd {ι : Type u_3} {V : Type u_4} : Labelling (ι → Flat V) (ι × V)

A partial valuation, such as a segment, carries the values it gives its features.

Equations

• Subregular.WordModel.instLabellingForallFlatProd = { labels := fun (s : ι → Flat V) => {p : ι × V | s p.1 = ↑p.2} }

theorem Subregular.WordModel.labels_subset_labels_iff {ι : Type u_3} {V : Type u_4} {s t : ι → Flat V} : Labelling.labels s ⊆ Labelling.labels t ↔ s ≤ t

A valuation carries the labels of another exactly when it lies above it.

theorem Subregular.WordModel.diagram_occurs_iff_forall₂_le {ι : Type u_3} {V : Type u_4} {s w : List (ι → Flat V)} {k : ℕ} (hs : s.length ≤ k) : FirstOrder.Language.Factor.Occurs (WordModel w fun (x1 x2 : Fin w.length) => x1 < x2) (diagram (ι × V) s hs) ↔ ∃ (t : List (ι → Flat V)), t.Sublist w ∧ List.Forall₂ (fun (x1 x2 : ι → Flat V) => x1 ≤ x2) s t

Under feature-labelled precedence models the diagram of a word occurs exactly in the words with a subsequence lying above it position by position.

Orderings with unit steps

theorem Subregular.WordModel.le_add_one_of_adj {β : Type u_1} {u : List β} {R : Fin u.length → Fin u.length → Prop} {P : Type u_2} [Labelling β P] {n : ℕ} {T : Set ((wordLanguage P).Atom (Fin n))} {r : Fin n → WordModel u R} (hR : ∀ (a b : Fin u.length), R a b → ↑a ≤ ↑b + 1 ∧ ↑b ≤ ↑a + 1) (hr : r ∈ FirstOrder.Language.Atom.realizers (WordModel u R) T) {x y : Fin n} (h : (FirstOrder.Language.Atom.gaifman T).Adj x y) : ↑(r x).toFin ≤ ↑(r y).toFin + 1

Variables an atom relates are at most one position apart, when the ordering takes unit steps.

theorem Subregular.WordModel.le_add_of_occurs {β : Type u_1} {u : List β} {R : Fin u.length → Fin u.length → Prop} {P : Type u_2} [Labelling β P] {k : ℕ} {f : (wordLanguage P).Factor k} (hR : ∀ (a b : Fin u.length), R a b → ↑a ≤ ↑b + 1 ∧ ↑b ≤ ↑a + 1) {r : Fin f.n → WordModel u R} (hr : r ∈ FirstOrder.Language.Atom.realizers (WordModel u R) f.atoms) (x y : Fin f.n) : ↑(r x).toFin ≤ ↑(r y).toFin + (k - 1)

An occurrence of a k-factor spans at most k - 1 positions, when the ordering takes unit steps.

Successor

theorem Subregular.WordModel.covBy_unit {m : ℕ} (a b : Fin m) (h : a ⋖ b) : ↑a ≤ ↑b + 1 ∧ ↑b ≤ ↑a + 1

Successor between positions takes unit steps.

theorem Subregular.WordModel.factors_subset_of_infix {β : Type u_1} {P : Type u_2} [Labelling β P] {k : ℕ} {c u : List β} (h : c <:+: u) : (wordLanguage P).factors k (WordModel c fun (x1 x2 : Fin c.length) => x1 ⋖ x2) ⊆ (wordLanguage P).factors k (WordModel u fun (x1 x2 : Fin u.length) => x1 ⋖ x2)

The factors of an infix occur in the word under successor.

theorem Subregular.WordModel.exists_infix_of_occurs {β : Type u_1} {P : Type u_2} [Labelling β P] {k : ℕ} {u : List β} {f : (wordLanguage P).Factor k} (hf : FirstOrder.Language.Factor.Occurs (WordModel u fun (x1 x2 : Fin u.length) => x1 ⋖ x2) f) : ∃ (c : List β), c <:+: u ∧ c.length ≤ k ∧ FirstOrder.Language.Factor.Occurs (WordModel c fun (x1 x2 : Fin c.length) => x1 ⋖ x2) f

An occurrence of a k-factor under successor lies in an infix of at most k symbols, the window it spans.

def Subregular.WordModel.succDiagram {β : Type u_1} (P : Type u_3) [Labelling β P] (c : List β) {k : ℕ} (hc : c.length ≤ k) : (wordLanguage P).Factor k

The diagram of a word under successor, as a k-factor of the labels P: the path of its positions, each carrying the labels of its symbol.

Equations

• Subregular.WordModel.succDiagram P c hc = { n := c.length, le := hc, atoms := {a : (Subregular.wordLanguage P).Atom (Fin c.length) | a.Realize id}, preconnected := ⋯ }

theorem Subregular.WordModel.succDiagram_occurs_iff_forall₂ {β : Type u_1} {P : Type u_2} [Labelling β P] {c u : List β} {k : ℕ} (hc : c.length ≤ k) : FirstOrder.Language.Factor.Occurs (WordModel u fun (x1 x2 : Fin u.length) => x1 ⋖ x2) (succDiagram P c hc) ↔ ∃ (t : List β), t <:+: u ∧ List.Forall₂ (fun (a b : β) => Labelling.labels a ⊆ Labelling.labels b) c t

The successor diagram of a word occurs exactly in the words with an infix whose positions carry its labels, position by position.

theorem Subregular.WordModel.succDiagram_occurs_iff {β : Type u_1} {c u : List β} {k : ℕ} (hc : c.length ≤ k) : FirstOrder.Language.Factor.Occurs (WordModel u fun (x1 x2 : Fin u.length) => x1 ⋖ x2) (succDiagram β c hc) ↔ c <:+: u

The diagram of a word occurs under successor exactly in the words of which it is an infix.

theorem Subregular.WordModel.factors_eq_iff_infix {β : Type u_1} {k : ℕ} {u u' : List β} : (wordLanguage β).factors k (WordModel u fun (x1 x2 : Fin u.length) => x1 ⋖ x2) = (wordLanguage β).factors k (WordModel u' fun (x1 x2 : Fin u'.length) => x1 ⋖ x2) ↔ {c : List β | c <:+: u ∧ c.length ≤ k} = {c : List β | c <:+: u' ∧ c.length ≤ k}

Two words have the same factors under successor exactly when they have the same infixes of at most k symbols.

Anchored words

def Subregular.anchor {α : Type u} (w : List α) : List (α ⊕ Edge)

The word w between its edges, ⋊ w ⋉.

Equations

• Subregular.anchor w = Sum.inr Edge.left :: (List.map Sum.inl w ++ [Sum.inr Edge.right])

@[simp]

theorem Subregular.length_anchor {α : Type u} (w : List α) : (anchor w).length = w.length + 2

theorem Subregular.infix_of_map_inl_infix_anchor {α : Type u} {s v : List α} (h : List.map Sum.inl s <:+: anchor v) : s <:+: v

The symbols of a word occurring together in an anchored word occur together in the word.

theorem Subregular.prefix_of_infix_anchor {α : Type u} {s v : List α} (h : Sum.inr Edge.left :: List.map Sum.inl s <:+: anchor v) : s <+: v

An infix of an anchored word starting at its left edge reads a prefix of the word.

theorem Subregular.suffix_of_infix_anchor {α : Type u} {s v : List α} (h : List.map Sum.inl s ++ [Sum.inr Edge.right] <:+: anchor v) : s <:+ v

An infix of an anchored word ending at its right edge reads a suffix of the word.

theorem Subregular.eq_of_anchor_infix_anchor {α : Type u} {v w : List α} (h : anchor w <:+: anchor v) : w = v

An anchored word is an infix of another only when the words are equal.

theorem Subregular.getElem_anchor_append_of_le {α : Type u} {p q q' : List α} {i : ℕ} (hi : i ≤ p.length) (h₁ : i < (anchor (p ++ q)).length) (h₂ : i < (anchor (p ++ q')).length) : (anchor (p ++ q))[i] = (anchor (p ++ q'))[i]

Anchored words agree up to the end of a common prefix.

theorem Subregular.getElem_anchor_append_of_ge {α : Type u} {l l' p p' q : List α} (hl : l = p ++ q) (hl' : l' = p' ++ q) {i i' : ℕ} (hi : p.length + 1 ≤ i) (hi' : i' = i - p.length + p'.length) (h₁ : i < (anchor l).length) (h₂ : i' < (anchor l').length) : (anchor l)[i] = (anchor l')[i']

Anchored words agree from the start of a common suffix.

theorem Subregular.map_inl_infix_anchor_iff {α : Type u} {s v : List α} : List.map Sum.inl s <:+: anchor v ↔ s <:+: v

theorem Subregular.cons_infix_anchor_iff {α : Type u} {s v : List α} : Sum.inr Edge.left :: List.map Sum.inl s <:+: anchor v ↔ s <+: v

theorem Subregular.append_infix_anchor_iff {α : Type u} {s v : List α} : List.map Sum.inl s ++ [Sum.inr Edge.right] <:+: anchor v ↔ s <:+ v

theorem Subregular.infix_anchor_cases {α : Type u} {v : List α} {c : List (α ⊕ Edge)} (h : c <:+: anchor v) : ∃ (s : List α), c = List.map Sum.inl s ∨ c = Sum.inr Edge.left :: List.map Sum.inl s ∨ c = List.map Sum.inl s ++ [Sum.inr Edge.right] ∨ c = anchor s

Every infix of an anchored word is the image of an infix of the word, possibly preceded by the left edge and followed by the right edge.

Locally testable stringsets

theorem Subregular.kTestVector_eq_iff {α : Type u} {w v : List α} {k : ℕ} : List.kTestVector k w = List.kTestVector k v ↔ {c : List (α ⊕ Edge) | c <:+: anchor w ∧ c.length ≤ k} = {c : List (α ⊕ Edge) | c <:+: anchor v ∧ c.length ≤ k}

Two words have the same k-test vector exactly when their anchored words have the same infixes of at most k symbols.

Strictly local stringsets

theorem Subregular.factors_crossover_subset {α : Type u} {u₁ v₁ u₂ v₂ x : List α} {k : ℕ} (hx : x.length = k - 1) : (wordLanguage (α ⊕ Edge)).factors k (WordModel (anchor (u₁ ++ x ++ v₂)) fun (x1 x2 : Fin (anchor (u₁ ++ x ++ v₂)).length) => x1 ⋖ x2) ⊆ (wordLanguage (α ⊕ Edge)).factors k (WordModel (anchor (u₁ ++ x ++ v₁)) fun (x1 x2 : Fin (anchor (u₁ ++ x ++ v₁)).length) => x1 ⋖ x2) ∪ (wordLanguage (α ⊕ Edge)).factors k (WordModel (anchor (u₂ ++ x ++ v₂)) fun (x1 x2 : Fin (anchor (u₂ ++ x ++ v₂)).length) => x1 ⋖ x2)

A factor of u₁ x v₂, with k - 1 symbols in x, is a factor of u₁ x v₁ or of u₂ x v₂: an occurrence spans at most k - 1 positions, so it misses u₁ or v₂.

theorem Subregular.mem_of_factors_subset_biUnion {α : Type u} {k : ℕ} {L : Language α} (hL : L.SuffixSubstitutionClosed k) (hk : 2 ≤ k) {w : List α} (hw : (wordLanguage (α ⊕ Edge)).factors k (WordModel (anchor w) fun (x1 x2 : Fin (anchor w).length) => x1 ⋖ x2) ⊆ ⋃ v ∈ L, (wordLanguage (α ⊕ Edge)).factors k (WordModel (anchor v) fun (x1 x2 : Fin (anchor v).length) => x1 ⋖ x2)) : w ∈ L

A suffix-substitution-closed stringset contains every word whose factors under successor all occur in its members: the word is rebuilt from members a symbol at a time.

theorem Language.isStrictlyPiecewise_iff_wordModel {α : Type u} {L : Language α} {k : ℕ} : L.IsStrictlyPiecewise k ↔ (Subregular.wordLanguage α).IsStrictlyLocal (fun (x : List α) => Subregular.WordModel x fun (x1 x2 : Fin x.length) => x1 < x2) k L

A stringset is strictly k-piecewise exactly when it is a strictly k-local set of precedence models.

theorem Language.isStrictlyLocal_iff_wordModel {α : Type u} {L : Language α} {k : ℕ} (hk : 2 ≤ k) : L.IsStrictlyLocal k ↔ (Subregular.wordLanguage (α ⊕ Edge)).IsStrictlyLocal (fun (w : List α) => Subregular.WordModel (Subregular.anchor w) fun (x1 x2 : Fin (Subregular.anchor w).length) => x1 ⋖ x2) k L

A stringset is strictly k-local, for 2 ≤ k, exactly when it is a strictly k-local set of anchored words ordered by successor.

theorem Language.isTierStrictlyLocal_iff_wordModel {α : Type u} {L : Language α} {k : ℕ} (hk : 2 ≤ k) : IsTierStrictlyLocal k L ↔ ∃ (T : α → Prop) (x : DecidablePred T), (Subregular.wordLanguage (α ⊕ Edge)).IsStrictlyLocal (fun (w : List α) => Subregular.WordModel (Subregular.anchor (List.filter (fun (x_1 : α) => decide (T x_1)) w)) fun (x1 x2 : Fin (Subregular.anchor (List.filter (fun (x_1 : α) => decide (T x_1)) w)).length) => x1 ⋖ x2) k L

A stringset is tier-based strictly k-local, for 2 ≤ k, exactly when for some tier it is a strictly k-local set of words under successor relativized to the tier. Restricting a word to its tier positions and taking successor there gives the successor model of its projection, so the relativized models are those of the projections.

theorem Language.isPiecewiseTestable_iff_wordModel {α : Type u} {L : Language α} {k : ℕ} : L.IsPiecewiseTestable k ↔ (Subregular.wordLanguage α).IsLocallyTestable (fun (x : List α) => Subregular.WordModel x fun (x1 x2 : Fin x.length) => x1 < x2) k L

A stringset is piecewise k-testable exactly when it is a locally k-testable set of words under precedence.

theorem Language.isLocallyTestable_iff_wordModel {α : Type u} {L : Language α} {k : ℕ} : L.IsLocallyTestable k ↔ (Subregular.wordLanguage (α ⊕ Edge)).IsLocallyTestable (fun (w : List α) => Subregular.WordModel (Subregular.anchor w) fun (x1 x2 : Fin (Subregular.anchor w).length) => x1 ⋖ x2) k L

A stringset is locally k-testable exactly when it is a locally k-testable set of words between their edges under successor.