A regular-domain guard for binary CSLib machines

The guard scans the read-only input with a DFA. Rejection halts with empty output. Acceptance rewinds the input and starts the original machine with untouched work tapes and output.

inductive Complexity.CslibGuard.State (σ Q : Type) : Type

Validation, rewind, and source execution control.

• scan {σ Q : Type} : σ → State σ Q

  Scan using the current DFA state.

• rewind {σ Q : Type} : State σ Q

  Return to the left input boundary.

• run {σ Q : Type} : Q → State σ Q

  Execute the source machine.

@[instance_reducible]

instance Complexity.CslibGuard.instFintypeState {σ✝ Q✝ : Type} [Fintype σ✝] [Fintype Q✝] : Fintype (State σ✝ Q✝)

Equations

• Complexity.CslibGuard.instFintypeState = Fintype.ofEquiv (σ✝ ⊕ Unit ⊕ Q✝) (Complexity.CslibGuard.State.proxyTypeEquiv σ✝ Q✝)

def Complexity.CslibGuard.idle {k : ℕ} {σ Q : Type} (q : Option (State σ Q)) (move : SignType) : Turing.Action k Bool (State σ Q)

Change control and input position without changing work tapes or output.

Equations

• Complexity.CslibGuard.idle q move = { inputTape := move, workTapes := fun (x : Fin k) => (none, 0), output := none, state := q }

noncomputable def Complexity.CslibGuard.machine {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) : Turing.MultiTapeTM k Bool (State σ Q)

Validate a regular input format before executing a binary CSLib machine.

Equations

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