Languages

This file contains the definition and operations on formal languages over an alphabet. Note that "strings" are implemented as lists over the alphabet.

Union and concatenation define a Kleene algebra over the languages.

In addition to that, we define a reversal of a language and prove that it behaves well with respect to other language operations.

Notation

• l + m: union of languages l and m
• l - m: difference of languages l and m
• l * m: language of strings x ++ y such that x ∈ l and y ∈ m
• l ^ n: language of strings consisting of n members of l concatenated together
• 1: language consisting of only the empty string. This is because it is the unit of the * operator.
• l∗: Kleene star – language of strings consisting of arbitrarily many members of l concatenated together. Note that this notation uses the Unicode asterisk operator ∗, as opposed to the more common ASCII asterisk *.
• lᶜ: complement, language of strings x such that x ∉ l
• l ⊓ m: intersection of languages l and m

Main definitions

• Language α: a set of strings over the alphabet α
• l.map f: transform a language l over α into a language over β by translating through f : α → β

Main theorems

• Language.self_eq_mul_add_iff: Arden's lemma – if a language l satisfies the equation l = m * l + n, and m doesn't contain the empty string, then l is the language m∗ * n

def Language (α : Type u_4) : Type u_4

A language is a set of strings over an alphabet.

instance Language.instMembershipList {α : Type u_1} : Membership (List α) (Language α)

instance Language.instSingletonList {α : Type u_1} : Singleton (List α) (Language α)

instance Language.instInsertList {α : Type u_1} : Insert (List α) (Language α)

instance Language.instCompleteAtomicBooleanAlgebra {α : Type u_1} : CompleteAtomicBooleanAlgebra (Language α)

instance Language.instZero {α : Type u_1} : Zero (Language α)

Zero language has no elements.

instance Language.instOne {α : Type u_1} : One (Language α)

1 : Language α contains only one element [].

instance Language.instInhabited {α : Type u_1} : Inhabited (Language α)

instance Language.instAdd {α : Type u_1} : Add (Language α)

The sum of two languages is their union.

instance Language.instSub {α : Type u_1} : Sub (Language α)

The subtraction of two languages is their difference.

instance Language.instMul {α : Type u_1} : Mul (Language α)

The product of two languages l and m is the language made of the strings x ++ y where x ∈ l and y ∈ m.

theorem Language.zero_def {α : Type u_1} : 0 = ∅

theorem Language.one_def {α : Type u_1} : 1 = {[]}

theorem Language.add_def {α : Type u_1} (l m : Language α) : l + m = l ∪ m

theorem Language.sub_def {α : Type u_1} (l m : Language α) : l - m = l \ m

theorem Language.mul_def {α : Type u_1} (l m : Language α) : l * m = Set.image2 (fun (x1 x2 : List α) => x1 ++ x2) l m

instance Language.instKStar {α : Type u_1} : KStar (Language α)

The Kleene star of a language L is the set of all strings which can be written by concatenating strings from L.

theorem Language.kstar_def {α : Type u_1} (l : Language α) : KStar.kstar l = {x : List α | ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l}

theorem Language.ext {α : Type u_1} {l m : Language α} (h : ∀ (x : List α), x ∈ l ↔ x ∈ m) : l = m

theorem Language.ext_iff {α : Type u_1} {l m : Language α} : l = m ↔ ∀ (x : List α), x ∈ l ↔ x ∈ m

@[simp]

theorem Language.notMem_zero {α : Type u_1} (x : List α) : x ∉ 0

@[simp]

theorem Language.mem_one {α : Type u_1} (x : List α) : x ∈ 1 ↔ x = []

theorem Language.nil_mem_one {α : Type u_1} : [] ∈ 1

theorem Language.mem_add {α : Type u_1} (l m : Language α) (x : List α) : x ∈ l + m ↔ x ∈ l ∨ x ∈ m

theorem Language.mem_sub {α : Type u_1} (l m : Language α) (x : List α) : x ∈ l - m ↔ x ∈ l ∧ x ∉ m

theorem Language.mem_mul {α : Type u_1} {l m : Language α} {x : List α} : x ∈ l * m ↔ ∃ a ∈ l, ∃ b ∈ m, a ++ b = x

theorem Language.append_mem_mul {α : Type u_1} {l m : Language α} {a b : List α} : a ∈ l → b ∈ m → a ++ b ∈ l * m

