Grammar Inverse Homomorphism

Given a grammar g over terminal alphabet Γ and a map encode : T → Γ (with [Fintype T]), we construct a grammar GrammarPullback.pullbackGrammar g encode over terminal alphabet T such that:

w ∈ grammar_language (pullbackGrammar g encode) ↔ w.map encode ∈ grammar_language g

This is the inverse-homomorphism construction used to change the terminal alphabet of a grammar along an encoding function.

Key results

• GrammarPullback.pullbackGrammar: constructs the pulled-back grammar.
• GrammarPullback.pullbackGrammar_language: proves w ∈ pullbackGrammar g encode iff w.map encode ∈ grammar_language g.

Symbol maps

def GrammarPullback.liftSym {T Γ NT : Type} : symbol Γ NT → symbol T (NT ⊕ Γ)

Lift symbols from g (over Γ) to the pullback grammar (over T). Terminals become decoding nonterminals; nonterminals are tagged.

Equations

• GrammarPullback.liftSym (symbol.terminal γ) = symbol.nonterminal (Sum.inr γ)
• GrammarPullback.liftSym (symbol.nonterminal n) = symbol.nonterminal (Sum.inl n)

def GrammarPullback.projSym {T Γ NT : Type} (encode : T → Γ) : symbol T (NT ⊕ Γ) → symbol Γ NT

Project symbols from the pullback grammar back to g. Terminals in T are mapped via encode; nonterminals are untagged.

Equations

• GrammarPullback.projSym encode (symbol.terminal t) = symbol.terminal (encode t)
• GrammarPullback.projSym encode (symbol.nonterminal (Sum.inl n)) = symbol.nonterminal n
• GrammarPullback.projSym encode (symbol.nonterminal (Sum.inr γ)) = symbol.terminal γ

theorem GrammarPullback.projSym_liftSym {T Γ NT : Type} (encode : T → Γ) (s : symbol Γ NT) : projSym encode (liftSym s) = s

theorem GrammarPullback.map_projSym_map_liftSym {T Γ NT : Type} (encode : T → Γ) (l : List (symbol Γ NT)) : List.map (projSym encode) (List.map liftSym l) = l

Pullback grammar construction

def GrammarPullback.liftRule {T Γ NT : Type} (r : grule Γ NT) : grule T (NT ⊕ Γ)

Lift a grammar rule from g to the pullback grammar.

Equations

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

def GrammarPullback.decodeRule {T Γ NT : Type} (encode : T → Γ) (t : T) : grule T (NT ⊕ Γ)

A decode rule: (Sum.inr (encode t)) → [terminal t].

Equations

• GrammarPullback.decodeRule encode t = { input_L := [], input_N := Sum.inr (encode t), input_R := [], output_string := [symbol.terminal t] }

noncomputable def GrammarPullback.pullbackGrammar {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] : grammar T

The pullback grammar: given grammar g over Γ and encode : T → Γ, produces a grammar over T that generates w iff g generates w.map encode.

Equations

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

Forward direction: pullback generates ⟹ g generates encoded

theorem GrammarPullback.transforms_proj {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (sf₁ sf₂ : List (symbol T (g.nt ⊕ Γ))) (h : grammar_transforms (pullbackGrammar g encode) sf₁ sf₂) : grammar_derives g (List.map (projSym encode) sf₁) (List.map (projSym encode) sf₂)

theorem GrammarPullback.derives_proj {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (sf₁ sf₂ : List (symbol T (g.nt ⊕ Γ))) (h : grammar_derives (pullbackGrammar g encode) sf₁ sf₂) : grammar_derives g (List.map (projSym encode) sf₁) (List.map (projSym encode) sf₂)

theorem GrammarPullback.pullback_generates_implies_original {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (w : List T) (h : w ∈ grammar_language (pullbackGrammar g encode)) : List.map encode w ∈ grammar_language g

Backward direction: g generates encoded ⟹ pullback generates

theorem GrammarPullback.pullback_transforms_of_transforms {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (sf₁ sf₂ : List (symbol Γ g.nt)) (h : grammar_transforms g sf₁ sf₂) : grammar_transforms (pullbackGrammar g encode) (List.map liftSym sf₁) (List.map liftSym sf₂)

theorem GrammarPullback.pullback_derives_of_derives {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (sf₁ sf₂ : List (symbol Γ g.nt)) (h : grammar_derives g sf₁ sf₂) : grammar_derives (pullbackGrammar g encode) (List.map liftSym sf₁) (List.map liftSym sf₂)

theorem GrammarPullback.decode_all {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (w : List T) : grammar_derives (pullbackGrammar g encode) (List.map (fun (t : T) => symbol.nonterminal (Sum.inr (encode t))) w) (List.map symbol.terminal w)

theorem GrammarPullback.original_generates_implies_pullback {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (w : List T) (h : List.map encode w ∈ grammar_language g) : w ∈ grammar_language (pullbackGrammar g encode)

Main theorem

theorem GrammarPullback.pullbackGrammar_language {T Γ : Type} (g : grammar Γ) (encode : T → Γ) [Fintype T] (w : List T) : w ∈ grammar_language (pullbackGrammar g encode) ↔ List.map encode w ∈ grammar_language g

Pullback grammar language: The pullback grammar generates w iff g generates w.map encode.