def DPDA.complement {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : DPDA Q T S

Construct the complement DPDA by replacing the set of accepting states with its complement. This is a syntactic operation that swaps which states are accepting.

Equations

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

@[simp]

theorem DPDA.complement_final_states {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.final_states = M.final_statesᶜ

@[simp]

theorem DPDA.complement_transition {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.transition = M.transition

@[simp]

theorem DPDA.complement_epsilon_transition {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.epsilon_transition = M.epsilon_transition

@[simp]

theorem DPDA.complement_initial_state {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.initial_state = M.initial_state

@[simp]

theorem DPDA.complement_start_symbol {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.start_symbol = M.start_symbol

@[simp]

theorem DPDA.complement_complement {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.complement.initial_state = M.initial_state ∧ M.complement.complement.start_symbol = M.start_symbol ∧ M.complement.complement.final_states = M.final_states ∧ M.complement.complement.transition = M.transition ∧ M.complement.complement.epsilon_transition = M.epsilon_transition

@[simp]

theorem DPDA.complement_toPDA {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.toPDA.initial_state = M.toPDA.initial_state

theorem DPDA.complement_toPDA_transition_fun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.toPDA.transition_fun = M.toPDA.transition_fun

The complement DPDA has the same transition functions as the original.

theorem DPDA.complement_toPDA_transition_fun' {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : M.complement.toPDA.transition_fun' = M.toPDA.transition_fun'

The complement DPDA has the same ε-transition functions as the original.

theorem DPDA.complement_toPDA_reaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q q' : Q) (w : List T) (γ γ' : List S) : PDA.Reaches { state := q, input := w, stack := γ } { state := q', input := [], stack := γ' } ↔ PDA.Reaches { state := q, input := w, stack := γ } { state := q', input := [], stack := γ' }

The multi-step reachability relation is the same for a DPDA and its complement, because the step function depends only on the transitions, not the accepting states.

theorem DPDA.complement_isTotal {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (h : M.IsTotal) : M.complement.IsTotal

Complementing a total DPDA yields a total DPDA: flipping the accepting states changes neither the transitions (so totality is preserved) nor whether two empty-input configurations agree (so acceptance consistency is preserved).

theorem DPDA.complement_acceptsByFinalState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (h : M.IsTotal) : M.complement.acceptsByFinalState = M.acceptsByFinalStateᶜ

For a total DPDA, the complemented DPDA accepts precisely the complement of the original language.

theorem is_DCF_total_complement {T : Type} [Fintype T] {L : Language T} (hL : is_DCF_total L) : is_DCF_total Lᶜ

Complement closure for total presentations. If L is recognized by a total DPDA, so is Lᶜ: complement the total DPDA.

theorem is_DCF_complement {T : Type} [Fintype T] {L : Language T} (hL : is_DCF L) : is_DCF Lᶜ

Complement closure for deterministic context-free languages. Every DCF L has Lᶜ deterministic context-free as well. An arbitrary final-state DPDA for L need not decide every input, so the proof first totalizes it (DPDA.exists_equivalent_total) into an equivalent total DPDA and then complements that — no DPDA.IsTotal hypothesis on the input is required.

theorem is_DCF_closedUnderComplement {T : Type} [Fintype T] : ClosedUnderComplement is_DCF

Deterministic context-free languages are closed under complement.