Languages #

This file contains the definition and operations on formal languages over an alphabet. Note that "strings" are implemented as lists over the alphabet.

Union and concatenation define a Kleene algebra over the languages.

In addition to that, we define a reversal of a language and prove that it behaves well with respect to other language operations.

Notation #

l + m: union of languages l and m
l * m: language of strings x ++ y such that x ∈ l and y ∈ m
l ^ n: language of strings consisting of n members of l concatenated together
1: language consisting of only the empty string. This is because it is the unit of the * operator.
l∗: Kleene's star – language of strings consisting of arbitrarily many members of l concatenated together (Note that this is the Unicode asterisk ∗, and not the more common star *)

Main definitions #

Language α: a set of strings over the alphabet α
l.map f: transform a language l over α into a language over β by translating through f : α → β

Main theorems #

Language.self_eq_mul_add_iff: Arden's lemma – if a language l satisfies the equation l = m * l + n, and m doesn't contain the empty string, then l is the language m∗ * n

source

def Language (α : Type u_4) :

Type u_4

A language is a set of strings over an alphabet.

Equations

Language α = Set (List α)

Instances For

source

instance Language.instMembershipList {α : Type u_1} :

Membership (List α) (Language α)

Equations

Language.instMembershipList = { mem := Set.Mem }

source

instance Language.instSingletonList {α : Type u_1} :

Singleton (List α) (Language α)

Equations

Language.instSingletonList = { singleton := Set.singleton }

source

instance Language.instInsertList {α : Type u_1} :

Insert (List α) (Language α)

Equations

Language.instInsertList = { insert := Set.insert }

source

instance Language.instCompleteAtomicBooleanAlgebra {α : Type u_1} :

CompleteAtomicBooleanAlgebra (Language α)

Equations

Language.instCompleteAtomicBooleanAlgebra = Set.instCompleteAtomicBooleanAlgebra

source

instance Language.instZero {α : Type u_1} :

Zero (Language α)

Zero language has no elements.

Equations

Language.instZero = { zero := ∅ }

source

instance Language.instOne {α : Type u_1} :

One (Language α)

1 : Language α contains only one element [].

Equations

Language.instOne = { one := {[]} }

source

instance Language.instInhabited {α : Type u_1} :

Inhabited (Language α)

Equations

Language.instInhabited = { default := ∅ }

source

instance Language.instAdd {α : Type u_1} :

Add (Language α)

The sum of two languages is their union.

Equations

Language.instAdd = { add := fun (x1 x2 : Set (List α)) => x1 ∪ x2 }

source

instance Language.instMul {α : Type u_1} :

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

Language.instMul = { mul := Set.image2 fun (x1 x2 : List α) => x1 ++ x2 }

source

theorem Language.zero_def {α : Type u_1} :

0 = ∅

source

theorem Language.one_def {α : Type u_1} :

1 = {[]}

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 (fun (x1 x2 : List α) => x1 ++ x2) l m

source

instance Language.instKStar {α : Type u_1} :

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

Language.instKStar = { kstar := fun (l : Language α) => {x : List α | ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l} }

source

theorem Language.kstar_def {α : Type u_1} (l : Language α) :

KStar.kstar l = {x : List α | ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l}

source

theorem Language.ext {α : Type u_1} {l m : Language α} (h : ∀ (x : List α), x ∈ l ↔ x ∈ m) :

l = m

source

theorem Language.ext_iff {α : Type u_1} {l m : Language α} :

l = m ↔ ∀ (x : List α), x ∈ l ↔ x ∈ m

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 = []

source

theorem Language.nil_mem_one {α : Type u_1} :

[] ∈ 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 ∈ 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 ∈ KStar.kstar l ↔ ∃ (L : List (List α)), x = L.flatten ∧ ∀ y ∈ L, y ∈ l

source

theorem Language.join_mem_kstar {α : Type u_1} {l : Language α} {L : List (List α)} (h : ∀ y ∈ L, y ∈ l) :

L.flatten ∈ KStar.kstar l

source

theorem Language.nil_mem_kstar {α : Type u_1} (l : Language α) :

[] ∈ KStar.kstar l

source

instance Language.instSemiring {α : Type u_1} :

Semiring (Language α)

Equations

One or more equations did not get rendered due to their size.

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

