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]
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_star
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(l : language α) :
⇑(language.map f) l.star = (⇑(language.map f) l).star