Deterministic Context-Free Languages Are Not Closed Under Homomorphism

If deterministic context-free languages were closed under arbitrary string homomorphisms, then erasing the first symbol of a prefix-marked disjoint union would make them closed under union.

@[reducible, inline]

abbrev DCFHomomorphism.DPDA.LeftQuotientState (Q : Type) : Type

Equations

• DCFHomomorphism.DPDA.LeftQuotientState Q = (Bool × Q)

def DCFHomomorphism.DPDA.leftQuotientSingleton {Q A S : Type} [Fintype Q] [Fintype A] [Fintype S] (M : DPDA Q A S) (a : A) : DPDA (LeftQuotientState Q) A S

Equations

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

theorem DCFHomomorphism.DPDA.leftQuotientSingleton_accepts {Q A S : Type} [Fintype Q] [Fintype A] [Fintype S] (M : DPDA Q A S) (a : A) : (leftQuotientSingleton M a).acceptsByFinalState = (fun (x : List A) (L : Language A) => L.leftQuotient x) [a] M.acceptsByFinalState

theorem DCFHomomorphism.DPDA.is_DCF_leftQuotient_singleton {Q A S : Type} [Fintype Q] [Fintype A] [Fintype S] (M : DPDA Q A S) (a : A) : is_DCF ((fun (x : List A) (L : Language A) => L.leftQuotient x) [a] M.acceptsByFinalState)

theorem DCFHomomorphism.DCF_leftQuotient_singleton {A : Type} [Fintype A] {L : Language A} (a : A) (hL : is_DCF L) : is_DCF ((fun (x : List A) (L : Language A) => L.leftQuotient x) [a] L)

theorem DCFHomomorphism.DCF_leftQuotient_word {A : Type} [Fintype A] (x : List A) {L : Language A} (hL : is_DCF L) : is_DCF ((fun (x : List A) (L : Language A) => L.leftQuotient x) x L)

theorem DCFHomomorphism.DCF_notClosedUnderHomomorphism : ¬ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_DCF

theorem DCFHomomorphism.DCF_notClosedUnderEpsFreeHomomorphism : ¬ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_DCF