Language.map f = { toFun := Set.image (List.map f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Language.map_id {α : Type u_1} (l : Language α) :

(map id) l = l

source

@[simp]

theorem Language.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (l : Language α) :

(map g) ((map f) l) = (map (g ∘ f)) l

source

theorem Language.mem_kstar_iff_exists_nonempty {α : Type u_1} {l : Language α} {x : List α} :

x ∈ KStar.kstar l ↔ ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

source

theorem Language.kstar_def_nonempty {α : Type u_1} (l : Language α) :

KStar.kstar l = {x : List α | ∃ (S : List (List α)), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

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_iSup {α : Type u_1} {ι : Sort v} {l : ι → Language α} {x : List α} :

x ∈ ⨆ (i : ι), l i ↔ ∃ (i : ι), x ∈ l i

source

theorem Language.iSup_mul {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) :

(⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m

source

theorem Language.mul_iSup {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) :

m * ⨆ (i : ι), l i = ⨆ (i : ι), m * l i

source

theorem Language.iSup_add {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) :

(⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m

source

theorem Language.add_iSup {α : 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.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l

source

theorem Language.kstar_eq_iSup_pow {α : Type u_1} (l : Language α) :

KStar.kstar l = ⨆ (i : ℕ), l ^ i

source

@[simp]

theorem Language.map_kstar {α : Type u_1} {β : Type u_2} (f : α → β) (l : Language α) :

(map f) (KStar.kstar l) = KStar.kstar ((map f) l)

source

theorem Language.mul_self_kstar_comm {α : Type u_1} (l : Language α) :

KStar.kstar l * l = l * KStar.kstar l

source

@[simp]

theorem Language.one_add_self_mul_kstar_eq_kstar {α : Type u_1} (l : Language α) :

1 + l * KStar.kstar l = KStar.kstar l

source

@[simp]

theorem Language.one_add_kstar_mul_self_eq_kstar {α : Type u_1} (l : Language α) :

1 + KStar.kstar l * l = KStar.kstar l

source

instance Language.instKleeneAlgebra {α : Type u_1} :

KleeneAlgebra (Language α)

Equations

One or more equations did not get rendered due to their size.

source

theorem Language.self_eq_mul_add_iff {α : Type u_1} {l m n : Language α} (hm : [] ∉ m) :

l = m * l + n ↔ l = KStar.kstar m * n

Arden's lemma

source

def Language.reverse {α : Type u_1} (l : Language α) :

Language α

Language l.reverse is defined as the set of words from l backwards.

Equations

l.reverse = {w : List α | w.reverse ∈ l}

Instances For

source

@[simp]

theorem Language.mem_reverse {α : Type u_1} {l : Language α} {a : List α} :

a ∈ l.reverse ↔ a.reverse ∈ l

source

theorem Language.reverse_mem_reverse {α : Type u_1} {l : Language α} {a : List α} :

a.reverse ∈ l.reverse ↔ a ∈ l

source

theorem Language.reverse_eq_image {α : Type u_1} (l : Language α) :

l.reverse = List.reverse '' l

source

@[simp]

theorem Language.reverse_zero {α : Type u_1} :

reverse 0 = 0

source

@[simp]

theorem Language.reverse_one {α : Type u_1} :

reverse 1 = 1

source

theorem Language.reverse_involutive {α : Type u_1} :

Function.Involutive reverse

source

theorem Language.reverse_bijective {α : Type u_1} :

Function.Bijective reverse

source

theorem Language.reverse_injective {α : Type u_1} :

Function.Injective reverse

source

theorem Language.reverse_surjective {α : Type u_1} :

Function.Surjective reverse

source

@[simp]

theorem Language.reverse_reverse {α : Type u_1} (l : Language α) :

l.reverse.reverse = l

source

@[simp]

theorem Language.reverse_add {α : Type u_1} (l m : Language α) :

(l + m).reverse = l.reverse + m.reverse

source

@[simp]

theorem Language.reverse_mul {α : Type u_1} (l m : Language α) :

(l * m).reverse = m.reverse * l.reverse

source

@[simp]

theorem Language.reverse_iSup {α : Type u_1} {ι : Sort u_4} (l : ι → Language α) :

(⨆ (i : ι), l i).reverse = ⨆ (i : ι), (l i).reverse

source

@[simp]

theorem Language.reverse_iInf {α : Type u_1} {ι : Sort u_4} (l : ι → Language α) :

(⨅ (i : ι), l i).reverse = ⨅ (i : ι), (l i).reverse

source

def Language.reverseIso (α : Type u_1) :

Language α ≃+* (Language α)ᵐᵒᵖ

Language.reverse as a ring isomorphism to the opposite ring.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Language.reverseIso_symm_apply (α : Type u_1) (l' : (Language α)ᵐᵒᵖ) :

(reverseIso α).symm l' = (MulOpposite.unop l').reverse

source

@[simp]

theorem Language.reverseIso_apply (α : Type u_1) (l : Language α) :

(reverseIso α) l = MulOpposite.op l.reverse

source

@[simp]

theorem Language.reverse_pow {α : Type u_1} (l : Language α) (n : ℕ) :

(l ^ n).reverse = l.reverse ^ n

source

@[simp]

theorem Language.reverse_kstar {α : Type u_1} (l : Language α) :

(KStar.kstar l).reverse = KStar.kstar l.reverse

source

inductive Symbol (T : Type u_4) (N : Type u_5) :

Type (max u_4 u_5)

Symbols for use by all kinds of grammars.

terminal {T : Type u_4} {N : Type u_5} (t : T) : Symbol T N
Terminal symbols (of the same type as the language)
nonterminal {T : Type u_4} {N : Type u_5} (n : N) : Symbol T N
Nonterminal symbols (must not be present when the word being generated is finalized)