RE Closure Under Inverse Homomorphism

This file proves that recursively enumerable languages over finite alphabets are closed under inverse string homomorphism. The key result is RE_of_inverseHomomorphism_RE: for a fixed finite-alphabet homomorphism h : α → List β, the preprocessing map w ↦ w.flatMap h is primitive recursive, so a grammar-membership search for L can be reused as a search for the preimage {w | w.flatMap h ∈ L}.

Main declarations

• primrec_flatMap_finite
• reInverseHomomorphismTest
• reInverseHomomorphismTest_computable₂
• RE_of_inverseHomomorphism_RE
• RE_closedUnderInverseHomomorphism

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

Search test for the inverse homomorphic image of a grammar language.

Equations

• reInverseHomomorphismTest g h seq w = grammarTest g seq (List.flatMap h w)

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

The inverse-homomorphism grammar search test is computable.

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

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

theorem RE_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => is_RE

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