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
source
@[instance]
def language.complete_boolean_algebra (α : Type u_1) :
complete_boolean_algebra (language α)
source
@[instance]
def language.has_insert (α : Type u_1) :
has_insert (list α) (language α)
source
@[instance]
def language.has_singleton (α : Type u_1) :
has_singleton (list α) (language α)
source
@[instance]
def language.has_mem (α : Type u_1) :
has_mem (list α) (language α)
source
@[instance]
def language.has_zero {α : Type u} :
has_zero (language α)

Zero language has no elements.

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

1 : language α contains only one element [].

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

The sum of two languages is the union of

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