Recursive Closure Under Inverse Homomorphism

This file proves that recursive languages over finite alphabets are closed under inverse string homomorphism.

Membership in the inverse image {w | w.flatMap h ∈ L} is decided by computing w.flatMap h and running the decider for L.

theorem is_Recursive_inverseHomomorphism {α β : Type} [Fintype α] [Fintype β] (L : Language β) (h : α → List β) : is_Recursive L → is_Recursive {w : List α | List.flatMap h w ∈ L}

Recursive languages over finite alphabets are closed under inverse string homomorphism.

theorem Recursive_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => is_Recursive

The class of recursive languages is closed under inverse string homomorphism.