RE Closure Under String Homomorphism

This file proves that the class of recursively enumerable languages is closed under string homomorphism. It also provides a grammar construction for the ε-free case, where no symbol is erased.

Proof idea for arbitrary finite-alphabet homomorphisms: a word w is in the homomorphic image iff there exists a source word x and a derivation witness for x in the original grammar such that x.flatMap h = w. This existential search is computable over finite alphabets, so the search-to-TM and TM-to-RE bridges produce the RE witness.

Given an unrestricted grammar g over terminals α generating L, and an ε-free string homomorphism h : α → List β, we construct an unrestricted grammar hom_grammar g h over terminals β whose language is L.homomorphicImage h.

Main declarations

• hom_grammar
• RE_closed_under_homomorphism
• RE_closedUnderHomomorphism
• RE_closed_under_epsfree_homomorphism

Note on erasing homomorphisms

The two-phase grammar construction hom_grammar is correct only for ε-free homomorphisms (where h a ≠ [] for all a). For erasing homomorphisms (where some h a = []), the Phase 2 expansion can remove nonterminal placeholders, which may create new adjacencies that enable Phase 1 rules that have no corresponding rule application in the original grammar. A correct construction for the general case would require a more sophisticated mechanism (e.g., a scanning phase to ensure Phase 1 is complete before Phase 2 begins).

def homLiftSym {α β N : Type} : symbol α N → symbol β (N ⊕ α)

Map a symbol by replacing terminals with nonterminal placeholders.

Equations

• homLiftSym (symbol.terminal a) = symbol.nonterminal (Sum.inr a)
• homLiftSym (symbol.nonterminal n) = symbol.nonterminal (Sum.inl n)

def homLiftStr {α β N : Type} (s : List (symbol α N)) : List (symbol β (N ⊕ α))

Lift an entire string to placeholder form.

Equations

• homLiftStr s = List.map homLiftSym s

def homLiftRule {α β N : Type} (r : grule α N) : grule β (N ⊕ α)

Lift a rule to phase 1 form.

Equations

• homLiftRule r = { input_L := homLiftStr r.input_L, input_N := Sum.inl r.input_N, input_R := homLiftStr r.input_R, output_string := homLiftStr r.output_string }

def homExpandRule {α β N : Type} (h : α → List β) (a : α) : grule β (N ⊕ α)

Create a phase 2 rule for terminal a.

Equations

• homExpandRule h a = { input_L := [], input_N := Sum.inr a, input_R := [], output_string := List.map symbol.terminal (h a) }

def hom_grammar {α β : Type} (g : grammar α) (h : α → List β) : grammar β

The two-phase grammar for the homomorphic image.

Equations

• hom_grammar g h = { nt := g.nt ⊕ α, initial := Sum.inl g.initial, rules := List.map homLiftRule g.rules ++ List.map (homExpandRule h) (all_used_terminals g) }

theorem homLiftStr_map_terminal {α β : Type} {g : grammar α} (w : List α) : homLiftStr (List.map symbol.terminal w) = List.map (fun (a : α) => symbol.nonterminal (Sum.inr a)) w

theorem mem_prod_singletons_iff_flatMap {α β : Type} (w : List α) (h : α → List β) (u : List β) : u ∈ (List.map (fun (a : α) => {h a}) w).prod ↔ u = List.flatMap h w

theorem hom_grammar_language_epsfree {α β : Type} (g : grammar α) (h : α → List β) (heps : IsEpsFreeHomomorphism h) : grammar_language (hom_grammar g h) = (grammar_language g).homomorphicImage h

The ε-free homomorphic-image grammar generates exactly the homomorphic image.

def reHomomorphismTest {α β : Type} [DecidableEq α] [DecidableEq β] (g : grammar α) [DecidableEq g.nt] (h : α → List β) (p : List α × List (ℕ × ℕ)) (w : List β) : Bool

Search test for the homomorphic image of a grammar language.

The witness contains both a preimage word and a derivation sequence for that preimage.

Equations

• reHomomorphismTest g h p w = (grammarTest g p.2 p.1 && decide (List.flatMap h p.1 = w))

theorem reHomomorphismTest_computable₂ {α β : Type} [DecidableEq α] [DecidableEq β] [Primcodable α] [Primcodable β] [Finite α] (g : grammar α) [DecidableEq g.nt] [Primcodable g.nt] (h : α → List β) : Computable₂ (reHomomorphismTest g h)

The homomorphic-image search test is computable over finite source alphabets.

theorem RE_closed_under_homomorphism {α β : Type} [Fintype α] [Fintype β] (L : Language α) (h : α → List β) (hL : is_RE L) : is_RE (L.homomorphicImage h)

The class of RE languages is closed under arbitrary finite-alphabet string homomorphism.

theorem RE_closedUnderHomomorphism : ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_RE

The class of recursively enumerable languages is closed under string homomorphism.

theorem RE_closed_under_epsfree_homomorphism {α β : Type} (L : Language α) (h : α → List β) (hL : is_RE L) (heps : IsEpsFreeHomomorphism h) : is_RE (L.homomorphicImage h)

The class of RE languages is closed under ε-free string homomorphism.

theorem RE_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_RE

The class of recursively enumerable languages is closed under ε-free string homomorphism.