Recursively enumerable languages as erasing images of non-contracting languages

This file implements the standard padding construction for unrestricted grammars. A rule whose output is shorter than its input emits enough padding symbols to preserve length. The padding symbols then commute to the right and survive as terminals in the generated word; an erasing homomorphism removes them again.

The construction first restricts the source grammar to its finitely many used nonterminals. For a grammar with finite terminal and nonterminal alphabets, its simulation uses:

• some t for an original terminal t and none for terminal padding;
• some A for an original nonterminal A and none for the padding nonterminal;
• one padded copy of every source rule;
• rules moving the padding nonterminal rightward across every terminal and nonterminal; and
• one rule converting the padding nonterminal to the padding terminal.

Projection erases padding and recovers every simulated source step. Conversely, padding can be moved across the untouched right context after every source step, so every source derivation lifts to the new grammar.

This is the grammar-theoretic core of the classical fact that every recursively enumerable language is a homomorphic image of a context-sensitive language.

Main declarations

• erasePadding — the homomorphism deleting the padding terminal;
• erasingImageGrammar — the non-contracting padded simulation of an arbitrary grammar;
• erasingImageGrammar_noncontracting — every rule of the simulation is non-contracting;
• erasingImageGrammar_language — erasing padding recovers the source language;
• exists_noncontracting_erasingImage — language-level packaging of the construction.

Reference

J. E. Hopcroft and J. D. Ullman, Formal Languages and Their Relation to Automata, Theorem 9.9 and Corollary 9.3, 1969.

def Grammar.ErasingImage.erasePadding {T : Type} : Option T → List T

Delete padding terminals and retain original terminals.

Equations

• Grammar.ErasingImage.erasePadding (some t) = [t]
• Grammar.ErasingImage.erasePadding none = []

def Grammar.ErasingImage.liftSymbol {T N : Type} : symbol T N → symbol (Option T) (Option N)

Embed one source symbol into the padded grammar.

Equations

• Grammar.ErasingImage.liftSymbol (symbol.terminal t) = symbol.terminal (some t)
• Grammar.ErasingImage.liftSymbol (symbol.nonterminal A) = symbol.nonterminal (some A)

def Grammar.ErasingImage.liftString {T N : Type} (w : List (symbol T N)) : List (symbol (Option T) (Option N))

Embed a source sentential form into the padded grammar symbol by symbol.

Equations

• Grammar.ErasingImage.liftString w = List.map Grammar.ErasingImage.liftSymbol w

def Grammar.ErasingImage.paddingSymbol {T N : Type} : symbol (Option T) (Option N)

The nonterminal used while padding is moved to the right edge.

Equations

• Grammar.ErasingImage.paddingSymbol = symbol.nonterminal none

def Grammar.ErasingImage.paddingTerminal {T N : Type} : symbol (Option T) (Option N)

The terminal padding symbol that survives in a generated padded word.

Equations

• Grammar.ErasingImage.paddingTerminal = symbol.terminal none

def Grammar.ErasingImage.inputLength {T N : Type} (r : grule T N) : ℕ

Length of a rule's complete left-hand side.

Equations

• Grammar.ErasingImage.inputLength r = r.input_L.length + 1 + r.input_R.length

def Grammar.ErasingImage.paddingCount {T N : Type} (r : grule T N) : ℕ

Number of padding symbols needed to make a source rule non-contracting.

Equations

• Grammar.ErasingImage.paddingCount r = Grammar.ErasingImage.inputLength r - r.output_string.length

def Grammar.ErasingImage.paddingString {T N : Type} (n : ℕ) : List (symbol (Option T) (Option N))

A block of padding nonterminals.

Equations

• Grammar.ErasingImage.paddingString n = List.replicate n Grammar.ErasingImage.paddingSymbol

def Grammar.ErasingImage.paddedRule {T N : Type} (r : grule T N) : grule (Option T) (Option N)

A source rule with enough padding appended to make it non-contracting.

Equations

• One or more equations did not get rendered due to their size.

def Grammar.ErasingImage.swapRule {T N : Type} (s : symbol T N) : grule (Option T) (Option N)

Move the padding nonterminal one position to the right across a lifted source symbol.

Equations

• One or more equations did not get rendered due to their size.

def Grammar.ErasingImage.finishPaddingRule {T N : Type} : grule (Option T) (Option N)

