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.

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

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

Equations
source
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}
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
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_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
source
theorem language.join_mem_kstar {α : Type u_1} {l : language α} {L : list (list α)} (h : ∀ (y : list α), y ∈ L → y ∈ l) :
L.join ∈ has_kstar.kstar l
source
theorem language.nil_mem_kstar {α : Type u_1} (l : language α) :
list.nil ∈ has_kstar.kstar l
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.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}
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.kstar_eq_supr_pow {α : Type u_1} (l : language α) :
has_kstar.kstar l = ⨆ (i : ℕ), l ^ i
source
@[simp]
theorem language.map_kstar {α : Type u_1} {β : Type u_2} (f : α → β) (l : language α) :
⇑(language.map f) (has_kstar.kstar l) = has_kstar.kstar (⇑(language.map f) l)
source
theorem language.mul_self_kstar_comm {α : Type u_1} (l : language α) :
has_kstar.kstar l * l = l * has_kstar.kstar l
source
@[simp]
theorem language.one_add_self_mul_kstar_eq_kstar {α : Type u_1} (l : language α) :
1 + l * has_kstar.kstar l = has_kstar.kstar l
source
@[simp]
theorem language.one_add_kstar_mul_self_eq_kstar {α : Type u_1} (l : language α) :
1 + has_kstar.kstar l * l = has_kstar.kstar l
source
@[protected, instance]
def language.kleene_algebra {α : Type u_1} :
kleene_algebra (language α)
Equations