Definite languages

This file defines the definite languages and their relatives. A language L is k-definite when membership of a word is decided by its last k letters: any two words with the same length-k suffix are both in L or both outside it. Perles, Rabin and Shamir develop the theory of these languages; reverse k-definite languages are the mirror image through the length-k prefix, and generalized k-definite languages are decided by the prefix and suffix together.

Main definitions

• Language.IsDefinite, Language.IsReverseDefinite, Language.IsGeneralizedDefinite: membership factors through the suffix, the prefix, and both.
• Language.IsFiniteOrCofinite: L or its complement is finite.

Main results

• Language.IsDefinite.toIsGeneralizedDefinite, Language.IsReverseDefinite.toIsGeneralizedDefinite: definite and reverse definite languages are generalized definite.
• Language.IsDefinite.isRegular, Language.IsReverseDefinite.isRegular, Language.IsGeneralizedDefinite.isRegular: over a finite alphabet all three are regular.
• Language.isFiniteOrCofinite_iff_exists_isDefinite_and_isReverseDefinite: over a finite alphabet, a language is finite or cofinite exactly when it is both definite and reverse definite.

References

• [PRS63]
• [Pin]

Edge-bridge identities

Two long words are bridged by a word sharing the length-k suffix of the first and the length-k' prefix of the second. This is the combinatorial step behind the characterization of the finite and cofinite languages.

The definite family

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

A language is k-definite when membership factors through the length-k suffix.

Equations

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

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

A language is reverse k-definite when membership factors through the length-k prefix.

Equations

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

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

A language is generalized k-definite when membership factors through the length-k prefix and suffix together.

Equations

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

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

A language is generalized k-definite exactly when words with equal length-k prefix and suffix are both in it or both outside it.

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

A language is k-definite exactly when every word is in it just when its length-k suffix is.

theorem Language.isReverseDefinite_iff_mem_takeAt {α : Type u_1} {k : ℕ} {L : Language α} : L.IsReverseDefinite k ↔ ∀ (w : List α), w ∈ L ↔ Edge.left.takeAt k w ∈ L

A language is reverse k-definite exactly when every word is in it just when its length-k prefix is.

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

A language is finite or cofinite when it or its complement is finite.

Equations

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

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

The words whose length-k suffix lies in a given set form a k-definite language.

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

The words whose length-k prefix lies in a given set form a reverse k-definite language.

Monotonicity in the window

theorem Language.IsDefinite.mono {α : Type u_1} {k k' : ℕ} {L : Language α} (h : L.IsDefinite k) (hk : k ≤ k') : L.IsDefinite k'

A k-definite language is k'-definite for every k' ≥ k.

theorem Language.IsReverseDefinite.mono {α : Type u_1} {k k' : ℕ} {L : Language α} (h : L.IsReverseDefinite k) (hk : k ≤ k') : L.IsReverseDefinite k'

A reverse k-definite language is reverse k'-definite for every k' ≥ k.

theorem Language.IsGeneralizedDefinite.mono {α : Type u_1} {k k' : ℕ} {L : Language α} (h : L.IsGeneralizedDefinite k) (hk : k ≤ k') : L.IsGeneralizedDefinite k'

A generalized k-definite language is generalized k'-definite for every k' ≥ k.

Affix languages

def Language.ofPrefix {α : Type u_1} (xs : List α) : Language α

The words beginning with xs.

Equations

• Language.ofPrefix xs = {w : List α | xs <+: w}

def Language.ofSuffix {α : Type u_1} (xs : List α) : Language α

The words ending in xs.

Equations

• Language.ofSuffix xs = {w : List α | xs <:+ w}

@[simp]

theorem Language.mem_ofPrefix {α : Type u_1} {xs w : List α} : w ∈ ofPrefix xs ↔ xs <+: w

@[simp]

theorem Language.mem_ofSuffix {α : Type u_1} {xs w : List α} : w ∈ ofSuffix xs ↔ xs <:+ w

theorem Language.isReverseDefinite_ofPrefix {α : Type u_1} (xs : List α) : (ofPrefix xs).IsReverseDefinite xs.length

The words beginning with xs form a reverse definite language with window xs.length.

theorem Language.isDefinite_ofSuffix {α : Type u_1} (xs : List α) : (ofSuffix xs).IsDefinite xs.length

The words ending in xs form a definite language with window xs.length.

Reverse duality

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

A language is reverse k-definite exactly when its reversal is k-definite.

Inclusions into the generalized definite languages

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

A k-definite language is generalized k-definite.

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

A reverse k-definite language is generalized k-definite.

Regularity

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

A definite language over a finite alphabet is regular.

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

A reverse definite language over a finite alphabet is regular.

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

A generalized definite language over a finite alphabet is regular.

Finite and cofinite languages

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, since either Lᶜ ⊆ s or L ⊆ s.

theorem Language.isDefinite_succ_of_forall_length_le {α : Type u_1} {L : Language α} {N : ℕ} (h : ∀ w ∈ L, w.length ≤ N) : L.IsDefinite (N + 1)

A language whose words have length at most N is (N + 1)-definite.

theorem Language.isReverseDefinite_succ_of_forall_length_le {α : Type u_1} {L : Language α} {N : ℕ} (h : ∀ w ∈ L, w.length ≤ N) : L.IsReverseDefinite (N + 1)

A language whose words have length at most N is reverse (N + 1)-definite.

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

A finite or cofinite language is definite and reverse definite.

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

Over a finite alphabet, a language that is both definite and reverse definite is finite or cofinite, since membership is constant on words of length at least k + k'.

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

Over a finite alphabet, a language is finite or cofinite exactly when it is definite and reverse definite.