Definite languages

A language L is k-definite when membership is decided by the last k symbols of a word [RP11] [Lam22a]: any two words sharing their length-k suffix are L-equivalent. Reverse k-definite (RD_k) is the dual through the length-k prefix, and generalized k-definite (Lambert's ℒℐ_k) tests prefix and suffix jointly [Lam26].

Main definitions

• Subregular.Edge and Subregular.Edge.takeAt — a string edge and its length-k substring (right = suffix, left = prefix).
• Language.IsDefinite, Language.IsReverseDefinite, Language.IsGeneralizedDefinite — membership factoring through the suffix, prefix, and joint edge projections.
• Language.IsFiniteOrCofinite — Lambert's 𝒩: L or its complement is finite.

Main theorems

• Language.IsDefinite.toIsGeneralizedDefinite and Language.IsReverseDefinite.toIsGeneralizedDefinite — D_k, RD_k ⊆ ℒℐ_k.
• Language.isFiniteOrCofinite_iff_exists_isDefinite_and_isReverseDefinite — over a finite alphabet, 𝒩 = 𝒟 ∩ 𝒦 [Pin]: a language is finite-or-cofinite iff it is definite and reverse-definite.

Edge projections

inductive Subregular.Edge : Type

Which edge of the string the definite test inspects. right gives classical D_k (final substring); left gives RD_k (initial substring).

• left : Edge
• right : Edge

@[implicit_reducible]

instance Subregular.instDecidableEqEdge : DecidableEq Edge

Equations

• Subregular.instDecidableEqEdge x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Subregular.instReprEdge.repr : Edge → ℕ → Std.Format

Equations

• Subregular.instReprEdge.repr Subregular.Edge.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.Edge.left")).group prec✝
• Subregular.instReprEdge.repr Subregular.Edge.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Subregular.Edge.right")).group prec✝

@[implicit_reducible]

instance Subregular.instReprEdge : Repr Edge

Equations

• Subregular.instReprEdge = { reprPrec := Subregular.instReprEdge.repr }

def Subregular.Edge.takeAt {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : List α

Take the length-k substring at this edge of xs: left is the length-k prefix List.take, right the length-k suffix List.rtake. Strings shorter than k are returned in full.

Equations

• Subregular.Edge.left.takeAt k xs = List.take k xs
• Subregular.Edge.right.takeAt k xs = xs.rtake k

@[simp]

theorem Subregular.Edge.takeAt_left {α : Type u_1} (k : ℕ) (xs : List α) : left.takeAt k xs = List.take k xs

@[simp]

theorem Subregular.Edge.takeAt_right {α : Type u_1} (k : ℕ) (xs : List α) : right.takeAt k xs = xs.rtake k

theorem Subregular.Edge.length_takeAt {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : (e.takeAt k xs).length = min k xs.length

An edge substring has length min k xs.length.

theorem Subregular.Edge.takeAt_of_length_le {α : Type u_1} (e : Edge) {k : ℕ} {xs : List α} (h : xs.length ≤ k) : e.takeAt k xs = xs

For a short string the edge substring is the whole string.

theorem Subregular.Edge.takeAt_left_append_of_le_length {α : Type u_1} {k : ℕ} (p rest : List α) (h : k ≤ p.length) : left.takeAt k (p ++ rest) = left.takeAt k p

The left-k-prefix of p ++ rest is that of p, when k ≤ p.length.

theorem Subregular.Edge.takeAt_right_append_of_le_length {α : Type u_1} {k : ℕ} (x rest : List α) (h : k ≤ rest.length) : right.takeAt k (x ++ rest) = right.takeAt k rest

The right-k-suffix of x ++ rest is that of rest, when k ≤ rest.length.

theorem Subregular.Edge.takeAt_idem {α : Type u_1} (e : Edge) (k : ℕ) (xs : List α) : e.takeAt k (e.takeAt k xs) = e.takeAt k xs

takeAt k is idempotent: its output already has length ≤ k.

Edge-bridge identities

A long word can be bridged to one sharing its right k-suffix and a prescribed left k'-prefix; these are the combinatorial core of 𝒩 = 𝒟 ∩ 𝒦.

The definite family

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

A language is k-definite (right-edge): membership factors through the length-k suffix.

Equations

• L.IsDefinite k = Function.FactorsThrough (fun (x : List α) => x ∈ L) (Subregular.Edge.right.takeAt k)

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

A language is reverse k-definite (left-edge): membership factors through the length-k prefix.

Equations

• L.IsReverseDefinite k = Function.FactorsThrough (fun (x : List α) => x ∈ L) (Subregular.Edge.left.takeAt k)

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

A language is generalized k-definite (Lambert's ℒℐ_k): membership factors through the joint length-k prefix and suffix [Lam26].

Equations

• L.IsGeneralizedDefinite k = Function.FactorsThrough (fun (x : List α) => x ∈ L) fun (w : List α) => (Subregular.Edge.left.takeAt k w, Subregular.Edge.right.takeAt k w)

theorem Language.isGeneralizedDefinite_iff_edges {α : Type u_1} {k : ℕ} {L : Language α} : L.IsGeneralizedDefinite k ↔ ∀ ⦃a b : List α⦄, Subregular.Edge.left.takeAt k a = Subregular.Edge.left.takeAt k b → Subregular.Edge.right.takeAt k a = Subregular.Edge.right.takeAt k b → (a ∈ L ↔ b ∈ L)

Generalized definiteness in two-hypothesis form: equal length-k prefix and suffix give L-equivalence (unpacking the joint-projection invariance).

theorem Language.isDefinite_iff_mem_takeAt {α : Type u_1} {k : ℕ} {L : Language α} : L.IsDefinite k ↔ ∀ (w : List α), w ∈ L ↔ Subregular.Edge.right.takeAt k w ∈ L

Definiteness in membership form: a word and its length-k suffix are L-equivalent (single-edge analogue of isGeneralizedDefinite_iff_edges).

def Language.IsFiniteOrCofinite {α : Type u_1} (L : Language α) : Prop

A language is finite-or-cofinite (Lambert's 𝒩): L or its complement is finite (equivalently L.Finite ∨ L ∈ Filter.cofinite).

Equations

• L.IsFiniteOrCofinite = (Set.Finite L ∨ Set.Finite Lᶜ)

theorem Language.isDefinite_setOf_right {α : Type u_1} (k : ℕ) (P : Set (List α)) : IsDefinite {w : List α | Subregular.Edge.right.takeAt k w ∈ P} k

Constructive view: a language carved out by a permitted length-k suffix set is k-definite (this is the e of Function.factorsThrough_iff).

theorem Language.isReverseDefinite_setOf_left {α : Type u_1} (k : ℕ) (P : Set (List α)) : IsReverseDefinite {w : List α | Subregular.Edge.left.takeAt k w ∈ P} k

Mirror for the left edge: a permitted length-k prefix set is reverse-definite.

Reverse duality

theorem Language.isReverseDefinite_iff_isDefinite_reverse {α : Type u_1} {k : ℕ} {L : Language α} : L.IsReverseDefinite k ↔ L.reverse.IsDefinite k

Reverse duality: reverse-k-definite is k-definite of the reversed language.

Inclusions into ℒℐ_k

theorem Language.IsDefinite.toIsGeneralizedDefinite {α : Type u_1} {k : ℕ} {L : Language α} (h : L.IsDefinite k) : L.IsGeneralizedDefinite k

D_k ⊆ ℒℐ_k: the suffix alone determines membership, so the joint prefix-and-suffix test does too.

theorem Language.IsReverseDefinite.toIsGeneralizedDefinite {α : Type u_1} {k : ℕ} {L : Language α} (h : L.IsReverseDefinite k) : L.IsGeneralizedDefinite k

RD_k ⊆ ℒℐ_k: symmetric, via the prefix.

𝒩 = 𝒟 ∩ 𝒦

theorem Language.isFiniteOrCofinite_of_eventually_constant {α : Type u_1} {L : Language α} {s : Set (List α)} (hs : s.Finite) (h : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, a ∈ L ↔ b ∈ L) : L.IsFiniteOrCofinite

A language whose membership is constant off a finite set s is finite-or-cofinite: either some word outside s lies in L (forcing Lᶜ ⊆ s) or none does (forcing L ⊆ s). The reusable engine behind the reverse direction of 𝒩 = 𝒟 ∩ 𝒦.

theorem Language.IsFiniteOrCofinite.exists_isDefinite_and_isReverseDefinite {α : Type u_1} {L : Language α} (h : L.IsFiniteOrCofinite) : (∃ (k : ℕ), L.IsDefinite k) ∧ ∃ (k' : ℕ), L.IsReverseDefinite k'

Forward direction of 𝒩 = 𝒟 ∩ 𝒦: a finite-or-cofinite language is both k-definite and reverse-k'-definite for some k, k'.

theorem Language.isFiniteOrCofinite_of_isDefinite_and_isReverseDefinite {α : Type u_1} [Finite α] {L : Language α} (h : (∃ (k : ℕ), L.IsDefinite k) ∧ ∃ (k' : ℕ), L.IsReverseDefinite k') : L.IsFiniteOrCofinite

Reverse direction of 𝒩 = 𝒟 ∩ 𝒦 (finite alphabet): if L is both k-definite and reverse-k'-definite, it is finite-or-cofinite. For words of length ≥ k + k' membership is constant (bridge argument), so either the long words are all in L (Lᶜ bounded) or none are (L bounded).

theorem Language.isFiniteOrCofinite_iff_exists_isDefinite_and_isReverseDefinite {α : Type u_1} [Finite α] {L : Language α} : L.IsFiniteOrCofinite ↔ (∃ (k : ℕ), L.IsDefinite k) ∧ ∃ (k' : ℕ), L.IsReverseDefinite k'

Pin's 𝒩 = 𝒟 ∩ 𝒦 (finite alphabet): a language over a finite alphabet is finite-or-cofinite iff it is k-definite for some k and reverse-k'-definite for some k'.