Deterministic Context-Free Closure Under Inverse Homomorphism

The construction first totalizes the source DPDA. Besides preserving its language, the totalizer keeps a permanent bottom-of-stack marker and records in its finite control whether the current epsilon phase can accept.

For a homomorphism h : α → List β, the inverse-image machine stores one source letter and a position in h a in finite control. Consuming a source letter is deliberately performed before the simulated epsilon phase. This ordering is essential when h a = []: prioritizing source-machine epsilon steps can otherwise starve an erasable source letter forever.

@[reducible, inline]

abbrev InvHomBuffer (α β : Type) (h : α → List β) : Type

A buffered source letter together with the next position of its nonempty image.

Equations

• InvHomBuffer α β h = Option ((a : α) × Fin (h a).length)

def invHomBufferRemaining {α β : Type} (h : α → List β) : InvHomBuffer α β h → List β

The part of a buffered homomorphic image which remains to be simulated.

Equations

• invHomBufferRemaining h none = []
• invHomBufferRemaining h (some ⟨a, k⟩) = List.drop (↑k) (h a)

def invHomWord {α β : Type} (h : α → List β) (w : List α) : List β

Extension of a string homomorphism to words.

Equations

• invHomWord h w = List.flatMap h w

def invHomAdvance {α β : Type} (h : α → List β) (a : α) (k : Fin (h a).length) : InvHomBuffer α β h

Advance past one simulated symbol in a nonempty buffered image.

Equations

• invHomAdvance h a k = if hk : ↑k + 1 < (h a).length then some ⟨a, ⟨↑k + 1, hk⟩⟩ else none

@[simp]

theorem invHomWord_nil {α β : Type} (h : α → List β) : invHomWord h [] = []

@[simp]

theorem invHomWord_cons {α β : Type} (h : α → List β) (a : α) (w : List α) : invHomWord h (a :: w) = h a ++ invHomWord h w

@[simp]

theorem invHomBufferRemaining_none {α β : Type} (h : α → List β) : invHomBufferRemaining h none = []

def DPDA.inverseHomomorphism {α β : Type} [Fintype α] [Fintype β] {Q S : Type} [Fintype Q] [Fintype S] (M : DPDA Q β S) (h : α → List β) : DPDA (Q × InvHomBuffer α β h) α S

DPDA recognizing the inverse image of M under h, provided final-state membership of M is invariant along its empty-input epsilon runs.

In the ready state (buffer = none) the machine has no epsilon transition: it first consumes the next source letter. A nonempty image is then drained through epsilon transitions, with source-machine epsilon steps taking priority while a buffer is present.

Equations

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

theorem DPDA.inverseHomomorphism_correct {α β : Type} [Fintype α] [Fintype β] {Q S : Type} [Fintype Q] [Fintype S] (M : DPDA Q β S) (h : α → List β) (hfinal : ∀ (q q' : Q) (stack stack' : List S), PDA.Reaches { state := q, input := [], stack := stack } { state := q', input := [], stack := stack' } → (q ∈ M.final_states ↔ q' ∈ M.final_states)) (hne : ∀ (w : List β) (c : M.toPDA.conf), PDA.Reaches { state := M.initial_state, input := w, stack := [M.start_symbol] } c → c.stack ≠ []) : (M.inverseHomomorphism h).acceptsByFinalState = M.acceptsByFinalState.inverseHomomorphicImage h

Correctness of the repaired inverse-homomorphism construction under the two normal-form properties supplied by the DPDA totalizer.

theorem DCF_closed_under_inverse_homomorphism {α β : Type} [Fintype α] [Fintype β] (L : Language β) (h : α → List β) (hL : is_DCF L) : is_DCF (L.inverseHomomorphicImage h)

Deterministic context-free languages are closed under inverse string homomorphism.

theorem DCF_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => is_DCF

Predicate-form closure theorem used by the README closure table.