Certified row systems and linearly bounded automata #

A CertifiedRowSystem describes a length-preserving relation on finite rows. A successor row is certified one cell at a time by a finite left-to-right verifier. This file compiles every such system to a nondeterministic LBA. The machine keeps two row tracks on the input-sized tape. It guesses and verifies the inactive track in one sweep, and changes the active track only after the whole certificate has been accepted.

The construction is useful for space-bound arguments whose configurations have already been packed into a fixed number of logical slots per input cell: the packed cell is the row alphabet A, while C contains the finite local annotation witnessing one simulated step.

source

structure CertifiedRowSystem (I : Type u_1) (A : Type u_2) (C : Type u_3) (Q : Type u_4) (F : Type u_5) :

Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

A finite-state, cellwise-certified, length-preserving row transition system.

stepCell q old new cert is the verifier state after checking one aligned pair of cells. A row step is valid when some certificate row makes the final verifier state satisfy stepDone. finalCell and finalDone similarly specify the regular set of target rows.

inputCell : I → A
stepStart : Q
stepCell : Q → A → A → C → Q
stepDone : Q → Bool
finalStart : F
finalCell : F → A → F
finalDone : F → Bool

Instances For

source

def CertifiedRowSystem.evalStep {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) :

Q → List A → List A → List C → Option Q

Run the step verifier on three aligned lists. A length mismatch rejects with none.

Equations

S.evalStep x✝ [] [] [] = some x✝
S.evalStep x✝ (a :: as) (b :: bs) (c :: cs) = S.evalStep (S.stepCell x✝ a b c) as bs cs
S.evalStep x✝³ x✝² x✝¹ x✝ = none

Instances For

source

def CertifiedRowSystem.RowStep {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) (old new : List A) :

Prop

The length-preserving row relation certified by evalStep.

Equations

S.RowStep old new = ∃ (cert : List C) (q : Q), S.evalStep S.stepStart old new cert = some q ∧ S.stepDone q = true

Instances For

source

def CertifiedRowSystem.evalFinal {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) (q : F) (row : List A) :

Run the finite-state target-row checker.

Equations

S.evalFinal q row = List.foldl S.finalCell q row

Instances For

source

def CertifiedRowSystem.Final {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) (row : List A) :

Prop

The regular target predicate for rows.

Equations

S.Final row = (S.finalDone (S.evalFinal S.finalStart row) = true)

Instances For

source

def CertifiedRowSystem.rowReachLanguage {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) :

Language I

The nonempty input language obtained by row reachability from the cellwise input encoding.

Equations

S.rowReachLanguage w = (w ≠ [] ∧ ∃ (row : List A), Relation.ReflTransGen S.RowStep (List.map S.inputCell w) row ∧ S.Final row)

Instances For

source

@[simp]

theorem CertifiedRowSystem.evalStep_nil_iff {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) {q q' : Q} {as bs : List A} {cs : List C} :