Locally testable languages

A language is locally k-testable when membership of a word depends only on its prefix and suffix of length k - 1 and on the set of its factors of length k. Over all k these are the locally testable events of McNaughton and Papert.

Main definitions

• List.kTestVector k w: the prefix of w of length k - 1, the set of its factors of length k, and its suffix of length k - 1.
• Language.IsLocallyTestable: membership in the language factors through List.kTestVector k.

Main results

• List.kTestVector_append_congr: words with the same k-test vectors have concatenations with the same k-test vector.
• Language.IsLocallyTestable.isStarFree: over a finite alphabet, locally testable languages are star-free, and with them the generalized definite and the finite or cofinite languages.
• Language.IsLocallyTestable.leftQuotient, Language.IsLocallyTestable.rightQuotient, Language.IsLocallyTestable.preimage_map: closure under quotients and under inverse images of letter-to-letter maps.
• Language.isStarFree_setOf_infix: the words containing a given factor form a star-free language, over any alphabet.

Implementation notes

The name is McNaughton and Papert's, the convention Pin's. McNaughton and Papert take the two ends at length k and only the interior factors, and leave words shorter than k unconstrained. Here the ends have length k - 1 and every factor counts, so that a factor crossing the seam of a concatenation lies in the suffix of one word followed by the prefix of the other.

References

• [McNP71]
• [Pin]

def List.kTestVector {α : Type u_1} (k : ℕ) (w : List α) : List α × Set (List α) × List α

The k-test vector of w is its prefix of length k - 1, the set of its factors of length k, and its suffix of length k - 1.

Equations

• List.kTestVector k w = (Edge.left.takeAt (k - 1) w, {f : List α | f ∈ List.kFactors k w}, Edge.right.takeAt (k - 1) w)

theorem List.kTestVector_append_congr {α : Type u_1} {k : ℕ} {u u' v v' : List α} (hu : kTestVector k u = kTestVector k u') (hv : kTestVector k v = kTestVector k v') : kTestVector k (u ++ v) = kTestVector k (u' ++ v')

Words with the same k-test vectors have concatenations with the same k-test vector, since a factor across the seam lies in the suffix of one word followed by the prefix of the other.

theorem List.kTestVector_map {α : Type u_1} {β : Type u_2} {k : ℕ} (g : α → β) (w : List α) : kTestVector k (map g w) = Prod.map (map g) (Prod.map (Set.image (map g)) (map g)) (kTestVector k w)

Mapping a function over a word maps it over the k-test vector.

theorem List.kTestVector_flatten_replicate_succ {α : Type u_1} (k : ℕ) (w : List α) : kTestVector k (replicate (k + 1) w).flatten = kTestVector k (replicate k w).flatten

k + 1 copies of a word have the same k-test vector as k copies, since a factor of length k reaches across at most k consecutive copies.

theorem List.finite_range_kTestVector {α : Type u_1} [Finite α] (k : ℕ) : (Set.range (kTestVector k)).Finite

Over a finite alphabet List.kTestVector k takes finitely many values.

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

A language is locally k-testable when membership factors through the prefix and suffix of length k - 1 and the set of factors of length k.

Equations

• L.IsLocallyTestable k = Function.FactorsThrough (fun (x : List α) => x ∈ L) (List.kTestVector k)

theorem Language.IsLocallyTestable.compl {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsLocallyTestable k) : Lᶜ.IsLocallyTestable k

theorem Language.IsLocallyTestable.inter {α : Type u_1} {L M : Language α} {k : ℕ} (hL : L.IsLocallyTestable k) (hM : M.IsLocallyTestable k) : (L ⊓ M).IsLocallyTestable k

theorem Language.IsLocallyTestable.union {α : Type u_1} {L M : Language α} {k : ℕ} (hL : L.IsLocallyTestable k) (hM : M.IsLocallyTestable k) : (L ⊔ M).IsLocallyTestable k

theorem Language.isLocallyTestable_setOf_kFactors {α : Type u_1} (k : ℕ) (P : Set (Set (List α))) : IsLocallyTestable {w : List α | {f : List α | f ∈ List.kFactors k w} ∈ P} k

The words whose set of factors of length k lies in a given family form a locally k-testable language.

theorem Language.IsLocallyTestable.leftQuotient {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsLocallyTestable k) (u : List α) : (L.leftQuotient u).IsLocallyTestable k

theorem Language.IsLocallyTestable.rightQuotient {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsLocallyTestable k) (u : List α) : (L.rightQuotient u).IsLocallyTestable k

theorem Language.IsLocallyTestable.preimage_map {α : Type u_1} {β : Type u_2} {k : ℕ} {L : Language β} (h : L.IsLocallyTestable k) (g : α → β) : IsLocallyTestable (List.map g ⁻¹' L) k

Locally testable languages are closed under inverse images of letter-to-letter maps.

theorem Language.IsLocallyTestable.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsLocallyTestable k) : L.IsStarFree

Over a finite alphabet locally testable languages are star-free.

Generalized definite languages

theorem Language.IsGeneralizedDefinite.toIsLocallyTestable {α : Type u_1} {L : Language α} {k : ℕ} (h : L.IsGeneralizedDefinite k) : L.IsLocallyTestable (k + 1)

A generalized k-definite language is locally (k + 1)-testable.

theorem Language.IsGeneralizedDefinite.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsGeneralizedDefinite k) : L.IsStarFree

Over a finite alphabet generalized definite languages are star-free.

theorem Language.IsDefinite.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsDefinite k) : L.IsStarFree

theorem Language.IsReverseDefinite.isStarFree {α : Type u_1} {L : Language α} {k : ℕ} [Finite α] (h : L.IsReverseDefinite k) : L.IsStarFree

theorem Language.IsFiniteOrCofinite.isStarFree {α : Type u_1} {L : Language α} [Finite α] (h : L.IsFiniteOrCofinite) : L.IsStarFree

Over a finite alphabet finite and cofinite languages are star-free.

Containing a factor

theorem Language.isLocallyTestable_setOf_infix {α : Type u_1} (c : List α) : IsLocallyTestable {w : List α | c <:+: w} c.length

The words containing c as a factor form a locally testable language.

theorem Language.isStarFree_setOf_infix {α : Type u_1} (c : List α) : IsStarFree {w : List α | c <:+: w}

The words containing c as a factor form a star-free language over any alphabet, finite or not.