Non-contracting grammars and context-preserving grammars

This file completes the hard direction of the classical equivalence between non-contracting unrestricted grammars and non-erasing context-preserving grammars.

The terminal alphabet of a grammar is always finitely supported, even when its ambient terminal type is arbitrary. We therefore first restrict a non-contracting language to that finite support, use the Kuroda--Myhill CS = LBA development to obtain a context-preserving grammar there, and finally embed that grammar back into the ambient terminal type.

The last operation is proved below without a finiteness assumption on the target type. Original terminals are kept as private nonterminals while the source grammar runs and are converted to ambient terminals only by final one-symbol rules. Projecting such a derivation back either gives a source-grammar step or a stuttering step, which proves soundness even when the final conversions are interleaved with simulation steps.

inductive CSGTerminalEmbedding.NT {A : Type} (N : Type) : Type

Nonterminals used when embedding a context-preserving grammar's terminal alphabet.

• source {A N : Type} : N → NT N
• terminal {A N : Type} : A → NT N

def CSGTerminalEmbedding.liftSymbol {A T N : Type} : symbol A N → symbol T (NT N)

Lift every source symbol to a nonterminal over the target terminal alphabet.

Equations

• CSGTerminalEmbedding.liftSymbol (symbol.terminal a) = symbol.nonterminal (CSGTerminalEmbedding.NT.terminal a)
• CSGTerminalEmbedding.liftSymbol (symbol.nonterminal n) = symbol.nonterminal (CSGTerminalEmbedding.NT.source n)

def CSGTerminalEmbedding.liftRule {A T N : Type} (r : csrule A N) : csrule T (NT N)

Lift a source context-preserving rule.

Equations

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

def CSGTerminalEmbedding.terminalRule {A T N : Type} (f : A → T) (a : A) : csrule T (NT N)

Convert one private source-terminal nonterminal to its ambient terminal.

Equations

• CSGTerminalEmbedding.terminalRule f a = { context_left := [], input_nonterminal := CSGTerminalEmbedding.NT.terminal a, context_right := [], output_string := [symbol.terminal (f a)] }

noncomputable def CSGTerminalEmbedding.grammar {A T : Type} [Fintype A] [DecidableEq A] (g : CS_grammar A) (f : A ↪ T) : CS_grammar T

Embed a context-preserving grammar along an injective terminal map.

Equations

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

noncomputable def CSGTerminalEmbedding.projectSymbol {A T : Type} [Nonempty A] {N : Type} (f : A ↪ T) : symbol T (NT N) → symbol A N

Project an embedded sentential symbol to the source grammar. Ambient terminals not in the embedding's range may be sent to the arbitrary invFun default; the support invariant below proves that no such terminal is reachable.

Equations

• CSGTerminalEmbedding.projectSymbol f (symbol.terminal t) = symbol.terminal (Function.invFun (⇑f) t)
• CSGTerminalEmbedding.projectSymbol f (symbol.nonterminal (CSGTerminalEmbedding.NT.source n)) = symbol.nonterminal n
• CSGTerminalEmbedding.projectSymbol f (symbol.nonterminal (CSGTerminalEmbedding.NT.terminal a)) = symbol.terminal a

def CSGTerminalEmbedding.Supported {A T N : Type} (f : A ↪ T) (s : List (symbol T (NT N))) : Prop

All ambient terminals in a sentential form lie in the embedding's range.

Equations

• CSGTerminalEmbedding.Supported f s = ∀ (t : T), symbol.terminal t ∈ s → ∃ (a : A), f a = t

theorem CSGTerminalEmbedding.language_eq_map {A T : Type} [Fintype A] [DecidableEq A] [Nonempty A] (g : CS_grammar A) (f : A ↪ T) : CS_language (grammar g f) = (Language.map ⇑f) (CS_language g)

Embedding a finite source terminal alphabet along an injection produces exactly the language image, while the target terminal type remains completely arbitrary.

theorem is_CS_via_csg_of_is_noncontracting {T : Type} {L : Language T} (hL : is_noncontracting L) : is_CS_via_csg L

Non-contracting implies non-erasing context-preserving, for an arbitrary terminal type. No finiteness hypothesis is imposed on the ambient alphabet; only the finite support actually occurring in the source grammar is used internally.

theorem is_noncontracting_iff_is_CS_via_csg {T : Type} {L : Language T} : is_noncontracting L ↔ is_CS_via_csg L

The classical equivalence between non-contracting unrestricted grammars and non-erasing context-preserving grammars, uniformly over every terminal type.