mathlib3 documentation

computability.language

Languages #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected, instance]
@[protected, instance]
def language.has_insert (α : Type u_1) :
@[protected, instance]
def language.has_singleton (α : Type u_1) :
@[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 α) :
@[protected, instance]
def language.has_kstar {α : Type u_1} :

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

Equations
theorem language.kstar_def {α : Type u_1} (l : language α) :
has_kstar.kstar l = {x : list α | (L : list (list α)), x = L.join (y : list α), y L y l}
@[simp]
theorem language.not_mem_zero {α : Type u_1} (x : list α) :
x 0
@[simp]
theorem language.mem_one {α : Type u_1} (x : list α) :
theorem language.nil_mem_one {α : Type u_1} :
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 l b m a ++ b l * m
theorem language.mem_kstar {α : Type u_1} {l : language α} {x : list α} :
x has_kstar.kstar l (L : list (list α)), x = L.join (y : list α), y L y l
theorem language.join_mem_kstar {α : Type u_1} {l : language α} {L : list (list α)} (h : (y : list α), y L y l) :
@[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 α) :
@[simp]
theorem language.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : α β) (l : language α) :
theorem language.kstar_def_nonempty {α : Type u_1} (l : language α) :
has_kstar.kstar l = {x : list α | (S : list (list α)), x = S.join (y : list α), y S y l y list.nil}
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 : ι language α} {x : list α} :
(x (i : ι), l i) (i : ι), x l i
theorem language.supr_mul {α : Type u_1} {ι : Sort v} (l : ι language α) (m : language α) :
( (i : ι), l i) * m = (i : ι), l i * m
theorem language.mul_supr {α : Type u_1} {ι : Sort v} (l : ι language α) (m : language α) :
(m * (i : ι), l i) = (i : ι), m * l i
theorem language.supr_add {α : Type u_1} {ι : Sort v} [nonempty ι] (l : ι language α) (m : language α) :
( (i : ι), l i) + m = (i : ι), l i + m
theorem language.add_supr {α : 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.join S.length = n (y : list α), y S y l
theorem language.kstar_eq_supr_pow {α : Type u_1} (l : language α) :
has_kstar.kstar l = (i : ), l ^ i
@[simp]
theorem language.map_kstar {α : Type u_1} {β : Type u_2} (f : α β) (l : language α) :