Langlib

Langlib.Classes.DeterministicContextFree.Closure.Homomorphism

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.

source
@[reducible, inline]
abbrev DCFHomomorphism.DPDA.LeftQuotientState (Q : Type) :
Type
Equations
Instances For
    source
    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.
    Instances For
      source
      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
      source
      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)
      source
      def DCFHomomorphism.markedChoice {T : Type} (L₁ L₂ : Language T) :
      Language (Bool ⊕ T)

      A disjoint, prefix-marked choice between two languages. The leading Boolean selects the source language and every payload symbol is injected with Sum.inr.

      Unlike ordinary union, this operation is deterministic: a DPDA chooses the source machine from the first input symbol.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem DCFHomomorphism.DCF_markedChoice {T : Type} [Fintype T] {L₁ L₂ : Language T} (hL₁ : is_DCF L₁) (hL₂ : is_DCF L₂) :
        is_DCF (markedChoice L₁ L₂)

        Prefix-marked choice preserves deterministic context-freeness.

        source
        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)
        source
        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)
        source
        theorem DCFHomomorphism.DCF_notClosedUnderHomomorphism :
        ¬ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_DCF
        source
        theorem DCFHomomorphism.DCF_notClosedUnderEpsFreeHomomorphism :
        ¬ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_DCF