# mathlibdocumentation

computability.language

# 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.

def language (α : Type u_1) :
Type u_1

A language is a set of strings over an alphabet.

Equations
Instances for language
@[protected, instance]
def language.complete_boolean_algebra (α : Type u_1) :
@[protected, instance]
def language.has_insert (α : Type u_1) :
@[protected, instance]
def language.has_singleton (α : Type u_1) :
(language α)
@[protected, instance]
def language.has_mem (α : Type u_1) :
@[protected, instance]
def language.has_zero {α : Type u_1} :

Zero language has no elements.

Equations
@[protected, instance]
def language.has_one {α : Type u_1} :

1 : language α contains only one element [].

Equations
@[protected, instance]
def language.inhabited {α : Type u_1} :
Equations
@[protected, instance]
def language.has_add {α : Type u_1} :

The sum of two languages is their union.

Equations
@[protected, instance]
def language.has_mul {α : Type u_1} :

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.zero_def {α : Type u_1} :
0 =
theorem language.one_def {α : Type u_1} :
theorem language.add_def {α : Type u_1} (l m : language α) :
l + m = l m
theorem language.mul_def {α : Type u_1} (l m : language α) :
l * m =
def language.star {α : Type u_1} (l : language α) :

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

Equations
theorem language.star_def {α : Type u_1} (l : language α) :
l.star = {x : list α | ∃ (S : list (list α)), x = S.join ∀ (y : list α), y Sy l}
@[simp]
theorem language.not_mem_zero {α : Type u_1} (x : list α) :
x 0
@[simp]
theorem language.mem_one {α : Type u_1} (x : list α) :
x 1
theorem language.nil_mem_one {α : Type u_1} :
@[simp]
theorem language.mem_add {α : 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 b : list α), a l b m a ++ b = x
theorem language.append_mem_mul {α : Type u_1} {l m : language α} {a b : list α} :
a lb ma ++ b l * m
theorem language.mem_star {α : Type u_1} {l : language α} {x : list α} :
x l.star ∃ (S : list (list α)), x = S.join ∀ (y : list α), y Sy l
theorem language.join_mem_star {α : Type u_1} {l : language α} {S : list (list α)} (h : ∀ (y : list α), y Sy l) :
theorem language.nil_mem_star {α : Type u_1} (l : language α) :
@[protected, instance]
def language.semiring {α : Type u_1} :
Equations
@[simp]
theorem language.add_self {α : Type u_1} (l : language α) :
l + l = l
def language.map {α : Type u_1} {β : Type u_2} (f : α → β) :

Maps the alphabet of a language.

Equations
@[simp]
theorem language.map_id {α : Type u_1} (l : language α) :
l = l
@[simp]
theorem language.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (l : language α) :
theorem language.star_def_nonempty {α : Type u_1} (l : language α) :
l.star = {x : list α | ∃ (S : list (list α)), x = S.join ∀ (y : list α), y Sy l
theorem language.le_iff {α : Type u_1} (l m : language α) :
l m l + m = m
theorem language.le_mul_congr {α : Type u_1} {l₁ l₂ m₁ m₂ : language α} :
l₁ m₁l₂ m₂l₁ * l₂ m₁ * m₂
theorem language.le_add_congr {α : Type u_1} {l₁ l₂ m₁ m₂ : language α} :
l₁ m₁l₂ m₂l₁ + l₂ m₁ + m₂
theorem language.mem_supr {α : Type u_1} {ι : Sort v} {l : ι → } {x : list α} :
(x ⨆ (i : ι), l i) ∃ (i : ι), x l i
theorem language.supr_mul {α : Type u_1} {ι : Sort v} (l : ι → ) (m : language α) :
(⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m
theorem language.mul_supr {α : Type u_1} {ι : Sort v} (l : ι → ) (m : language α) :
(m * ⨆ (i : ι), l i) = ⨆ (i : ι), m * l i
theorem language.supr_add {α : Type u_1} {ι : Sort v} [nonempty ι] (l : ι → ) (m : language α) :
(⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m
theorem language.add_supr {α : Type u_1} {ι : Sort v} [nonempty ι] (l : ι → ) (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.join S.length = n ∀ (y : list α), y Sy l
theorem language.star_eq_supr_pow {α : Type u_1} (l : language α) :
l.star = ⨆ (i : ), l ^ i
@[simp]
theorem language.map_star {α : Type u_1} {β : Type u_2} (f : α → β) (l : language α) :
theorem language.mul_self_star_comm {α : Type u_1} (l : language α) :
l.star * l = l * l.star
@[simp]
theorem language.one_add_self_mul_star_eq_star {α : Type u_1} (l : language α) :
1 + l * l.star = l.star
@[simp]
theorem language.one_add_star_mul_self_eq_star {α : Type u_1} (l : language α) :
1 + l.star * l = l.star
theorem language.star_mul_le_right_of_mul_le_right {α : Type u_1} (l m : language α) :
l * m ml.star * m m
theorem language.star_mul_le_left_of_mul_le_left {α : Type u_1} (l m : language α) :
m * l mm * l.star m