Locally Testable Languages (LT_k, LTT_{k,t})

A language L is locally k-testable when membership depends only on which length-k factors occur in the boundary-augmented form of the input — ignoring order and multiplicity @cite{rogers-pullum-2011} @cite{lambert-2022}. The threshold-testable variant LTT_{k,t} relaxes "ignoring multiplicity" to "saturating multiplicities at threshold t": LT counts only presence vs absence (t = 1), LTT_{k,t} counts up to t and treats anything beyond as "≥ t".

Both are property-based (extensional) classifications — there is no canonical grammar, only an indistinguishability relation on strings: w₁ ~_LT w₂ iff their k-factor sets coincide. L is LT_k iff it is closed under ~_LT.

Main definitions

• factorSet k w — the set of k-factors of boundary k w.
• IsLocallyTestable k L — closure of L under equality of factorSet.
• factorCount k t f w — multiplicity of f in boundary k w, capped at t.
• IsLocallyThresholdTestable k t L — closure under equality of factorCount.

Inclusions

The cast lemma IsStrictlyLocal k L → IsLocallyTestable k L lives at the end of the file (the larger-class file holds the cast, mathlib-style). The companion cast LT_k ⊆ LTT_{k,t} for t ≥ 1 lives inside the DecidableEq-scoped section with IsLocallyThresholdTestable.

def Core.Computability.Subregular.factorSet {α : Type u_1} (k : ℕ) (w : List α) : Set (Augmented α)

The set of k-factors of the boundary-augmented form of w. The LT indistinguishability relation w₁ ~_LT w₂ is exactly equality of factorSet k w₁ and factorSet k w₂.

Equations

• Core.Computability.Subregular.factorSet k w = {f : Core.Computability.Subregular.Augmented α | f ∈ Core.Computability.Subregular.kFactors k (Core.Computability.Subregular.boundary k w)}

@[simp]

theorem Core.Computability.Subregular.mem_factorSet {α : Type u_1} {k : ℕ} {f : Augmented α} {w : List α} : f ∈ factorSet k w ↔ f ∈ kFactors k (boundary k w)

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

A language is locally k-testable iff strings with the same set of k-factors are either both in L or both out.

Equations

• Core.Computability.Subregular.IsLocallyTestable k L = ∀ (w₁ w₂ : List α), Core.Computability.Subregular.factorSet k w₁ = Core.Computability.Subregular.factorSet k w₂ → (w₁ ∈ L ↔ w₂ ∈ L)

theorem Core.Computability.Subregular.IsStrictlyLocal.toIsLocallyTestable {α : Type u_1} {k : ℕ} {L : Language α} (h : IsStrictlyLocal k L) : IsLocallyTestable k L

SL_k ⊆ LT_k: every strictly-k-local language is locally k-testable. The SL test ("every factor is permitted") trivially depends only on the set of factors, not their order or multiplicity.

def Core.Computability.Subregular.factorCount {α : Type u_1} [DecidableEq α] (k t : ℕ) (f : Augmented α) (w : List α) : ℕ

Saturated multiplicity: how many times factor f occurs in w's boundary-augmented form, capped at threshold t. The cap is what makes LTT a finite test even on infinite-input families.

Equations

• Core.Computability.Subregular.factorCount k t f w = min t (List.count f (Core.Computability.Subregular.kFactors k (Core.Computability.Subregular.boundary k w)))

def Core.Computability.Subregular.IsLocallyThresholdTestable {α : Type u_1} [DecidableEq α] (k t : ℕ) (L : Language α) : Prop

A language is locally (k,t)-threshold-testable iff strings with the same t-saturated factor counts agree on membership. Specializing to t = 1 recovers IsLocallyTestable (presence vs absence of each factor).

Equations

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

theorem Core.Computability.Subregular.IsLocallyTestable.toIsLocallyThresholdTestable {α : Type u_1} [DecidableEq α] {k t : ℕ} (ht : 1 ≤ t) {L : Language α} (h : IsLocallyTestable k L) : IsLocallyThresholdTestable k t L

LT_k ⊆ LTT_{k,t} for t ≥ 1. A factor occurs in w iff its saturated count is positive, so closure under count-equivalence implies closure under set-equivalence.