Documentation

Mathlib.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_4) :
Type u_4

A language is a set of strings over an alphabet.

Instances For
    instance instInsertListLanguage {α : Type u_1} :
    Insert (List α) (Language α)
    instance Language.instZeroLanguage {α : Type u_1} :

    Zero language has no elements.

    instance Language.instOneLanguage {α : Type u_1} :

    1 : Language α contains only one element [].

    instance Language.instAddLanguage {α : Type u_1} :

    The sum of two languages is their union.

    instance Language.instMulLanguage {α : 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.

    theorem Language.zero_def {α : Type u_1} :
    0 =
    theorem Language.one_def {α : Type u_1} :
    1 = {[]}
    theorem Language.add_def {α : Type u_1} (l : Language α) (m : Language α) :
    l + m = l m
    theorem Language.mul_def {α : Type u_1} (l : Language α) (m : Language α) :
    l * m = Set.image2 (fun x x_1 => x ++ x_1) l m
    instance Language.instKStarLanguage {α : 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.

    theorem Language.kstar_def {α : Type u_1} (l : Language α) :
    KStar.kstar l = {x | L, x = List.join L ∀ (y : List α), y Ly l}
    theorem Language.ext {α : Type u_1} {l : Language α} {m : Language α} (h : ∀ (x : List α), x l x m) :
    l = m
    @[simp]
    theorem Language.not_mem_zero {α : Type u_1} (x : List α) :
    ¬x 0
    @[simp]
    theorem Language.mem_one {α : Type u_1} (x : List α) :
    x 1 x = []
    theorem Language.nil_mem_one {α : Type u_1} :
    [] 1
    theorem Language.mem_add {α : Type u_1} (l : Language α) (m : Language α) (x : List α) :
    x l + m x l x m
    theorem Language.mem_mul {α : Type u_1} {l : Language α} {m : Language α} {x : List α} :
    x l * m a b, a l b m a ++ b = x
    theorem Language.append_mem_mul {α : Type u_1} {l : Language α} {m : Language α} {a : List α} {b : List α} :
    a lb ma ++ b l * m
    theorem Language.mem_kstar {α : Type u_1} {l : Language α} {x : List α} :
    x KStar.kstar l L, x = List.join L ∀ (y : List α), y Ly l
    theorem Language.join_mem_kstar {α : Type u_1} {l : Language α} {L : List (List α)} (h : ∀ (y : List α), y Ly l) :
    theorem Language.nil_mem_kstar {α : Type u_1} (l : Language α) :
    @[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.

    Instances For
      @[simp]
      theorem Language.map_id {α : Type u_1} (l : Language α) :
      ↑(Language.map id) l = l
      @[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
      theorem Language.kstar_def_nonempty {α : Type u_1} (l : Language α) :
      KStar.kstar l = {x | S, x = List.join S ∀ (y : List α), y Sy l y []}
      theorem Language.le_iff {α : Type u_1} (l : Language α) (m : Language α) :
      l m l + m = m
      theorem Language.le_mul_congr {α : Type u_1} {l₁ : Language α} {l₂ : Language α} {m₁ : Language α} {m₂ : Language α} :
      l₁ m₁l₂ m₂l₁ * l₂ m₁ * m₂
      theorem Language.le_add_congr {α : Type u_1} {l₁ : Language α} {l₂ : Language α} {m₁ : Language α} {m₂ : Language α} :
      l₁ m₁l₂ m₂l₁ + l₂ m₁ + m₂
      theorem Language.mem_iSup {α : Type u_1} {ι : Sort v} {l : ιLanguage α} {x : List α} :
      x ⨆ (i : ι), l i i, x l i
      theorem Language.iSup_mul {α : Type u_1} {ι : Sort v} (l : ιLanguage α) (m : Language α) :
      (⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m
      theorem Language.mul_iSup {α : Type u_1} {ι : Sort v} (l : ιLanguage α) (m : Language α) :
      m * ⨆ (i : ι), l i = ⨆ (i : ι), m * l i
      theorem Language.iSup_add {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ιLanguage α) (m : Language α) :
      (⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m
      theorem Language.add_iSup {α : 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, x = List.join S List.length S = n ∀ (y : List α), y Sy l
      theorem Language.kstar_eq_iSup_pow {α : Type u_1} (l : Language α) :
      KStar.kstar l = ⨆ (i : ), l ^ i
      @[simp]
      theorem Language.map_kstar {α : Type u_1} {β : Type u_2} (f : αβ) (l : Language α) :