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.
A language is a set of strings over an alphabet.
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- language.inhabited = {default := 0}
@[protected, instance]
The sum of two languages is their union.
Equations
@[protected, instance]
The product of two languages l
and m
is the language made of the strings x ++ y
where
x ∈ l
and y ∈ m
.
Equations
theorem
language.mul_def
{α : Type u_1}
(l m : language α) :
l * m = set.image2 has_append.append l m
@[protected, instance]
The Kleene star of a language L
is the set of all strings which can be written by
concatenating strings from L
.
@[protected, instance]
Equations
- language.semiring = {add := has_add.add language.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul._default 0 has_add.add language.semiring._proof_4 language.semiring._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul language.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (n : ℕ), ite (n = 0) 0 1, nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow._default 1 has_mul.mul language.semiring._proof_18 language.semiring._proof_19, npow_zero' := _, npow_succ' := _}
@[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
@[simp]
theorem
language.map_kstar
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(l : language α) :
⇑(language.map f) (has_kstar.kstar l) = has_kstar.kstar (⇑(language.map f) l)
theorem
language.mul_self_kstar_comm
{α : Type u_1}
(l : language α) :
has_kstar.kstar l * l = l * has_kstar.kstar l
@[simp]
theorem
language.one_add_self_mul_kstar_eq_kstar
{α : Type u_1}
(l : language α) :
1 + l * has_kstar.kstar l = has_kstar.kstar l
@[simp]
theorem
language.one_add_kstar_mul_self_eq_kstar
{α : Type u_1}
(l : language α) :
1 + has_kstar.kstar l * l = has_kstar.kstar l
@[protected, instance]
Equations
- language.kleene_algebra = {add := semiring.add language.semiring, add_assoc := _, zero := semiring.zero language.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul language.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul language.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one language.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast language.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow language.semiring, npow_zero' := _, npow_succ' := _, sup := complete_boolean_algebra.sup set.complete_boolean_algebra, le := complete_boolean_algebra.le set.complete_boolean_algebra, lt := complete_boolean_algebra.lt set.complete_boolean_algebra, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := complete_boolean_algebra.bot set.complete_boolean_algebra, bot_le := _, kstar := has_kstar.kstar language.has_kstar, one_le_kstar := _, mul_kstar_le_kstar := _, kstar_mul_le_kstar := _, mul_kstar_le_self := _, kstar_mul_le_self := _}