Langlib

Langlib.Classes.Regular.Closure.Bijection

Regular Closure Under Terminal Bijection #

Proof idea: a bijection of terminals is just a relabeling of the input alphabet. Transport the automaton transitions along the equivalence, and use the inverse map for the reverse direction.

Regular Closure Under Terminal Bijection #

This file packages regular-language transport lemmas for renaming terminals.

Main declarations #

source
theorem Language.IsRegular.preimage {α : Type u_1} {β : Type u_2} {L : Language α} (h : L.IsRegular) (f : β → α) :
IsRegular (List.map f ⁻¹' L)

Regular languages are closed under preimage along List.map.

source
theorem Language.IsRegular.of_map_injective {α : Type u_1} {β : Type u_2} {L : Language α} {f : α → β} (hf : Function.Injective f) (h : ((map f) L).IsRegular) :
L.IsRegular

Injective alphabet maps reflect regularity.

source
theorem isRegular_of_bijemap_isRegular {T₁ : Type u_1} {T₂ : Type u_2} (π : T₁ ≃ T₂) (L : Language T₁) :
L.IsRegular → (L.bijemapLang π).IsRegular

Regular languages are closed under bijections of the terminal alphabet.

source
theorem isRegular_of_bijemap_isRegular_rev {T₁ : Type u_1} {T₂ : Type u_2} (π : T₁ ≃ T₂) (L : Language T₁) :
(L.bijemapLang π).IsRegular → L.IsRegular

Reverse direction of isRegular_of_bijemap_isRegular.

source
@[simp]
theorem isRegular_bijemap_iff_isRegular {T₁ : Type u_1} {T₂ : Type u_2} (π : T₁ ≃ T₂) (L : Language T₁) :
(L.bijemapLang π).IsRegular ↔ L.IsRegular

A language is regular iff its image under a bijection of terminal alphabets is regular.