Recursive Non-Closure Under String Homomorphism

Recursive languages are not closed under arbitrary string homomorphisms. The counterexample uses an erasing homomorphism: a recursive source language stores a bounded halting witness in symbols that are erased by the homomorphism. After erasure, membership is exactly the unary halting problem.

theorem Recursive_notClosedUnderHomomorphism : ¬ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_Recursive

Recursive languages are not closed under arbitrary string homomorphism.