Langlib

Langlib.Classes.DeterministicContextFree.Inclusion.StrictContextFree

DCFs are a strict subset of CFLs #

This file records the closure-mismatch route to strictness for the inclusion DCF ⊆ CF.

source
theorem DCF_strict_subclass_CF_of_closedUnderComplement_of_three {T : Type} [Fintype T] (a b c : T) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hDCFcomp : ClosedUnderComplement is_DCF) :
DCF ⊂ CF

If deterministic context-free languages are closed under complement over an alphabet with 3 distinguished elements, then they form a strict subclass of context-free languages over that alphabet.

source
theorem DCF_strict_subclass_CF_of_closedUnderComplement_of_card {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) (hDCFcomp : ClosedUnderComplement is_DCF) :
DCF ⊂ CF

If deterministic context-free languages are closed under complement over a finite alphabet with at least 3 elements, then they form a strict subclass of context-free languages over that alphabet.

source
theorem DCF_strict_subclass_CF_of_card {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) :
DCF ⊂ CF

Deterministic context-free languages are a strict subclass of context-free languages over any finite alphabet with at least 3 elements.