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.

source
def language (α : Type u_1) :
Type u_1

A language is a set of strings over an alphabet.

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

Zero language has no elements.

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

1 : language α contains only one element [].

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

The sum of two languages is their union.

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

The product of two languages l and m is the language made of the strings x ++ y where x ∈ l and y ∈ m.

Equations
source
theorem language.zero_def {α : Type u_1} :
0 = ∅
source
theorem language.one_def {α : Type u_1} :
1 = {list.nil}
source
theorem language.add_def {α : Type u_1} (l m : language α) :
l + m = l ∪ m
source
theorem language.mul_def {α : Type u_1} (l m : language α) :
l * m = set.image2 has_append.append l m
source
def language.star {α : Type u_1} (l : language α) :
language α

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

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

Maps the alphabet of a language.

Equations
source
@[simp]
theorem language.map_id {α : Type u_1} (l : language α) :
⇑(language.map id) l = l
source
@[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
source
theorem language.star_def_nonempty {α : Type u_1} (l : language α) :
l.star = {x : list α | ∃ (S : list (list α)), x = S.join ∧ ∀ (y : list α), y ∈ S → y ∈ l ∧ y ≠ list.nil}
source
theorem language.le_iff {α : Type u_1} (l m : language α) :
l ≤ m ↔ l + m = m
source
theorem language.le_mul_congr {α : Type u_1} {l₁ l₂ m₁ m₂ : language α} :
l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂
source
theorem language.le_add_congr {α : Type u_1} {l₁ l₂ m₁ m₂ : language α} :
l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂
source
theorem language.mem_supr {α : Type u_1} {ι : Sort v} {l : ι → language α} {x : list α} :
(x ∈ ⨆ (i : ι), l i) ↔ ∃ (i : ι), x ∈ l i
source
theorem language.supr_mul {α : Type u_1} {ι : Sort v} (l : ι → language α) (m : language α) :
(⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m
source
theorem language.mul_supr {α : Type u_1} {ι : Sort v} (l : ι → language α) (m : language α) :
(m * ⨆ (i : ι), l i) = ⨆ (i : ι), m * l i
source
theorem language.supr_add {α : Type u_1} {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
(⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m
source
theorem language.add_supr {α : Type u_1} {ι : Sort v} [nonempty ι] (l : ι → language α) (m : language α) :
(m + ⨆ (i : ι), l i) = ⨆ (i : ι), m + l i
source
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
source
theorem language.star_eq_supr_pow {α : Type u_1} (l : language α) :
l.star = ⨆ (i : ℕ), l ^ i
source
@[simp]
theorem language.map_star {α : Type u_1} {β : Type u_2} (f : α → β) (l : language α) :
⇑(language.map f) l.star = (⇑(language.map f) l).star
source
theorem language.mul_self_star_comm {α : Type u_1} (l : language α) :
l.star * l = l * l.star
source
@[simp]
theorem language.one_add_self_mul_star_eq_star {α : Type u_1} (l : language α) :
1 + l * l.star = l.star
source
@[simp]
theorem language.one_add_star_mul_self_eq_star {α : Type u_1} (l : language α) :
1 + l.star * l = l.star
source
theorem language.star_mul_le_right_of_mul_le_right {α : Type u_1} (l m : language α) :
l * m ≤ m → l.star * m ≤ m
source
theorem language.star_mul_le_left_of_mul_le_left {α : Type u_1} (l m : language α) :
m * l ≤ m → m * l.star ≤ m