String Homomorphism

A string homomorphism h : α → List β extends to words by concatenation: h(a₁a₂…aₙ) = h(a₁) ++ h(a₂) ++ … ++ h(aₙ). The image of a language L under h is {h(w) | w ∈ L}.

This is a special case of substitution where each symbol a is mapped to the singleton language {h(a)}.

def Language.homomorphicImage {α β : Type} (L : Language α) (h : α → List β) : Language β

The image of a language L under a string homomorphism h.

Equations

• L.homomorphicImage h = L.subst fun (a : α) => {h a}

def IsEpsFreeHomomorphism {α β : Type} (h : α → List β) : Prop

A string homomorphism is ε-free if no symbol maps to the empty string.

Equations

• IsEpsFreeHomomorphism h = ∀ (a : α), h a ≠ []