RE Closure Under Substitution

This file proves that recursively enumerable languages over finite alphabets are closed under finite-alphabet substitution. The key result is RE_closedUnderSubstitution: encode each substituted symbol as a block inl a :: map inr u, take the Kleene star of the RE block language, restrict the projected source word to the original RE language by inverse homomorphism and intersection, then erase the source-symbol markers by homomorphism.

Main declarations

• RE_of_subst_RE
• RE_closedUnderSubstitution

theorem RE_of_finite_iUnion {α ι : Type} [Fintype α] [Fintype ι] (L : ι → Language α) (hL : ∀ (i : ι), is_RE (L i)) : is_RE (⋃ (i : ι), L i)

RE languages are closed under finite indexed union.

def Language.substProj {α β : Type} (x : α ⊕ β) : List α

Projection from encoded substitution blocks to the source alphabet.

Equations

• Language.substProj (Sum.inl a) = [a]
• Language.substProj (Sum.inr val) = []

def Language.substErase {α β : Type} (x : α ⊕ β) : List β

Erasure from encoded substitution blocks to the target alphabet.

Equations

• Language.substErase (Sum.inl a) = []
• Language.substErase (Sum.inr val) = [val]

@[simp]

theorem Language.substProj_map_inr {α β : Type} (u : List β) : List.flatMap substProj (List.map Sum.inr u) = []

@[simp]

theorem Language.substErase_map_inr {α β : Type} (u : List β) : List.flatMap substErase (List.map Sum.inr u) = u

def Language.substBlock {α β : Type} (f : α → Language β) : Language (α ⊕ β)

The language of one encoded substitution block.

Equations

• Language.substBlock f = ⋃ (a : α), {[Sum.inl a]} * (f a).homomorphicImage fun (b : β) => [Sum.inr b]

@[simp]

theorem Language.substProj_block {α β : Type} (a : α) (u : List β) : List.flatMap substProj (Sum.inl a :: List.map Sum.inr u) = [a]

@[simp]

theorem Language.substErase_block {α β : Type} (a : α) (u : List β) : List.flatMap substErase (Sum.inl a :: List.map Sum.inr u) = u

theorem Language.mem_homomorphicImage_iff_flatMap {α β : Type} (L : Language α) (h : α → List β) (w : List β) : w ∈ L.homomorphicImage h ↔ ∃ x ∈ L, List.flatMap h x = w

theorem Language.mem_substBlock_iff {α β : Type} (f : α → Language β) (z : List (α ⊕ β)) : z ∈ substBlock f ↔ ∃ (a : α), ∃ u ∈ f a, z = Sum.inl a :: List.map Sum.inr u

theorem Language.subst_coding_eq_subst {α β : Type} (L : Language α) (f : α → Language β) : (KStar.kstar (substBlock f) ⊓ {y : List (α ⊕ β) | List.flatMap substProj y ∈ L}).homomorphicImage substErase = L.subst f

theorem RE_of_substBlock_RE {α β : Type} [Fintype α] [Fintype β] (f : α → Language β) (hf : ∀ (a : α), is_RE (f a)) : is_RE (Language.substBlock f)

The encoded single-block language for an RE substitution family is RE.

theorem RE_of_subst_RE {α β : Type} [Fintype α] [Fintype β] (L : Language α) (f : α → Language β) (hL : is_RE L) (hf : ∀ (a : α), is_RE (f a)) : is_RE (L.subst f)

RE languages over finite alphabets are closed under substitution.

theorem RE_closedUnderSubstitution : ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_RE

The class of recursively enumerable languages is closed under substitution.