Recursive Closure Under ε-Free Homomorphism

This file proves that recursive languages over finite alphabets are closed under ε-free string homomorphisms.

For a target word u, any source word w with w.flatMap h = u has w.length ≤ u.length, because each source symbol maps to a nonempty word. The decider therefore enumerates all source words of length at most u.length, tests membership in the original recursive language, and checks w.flatMap h = u.

theorem is_Recursive_epsFreeHomomorphism {α β : Type} [Fintype α] [Fintype β] (L : Language α) (h : α → List β) (heps : IsEpsFreeHomomorphism h) : is_Recursive L → is_Recursive (L.homomorphicImage h)

Recursive languages over finite alphabets are closed under ε-free string homomorphism.

theorem Recursive_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_Recursive

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