DCF Closure Under Injective Terminal Maps

def DPDA.comapInput {T₁ T₂ Q S : Type} [Fintype Q] [Fintype T₁] [Fintype T₂] [Fintype S] (M : DPDA Q T₂ S) (f : T₁ → T₂) : DPDA Q T₁ S

Pull input symbols back along an alphabet map.

Equations

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

theorem DPDA.comap_acceptsByFinalState {T₁ T₂ Q S : Type} [Fintype Q] [Fintype T₁] [Fintype T₂] [Fintype S] (M : DPDA Q T₂ S) (f : T₁ → T₂) : (M.comapInput f).acceptsByFinalState = {w : List T₁ | List.map f w ∈ M.acceptsByFinalState}

noncomputable def DPDA.mapInput {T₁ T₂ Q S : Type} [Fintype Q] [Fintype T₁] [Fintype T₂] [Fintype S] (M : DPDA Q T₁ S) (f : T₁ → T₂) (g : T₂ → T₁) : DPDA Q T₂ S

Rename the input alphabet of a DPDA along f, decoding symbols in the image using g. Symbols outside the image of f have no transition.

Equations

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

theorem DPDA.map_acceptsByFinalState_of_injective {T₁ T₂ Q S : Type} [Fintype Q] [Fintype T₁] [Fintype T₂] [Fintype S] [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (M : DPDA Q T₁ S) : (M.mapInput f (Function.invFun f)).acceptsByFinalState = (Language.map f) M.acceptsByFinalState

Injective terminal renaming preserves final-state acceptance of DPDAs.

theorem DCF_of_map_injective_DCF {T₁ T₂ : Type} [Nonempty T₁] [Fintype T₁] [Fintype T₂] {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) : is_DCF L → is_DCF ((Language.map f) L)

Deterministic context-free languages are preserved under injective terminal maps.

theorem DCF_of_map_injective_DCF_rev {T₁ T₂ : Type} [Fintype T₁] [Fintype T₂] {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) : is_DCF ((Language.map f) L) → is_DCF L