Initialized iteration with a preserved input

initializedStep init step keeps its state in the first component of pair and its unchanged input in the second. An empty state is the initialization sentinel: the first call on pair [] x installs init x, and later calls apply step x while the state is nonempty. The step may depend on the original input.

initializedStep_iterate identifies the packed orbit with the ordinary orbit of step x, with one extra call for initialization. Its nonemptiness hypothesis covers exactly the states on which a step is taken; the final state may be empty. Without that hypothesis an empty intermediate state would initialize again.

The controller uses the total projections pairFst and pairSnd on arbitrary strings; no validity of malformed pair encodings is assumed. Its polynomial-time closure theorem and orbit equation are shared by Savitch's and IP's space-bounded iterations, independently of their state encodings and invariants.

def Complexity.initializedStep (init : List Bool → List Bool) (step : List Bool → List Bool → List Bool) (z : List Bool) : List Bool

Initialize an empty state, or take one step, preserving the input on the right.

Equations

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

theorem Complexity.initializedStep_pair (init : List Bool → List Bool) (step : List Bool → List Bool → List Bool) (s x : List Bool) : initializedStep init step (pair s x) = pair (Cobham.selectHead (emptyFlag s) (init x) (step x s)) x

The controller's action on an encoded state and input.

theorem Complexity.initializedStep_nil (init : List Bool → List Bool) (step : List Bool → List Bool → List Bool) (x : List Bool) : initializedStep init step (pair [] x) = pair (init x) x

The empty sentinel installs the initial state.

theorem Complexity.initializedStep_step (init : List Bool → List Bool) (step : List Bool → List Bool → List Bool) (s x : List Bool) (hs : s ≠ []) : initializedStep init step (pair s x) = pair (step x s) x

A nonempty state takes one step instead of initializing again.

theorem Complexity.initializedStep_iterate (init : List Bool → List Bool) (step : List Bool → List Bool → List Bool) (x : List Bool) (n : ℕ) : (∀ j < n, (step x)^[j] (init x) ≠ []) → (initializedStep init step)^[n + 1] (pair [] x) = pair ((step x)^[n] (init x)) x

Packing an orbit costs one initialization call. Only states on which another step is taken must be nonempty, so the state after the last step may be empty.

theorem Complexity.initializedStep_mem_FP {init : List Bool → List Bool} {step : List Bool → List Bool → List Bool} (hinit : init ∈ FP) (hstep : (fun (z : List Bool) => step (pairSnd z) (pairFst z)) ∈ FP) : initializedStep init step ∈ FP

A polynomial-time initializer and step give a polynomial-time packed controller. The step receives the unchanged input and current state through the pair projections.