The characteristic grammar of a deterministic pushdown automaton

This file fixes the construction used in the DPDA-to-LR(1) direction.

First, DPDA.firstFinal marks an epsilon phase after it has left a final state. The standard final-state-to-empty-stack conversion is then applied, followed by the standard PDA characteristic grammar. Finally, rules which are not fully productive are removed. Removing those rules is essential for the LR argument: the target states guessed by the characteristic grammar must actually be realizable by a computation.

noncomputable def DPDA_to_LR.emptyStackPDA {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : PDA (Q × Bool ⊕ Fin 2) T (Option S)

The normalized PDA accepting by empty stack.

Equations

• DPDA_to_LR.emptyStackPDA M = PDA_FS_to_ES_pda M.firstFinal.toPDA

noncomputable def DPDA_to_LR.mathlibCharacteristicGrammar {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : ContextFreeGrammar T

Mathlib's characteristic grammar for the normalized empty-stack PDA.

Equations

• DPDA_to_LR.mathlibCharacteristicGrammar M = PDA_to_CFG.G (DPDA_to_LR.emptyStackPDA M)

noncomputable def DPDA_to_LR.rawCharacteristicGrammar {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : CF_grammar T

The same characteristic grammar in Langlib's CF_grammar representation.

Equations

• DPDA_to_LR.rawCharacteristicGrammar M = cfg_of_mathlib_cfg (DPDA_to_LR.mathlibCharacteristicGrammar M)

noncomputable def DPDA_to_LR.characteristicGrammar {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : CF_grammar T

The reduced characteristic grammar used for the LR(1) proof.

Equations

• DPDA_to_LR.characteristicGrammar M = productiveGrammar (DPDA_to_LR.rawCharacteristicGrammar M)

@[simp]

theorem DPDA_to_LR.characteristicGrammar_nt {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : (characteristicGrammar M).nt = PDA_to_CFG.N (emptyStackPDA M)

@[simp]

theorem DPDA_to_LR.characteristicGrammar_initial {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : (characteristicGrammar M).initial = PDA_to_CFG.N.start

theorem DPDA_to_LR.characteristicGrammar_language {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : CF_language (characteristicGrammar M) = M.acceptsByFinalState

The complete language-equality chain for the characteristic grammar.