Determinizing certified row relations

A CertifiedRowSystem presents its row relation by a finite-state verifier that may guess one certificate symbol per cell. This file applies the ordinary subset construction to that verifier. The resulting system has Unit certificates: after reading an aligned pair of rows, its verifier state is exactly the finite set of source-verifier states obtainable from all certificate prefixes.

This is useful when both an edge and the absence of an edge must be checked in linear space. In particular, the inductive-counting proof of context-sensitive complement closure uses the determinized verifier in its negative branch.

noncomputable def CertifiedRowSystem.detStepCell {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] (S : CertifiedRowSystem I A C Q F) (states : Finset Q) (old new : A) : Finset Q

One subset-construction transition for a certified row verifier.

Equations

• S.detStepCell states old new = states.biUnion fun (q : Q) => Finset.image (fun (cert : C) => S.stepCell q old new cert) Finset.univ

@[simp]

theorem CertifiedRowSystem.mem_detStepCell {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) (states : Finset Q) (old new : A) (q' : Q) : q' ∈ S.detStepCell states old new ↔ ∃ q ∈ states, ∃ (cert : C), S.stepCell q old new cert = q'

noncomputable def CertifiedRowSystem.evalDetStep {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] (S : CertifiedRowSystem I A C Q F) : Finset Q → List A → List A → Option (Finset Q)

Run the determinized verifier on two aligned rows.

Equations

• S.evalDetStep x✝ [] [] = some x✝
• S.evalDetStep x✝ (old :: olds) (new :: news) = S.evalDetStep (S.detStepCell x✝ old new) olds news
• S.evalDetStep x✝² x✝¹ x✝ = none

theorem CertifiedRowSystem.mem_evalDetStep_iff {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) (states : Finset Q) (old new : List A) (out : Finset Q) (q' : Q) : S.evalDetStep states old new = some out → (q' ∈ out ↔ ∃ q ∈ states, ∃ (cert : List C), S.evalStep q old new cert = some q')

The determinized state set contains q' exactly when some certificate row takes some initial verifier state in states to q'.

noncomputable def CertifiedRowSystem.determinize {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) : CertifiedRowSystem I A Unit (Finset Q) F

The subset construction turns a certified system into an equivalent system whose certificate alphabet is Unit.

Equations

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

theorem CertifiedRowSystem.evalStep_determinize {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) (states : Finset Q) (old new : List A) (cert : List Unit) : cert.length = old.length → old.length = new.length → S.determinize.evalStep states old new cert = S.evalDetStep states old new

theorem CertifiedRowSystem.evalDetStep_eq_some_of_length {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) (states : Finset Q) (old new : List A) (hlen : old.length = new.length) : ∃ (out : Finset Q), S.evalDetStep states old new = some out

theorem CertifiedRowSystem.rowStep_determinize_iff {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) (old new : List A) : S.determinize.RowStep old new ↔ S.RowStep old new

Determinization preserves the certified row relation exactly.

theorem CertifiedRowSystem.rowReachLanguage_determinize {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype C] [DecidableEq Q] (S : CertifiedRowSystem I A C Q F) : S.determinize.rowReachLanguage = S.rowReachLanguage

Determinization preserves the reachability language.