Closure Properties of Formal Language Classes

Vocabulary for formal languages and string homomorphisms, plus the closure properties of context-free languages.

CFL Closure Properties

Context-free languages are closed under string homomorphisms and under intersection with regular languages (Hopcroft & Ullman 1979, pp. 130–135).

@cite{shieber-1985}'s proof uses the contrapositive: if applying a homomorphism f to a language L and intersecting with a regular language r produces a non-context-free result, then L is not context-free.

@[reducible, inline]

abbrev Language (α : Type) : Type

A formal language over alphabet α: a decidable predicate on strings.

Equations

• Language α = (List α → Bool)

@[reducible, inline]

abbrev StringHom (α β : Type) : Type

A string homomorphism: maps each source symbol to a target string. Extends to strings by concatenation: h(ε) = ε, h(a·w) = h(a) ++ h(w).

Equations

• StringHom α β = (α → List β)

def StringHom.applyTo {α β : Type} (h : StringHom α β) : List α → List β

Apply a string homomorphism to a string.

Equations

• h.applyTo [] = []
• h.applyTo (a :: w) = h a ++ h.applyTo w

def StringHom.letterMap {α β : Type} (f : α → β) : StringHom α β

A letter-to-letter homomorphism: each source symbol maps to exactly one target symbol. This is the case used by @cite{shieber-1985}.

Equations

• StringHom.letterMap f a = [f a]

theorem StringHom.applyTo_letterMap {α β : Type} (f : α → β) (w : List α) : (letterMap f).applyTo w = List.map f w

def Language.inter {α : Type} (L₁ L₂ : Language α) : Language α

Intersection of two languages.

Equations

• L₁.inter L₂ w = (L₁ w && L₂ w)