theorem Language.mem_kstar {α : Type u_1} {l : Language α} {x : List α} : x ∈ KStar.kstar l ↔ ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l

theorem Language.join_mem_kstar {α : Type u_1} {l : Language α} {L : List (List α)} (h : ∀ y ∈ L, y ∈ l) : L.flatten ∈ KStar.kstar l

theorem Language.nil_mem_kstar {α : Type u_1} (l : Language α) : [] ∈ KStar.kstar l

instance Language.instOrderedSub {α : Type u_1} : OrderedSub (Language α)

instance Language.instSemiring {α : Type u_1} : Semiring (Language α)

@[simp]

theorem Language.add_self {α : Type u_1} (l : Language α) : l + l = l

def Language.map {α : Type u_1} {β : Type u_2} (f : α → β) : Language α →+* Language β

Maps the alphabet of a language.

@[simp]

theorem Language.map_id {α : Type u_1} (l : Language α) : (map id) l = l

@[simp]

theorem Language.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (l : Language α) : (map g) ((map f) l) = (map (g ∘ f)) l

theorem Language.mem_kstar_iff_exists_nonempty {α : Type u_1} {l : Language α} {x : List α} : x ∈ KStar.kstar l ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

theorem Language.kstar_def_nonempty {α : Type u_1} (l : Language α) : KStar.kstar l = {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

theorem Language.le_iff {α : Type u_1} (l m : Language α) : l ≤ m ↔ l + m = m

instance Language.instMulLeftMono {α : Type u_1} : MulLeftMono (Language α)

instance Language.instMulRightMono {α : Type u_1} : MulRightMono (Language α)

@[deprecated mul_le_mul' (since := "2025-10-26")]

theorem Language.le_mul_congr {α : Type u_1} {l₁ l₂ m₁ m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂

theorem Language.mem_iSup {α : Type u_1} {ι : Sort v} {l : ι → Language α} {x : List α} : x ∈ ⨆ (i : ι), l i ↔ ∃ (i : ι), x ∈ l i

theorem Language.iSup_mul {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m

theorem Language.mul_iSup {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : m * ⨆ (i : ι), l i = ⨆ (i : ι), m * l i

theorem Language.iSup_add {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m

theorem Language.add_iSup {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : m + ⨆ (i : ι), l i = ⨆ (i : ι), m + l i

theorem Language.iSup_sub {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) - m = ⨆ (i : ι), l i - m

theorem Language.sub_iSup {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : m - ⨆ (i : ι), l i = ⨅ (i : ι), m - l i

theorem Language.mem_pow {α : Type u_1} {l : Language α} {x : List α} {n : ℕ} : x ∈ l ^ n ↔ ∃ (S : List (List α)), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l

theorem Language.kstar_eq_iSup_pow {α : Type u_1} (l : Language α) : KStar.kstar l = ⨆ (i : ℕ), l ^ i

@[simp]

theorem Language.map_kstar {α : Type u_1} {β : Type u_2} (f : α → β) (l : Language α) : (map f) (KStar.kstar l) = KStar.kstar ((map f) l)

theorem Language.mul_self_kstar_comm {α : Type u_1} (l : Language α) : KStar.kstar l * l = l * KStar.kstar l

@[simp]

theorem Language.one_add_self_mul_kstar_eq_kstar {α : Type u_1} (l : Language α) : 1 + l * KStar.kstar l = KStar.kstar l

@[simp]

theorem Language.one_add_kstar_mul_self_eq_kstar {α : Type u_1} (l : Language α) : 1 + KStar.kstar l * l = KStar.kstar l

instance Language.instKleeneAlgebra {α : Type u_1} : KleeneAlgebra (Language α)

@[deprecated add_le_add (since := "2025-10-26")]

theorem Language.le_add_congr {α : Type u_1} {l₁ l₂ m₁ m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂

theorem Language.self_eq_mul_add_iff {α : Type u_1} {l m n : Language α} (hm : [] ∉ m) : l = m * l + n ↔ l = KStar.kstar m * n

Arden's lemma

def Language.reverse {α : Type u_1} (l : Language α) : Language α

Language l.reverse is defined as the set of words from l backwards.

@[simp]

theorem Language.mem_reverse {α : Type u_1} {l : Language α} {a : List α} : a ∈ l.reverse ↔ a.reverse ∈ l

theorem Language.reverse_mem_reverse {α : Type u_1} {l : Language α} {a : List α} : a.reverse ∈ l.reverse ↔ a ∈ l

theorem Language.reverse_eq_image {α : Type u_1} (l : Language α) : l.reverse = List.reverse '' l

@[simp]

theorem Language.reverse_zero {α : Type u_1} : reverse 0 = 0

@[simp]

theorem Language.reverse_one {α : Type u_1} : reverse 1 = 1

theorem Language.reverse_involutive {α : Type u_1} : Function.Involutive reverse

theorem Language.reverse_bijective {α : Type u_1} : Function.Bijective reverse

theorem Language.reverse_injective {α : Type u_1} : Function.Injective reverse

theorem Language.reverse_surjective {α : Type u_1} : Function.Surjective reverse

@[simp]

theorem Language.reverse_reverse {α : Type u_1} (l : Language α) : l.reverse.reverse = l

@[simp]

theorem Language.reverse_add {α : Type u_1} (l m : Language α) : (l + m).reverse = l.reverse + m.reverse

@[simp]

theorem Language.reverse_mul {α : Type u_1} (l m : Language α) : (l * m).reverse = m.reverse * l.reverse

@[simp]

theorem Language.reverse_iSup {α : Type u_1} {ι : Sort u_4} (l : ι → Language α) : (⨆ (i : ι), l i).reverse = ⨆ (i : ι), (l i).reverse

@[simp]

theorem Language.reverse_iInf {α : Type u_1} {ι : Sort u_4} (l : ι → Language α) : (⨅ (i : ι), l i).reverse = ⨅ (i : ι), (l i).reverse

def Language.reverseIso (α : Type u_1) : Language α ≃+* (Language α)ᵐᵒᵖ

Language.reverse as a ring isomorphism to the opposite ring.

@[simp]

theorem Language.reverseIso_apply (α : Type u_1) (l : Language α) : (reverseIso α) l = MulOpposite.op l.reverse

@[simp]

theorem Language.reverseIso_symm_apply (α : Type u_1) (l' : (Language α)ᵐᵒᵖ) : (reverseIso α).symm l' = (MulOpposite.unop l').reverse

@[simp]

theorem Language.reverse_pow {α : Type u_1} (l : Language α) (n : ℕ) : (l ^ n).reverse = l.reverse ^ n

@[simp]

theorem Language.reverse_kstar {α : Type u_1} (l : Language α) : (KStar.kstar l).reverse = KStar.kstar l.reverse

@[simp]

theorem Language.mem_inf {α : Type u_1} {x : List α} {l m : Language α} : x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m

theorem Language.compl_compl {α : Type u_1} (l : Language α) : lᶜᶜ = l

inductive Symbol (T : Type u_4) (N : Type u_5) : Type (max u_4 u_5)

Symbols for use by all kinds of grammars.

• terminal {T : Type u_4} {N : Type u_5} (t : T) : Symbol T N

  Terminal symbols (of the same type as the language)

• nonterminal {T : Type u_4} {N : Type u_5} (n : N) : Symbol T N

  Nonterminal symbols (must not be present when the word being generated is finalized)

instance instDecidableEqSymbol {T✝ : Type u_4} {N✝ : Type u_5} [DecidableEq T✝] [DecidableEq N✝] : DecidableEq (Symbol T✝ N✝)

def instDecidableEqSymbol.decEq {T✝ : Type u_4} {N✝ : Type u_5} [DecidableEq T✝] [DecidableEq N✝] (x✝ x✝¹ : Symbol T✝ N✝) : Decidable (x✝ = x✝¹)

def instReprSymbol.repr {T✝ : Type u_4} {N✝ : Type u_5} [Repr T✝] [Repr N✝] : Symbol T✝ N✝ → ℕ → Std.Format

instance instReprSymbol {T✝ : Type u_4} {N✝ : Type u_5} [Repr T✝] [Repr N✝] : Repr (Symbol T✝ N✝)

instance instFintypeSymbol {T✝ : Type u_4} {N✝ : Type u_5} [Fintype T✝] [Fintype N✝] : Fintype (Symbol T✝ N✝)