mathlib documentation

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.

@[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 α) :