LR(k) grammars and deterministic pushdown automata

For every fixed positive amount of lookahead, LR(k) grammars generate exactly the languages accepted by deterministic pushdown automata. The same is true of the existential finite-lookahead LR class.

theorem is_LRk_iff_is_DPDA {T : Type} [Fintype T] {k : ℕ} (hk : 0 < k) {L : Language T} : is_LRk k L ↔ is_DPDA L

For every positive k, LR(k) languages are exactly DPDA languages.

theorem is_LR_iff_is_DPDA {T : Type} [Fintype T] {L : Language T} : is_LR L ↔ is_DPDA L

The existential finite-lookahead LR class is exactly the DPDA class.

theorem LRk_eq_DPDA {T : Type} [Fintype T] (k : ℕ) (hk : 0 < k) : LRk k = DPDA.Class

Equality of the fixed positive-lookahead LR(k) and DPDA language classes.

theorem LR_eq_DPDA {T : Type} [Fintype T] : LR = DPDA.Class

Equality of the existential finite-lookahead LR and DPDA classes.

theorem is_LRk_iff_is_DCF {T : Type} [Fintype T] {k : ℕ} (hk : 0 < k) {L : Language T} : is_LRk k L ↔ is_DCF L

DCF is the conventional class name for the same fixed positive-lookahead equivalence.

theorem is_LR_iff_is_DCF {T : Type} [Fintype T] {L : Language T} : is_LR L ↔ is_DCF L

Existential finite-lookahead LR languages are exactly deterministic context-free languages.

theorem LRk_eq_DCF {T : Type} [Fintype T] (k : ℕ) (hk : 0 < k) : LRk k = DCF

Class equality between fixed positive-lookahead LR(k) and DCF.

theorem LR_eq_DCF {T : Type} [Fintype T] : LR = DCF

Class equality between existential finite-lookahead LR and DCF.