Languages #
This file contains the definition and operations on formal languages over an alphabet. Note strings are implemented as lists over the alphabet. The operations in this file define a Kleene algebra over the languages.
Zero language has no elements.
The sum of two languages is their union.
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.mul_def
{α : Type u_1}
(l : Language α)
(m : Language α)
:
l * m = Set.image2 (fun x x_1 => x ++ x_1) l m
The Kleene star of a language L
is the set of all strings which can be written by
concatenating strings from L
.
@[simp]
theorem
Language.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(g : β → γ)
(f : α → β)
(l : Language α)
:
↑(Language.map g) (↑(Language.map f) l) = ↑(Language.map (g ∘ f)) 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 α)
:
↑(Language.map f) (KStar.kstar l) = KStar.kstar (↑(Language.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