Convert the padding nonterminal into the padding terminal.

Equations

• Grammar.ErasingImage.finishPaddingRule = { input_L := [], input_N := none, input_R := [], output_string := [Grammar.ErasingImage.paddingTerminal] }

noncomputable def Grammar.ErasingImage.activeSymbols {T N : Type} [Fintype T] [Fintype N] : List (symbol T N)

The finite list of source symbols across which padding may have to move.

Equations

• Grammar.ErasingImage.activeSymbols = List.map symbol.terminal Finset.univ.toList ++ List.map symbol.nonterminal Finset.univ.toList

noncomputable def Grammar.ErasingImage.swapRules {T N : Type} [Fintype T] [Fintype N] : List (grule (Option T) (Option N))

Commuting rules for every symbol of finite terminal and nonterminal alphabets.

Equations

• Grammar.ErasingImage.swapRules = List.map Grammar.ErasingImage.swapRule Grammar.ErasingImage.activeSymbols

noncomputable def Grammar.ErasingImage.finiteErasingImageGrammar {T : Type} [Fintype T] (g : grammar T) [Fintype g.nt] : grammar (Option T)

Padded simulation for a grammar whose terminal and nonterminal alphabets are finite.

Equations

• One or more equations did not get rendered due to their size.

theorem Grammar.ErasingImage.finiteErasingImageGrammar_noncontracting {T : Type} [Fintype T] (g : grammar T) [Fintype g.nt] : grammar_noncontracting (finiteErasingImageGrammar g)

Every rule of the finite padded simulation is non-contracting.

Projection and soundness

Padding motion and completeness

Language equivalence

def Grammar.ErasingImage.paddedTerminalWord {T : Type} (w : List T) (k : ℕ) : List (Option T)

Embed a terminal word and append k padding terminals.

Equations

• Grammar.ErasingImage.paddedTerminalWord w k = List.map some w ++ List.replicate k none

theorem Grammar.ErasingImage.finiteErasingImageGrammar_language {T : Type} [Fintype T] (g : grammar T) [Fintype g.nt] : (grammar_language (finiteErasingImageGrammar g)).homomorphicImage erasePadding = grammar_language g

Erasing the padding terminals from the finite padded simulation recovers exactly the source grammar's language.

noncomputable def Grammar.ErasingImage.erasingImageGrammar {T : Type} [Fintype T] (g : grammar T) : grammar (Option T)

The padded simulation of an arbitrary grammar. Restricting to the nonterminals occurring in its finite rule list supplies the finite alphabet needed to enumerate the commuting rules.

Equations

• Grammar.ErasingImage.erasingImageGrammar g = Grammar.ErasingImage.finiteErasingImageGrammar (restrictGrammar g)

theorem Grammar.ErasingImage.erasingImageGrammar_noncontracting {T : Type} [Fintype T] (g : grammar T) : grammar_noncontracting (erasingImageGrammar g)

The padded simulation of an arbitrary grammar is non-contracting.

theorem Grammar.ErasingImage.erasingImageGrammar_language {T : Type} [Fintype T] (g : grammar T) : (grammar_language (erasingImageGrammar g)).homomorphicImage erasePadding = grammar_language g

Erasing padding from the padded simulation of an arbitrary grammar recovers its language.

theorem Grammar.ErasingImage.erasingImageGrammar_generates_padded {T : Type} [Fintype T] (g : grammar T) {w : List T} (hw : grammar_generates g w) : ∃ (k : ℕ), grammar_generates (erasingImageGrammar g) (paddedTerminalWord w k)

Every source word has a representative generated by erasingImageGrammar whose padding occurs entirely as a terminal suffix. This is the non-erasing witness used by quotient reductions.

theorem Grammar.ErasingImage.erasingImageGrammar_generates_project {T : Type} [Fintype T] (g : grammar T) {w : List (Option T)} (hw : grammar_generates (erasingImageGrammar g) w) : grammar_generates g (List.flatMap erasePadding w)

Projecting any terminal word generated by erasingImageGrammar gives a terminal word of the source grammar.

theorem Grammar.ErasingImage.exists_noncontracting_erasingImage {T : Type} [Fintype T] (g : grammar T) : ∃ (K : Language (Option T)), is_noncontracting K ∧ K.homomorphicImage erasePadding = grammar_language g

Every unrestricted grammar language is the erasing homomorphic image of a non-contracting language.