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.

def language (α : Type u_1) :
Type u_1

A language is a set of strings over an alphabet.

Equations
@[instance]
def language.has_insert (α : Type u_1) :
@[instance]
def language.has_singleton (α : Type u_1) :
@[instance]
def language.has_mem (α : Type u_1) :
@[instance]
def language.has_zero {α : Type u} :

Zero language has no elements.

Equations
@[instance]
def language.has_one {α : Type u} :

1 : language α contains only one element [].

Equations
@[instance]
def language.inhabited {α : Type u} :
Equations
@[instance]
def language.has_add {α : Type u} :

The sum of two languages is the union of

Equations
@[instance]
def language.has_mul {α : Type u} :
Equations
theorem language.zero_def {α : Type u} :
0 =
theorem language.one_def {α : Type u} :
theorem language.add_def {α : Type u} (l m : language α) :
l + m = l m
theorem language.mul_def {α : Type u} (l m : language α) :
def language.star {α : Type u} (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} (l : language α) :
l.star = {x : list α | ∃ (S : list (list α)), x = S.join ∀ (y : list α), y Sy l}
@[simp]
theorem language.mem_one {α : Type u} (x : list α) :
@[simp]
theorem language.mem_add {α : Type u} (l m : language α) (x : list α) :
x l + m x l x m
theorem language.mem_mul {α : Type u} (l m : language α) (x : list α) :
x l * m ∃ (a b : list α), a l b m a ++ b = x
theorem language.mem_star {α : Type u} (l : language α) (x : list α) :
x l.star ∃ (S : list (list α)), x = S.join ∀ (y : list α), y Sy l
@[instance]
def language.semiring {α : Type u} :
Equations
@[simp]
theorem language.add_self {α : Type u} (l : language α) :
l + l = l
theorem language.star_def_nonempty {α : Type u} (l : language α) :
l.star = {x : list α | ∃ (S : list (list α)), x = S.join ∀ (y : list α), y Sy l y list.nil}
theorem language.le_iff {α : Type u} (l m : language α) :
l m l + m = m
theorem language.le_mul_congr {α : Type u} {l₁ l₂ m₁ m₂ : language α} :
l₁ m₁l₂ m₂l₁ * l₂ m₁ * m₂
theorem language.le_add_congr {α : Type u} {l₁ l₂ m₁ m₂ : language α} :
l₁ m₁l₂ m₂l₁ + l₂ m₁ + m₂
theorem language.mem_supr {α : Type u} {ι : Sort v} {l : ι → language α} {x : list α} :
(x ⨆ (i : ι), l i) ∃ (i : ι), x l i
theorem language.supr_mul {α : Type u} {ι : Sort v} (l : ι → language α) (m : language α) :
(⨆ (i : ι), l i) * m = ⨆ (i : ι), (l i) * m
theorem language.mul_supr {α : Type u} {ι : Sort v} (l : ι → language α) (m : language α) :
(m * ⨆ (i : ι), l i) = ⨆ (i : ι), m * l i
theorem language.supr_add {α : Type u} {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
(⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m
theorem language.add_supr {α : Type u} {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
(m + ⨆ (i : ι), l i) = ⨆ (i : ι), m + l i
theorem language.mem_pow {α : Type u} {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} (l : language α) :
l.star = ⨆ (i : ), l ^ i
theorem language.mul_self_star_comm {α : Type u} (l : language α) :
(l.star) * l = l * l.star
@[simp]
theorem language.one_add_self_mul_star_eq_star {α : Type u} (l : language α) :
1 + l * l.star = l.star
@[simp]
theorem language.one_add_star_mul_self_eq_star {α : Type u} (l : language α) :
1 + (l.star) * l = l.star
theorem language.star_mul_le_right_of_mul_le_right {α : Type u} (l m : language α) :
l * m m(l.star) * m m
theorem language.star_mul_le_left_of_mul_le_left {α : Type u} (l m : language α) :
m * l mm * l.star m