Binary-counted folds in polynomial space

Nat.fold visits the indices below a binary count in increasing order. The step receives the original input, current index and accumulator. Its native computation may use arbitrary time in polynomial space. A polynomial bound on all encoded accumulator prefixes suffices for the fold; the count itself need not be polynomially bounded.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolySpace.natFold: a fold with bounded accumulators.
• Turing.MultiTapeTM.ComputableTidilyInPolySpace.natFold_spec: a prefix invariant gives both the space certificate and the final postcondition.

References

Adapted from the lean-canny contributors' Computation/TidyBoundedFold.lean at 2a50a2ee. The port uses the standard Nat.fold and the existing tidy space calculus, with no separate machine or computability predicate.

theorem Turing.MultiTapeTM.ComputableTidilyInPolySpace.natFold {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} [Inhabited α] [Inhabited β] {step : α → ℕ → β → β} {init : α → β} {count bound : α → ℕ} (hcount : ComputableTidilyInPolyTime count encIn encNat) (hinit : ComputableTidilyInPolySpace init encIn encState) (hstep : ComputableTidilyInPolySpace (fun (p : α × ℕ × β) => step p.1 p.2.1 p.2.2) (encPair encIn (encPair encNat encState)) encState) (hbound : PolyBounded (fun (x : α) => (encIn x).length) bound) (hstates : ∀ (x : α), ∀ k ≤ count x, (encState (k.fold (fun (i : ℕ) (x_1 : i < k) (a : β) => step x i a) (init x))).length ≤ bound x) : ComputableTidilyInPolySpace (fun (x : α) => (count x).fold (fun (i : ℕ) (x_1 : i < count x) (a : β) => step x i a) (init x)) encIn encState

A fold over a binary count is polynomial-space when its step and seed are polynomial-space and every accumulator prefix has polynomially bounded encoded length.

theorem Turing.MultiTapeTM.ComputableTidilyInPolySpace.natFold_spec {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} [Inhabited α] [Inhabited β] {step : α → ℕ → β → β} {init : α → β} {count bound : α → ℕ} (hcount : ComputableTidilyInPolyTime count encIn encNat) (hinit : ComputableTidilyInPolySpace init encIn encState) (hstep : ComputableTidilyInPolySpace (fun (p : α × ℕ × β) => step p.1 p.2.1 p.2.2) (encPair encIn (encPair encNat encState)) encState) (invariant : α → ℕ → β → Prop) (hzero : ∀ (x : α), invariant x 0 (init x)) (hnext : ∀ (x : α) (k : ℕ) (a : β), k < count x → invariant x k a → invariant x (k + 1) (step x k a)) (hbound : PolyBounded (fun (x : α) => (encIn x).length) bound) (hsize : ∀ (x : α) (k : ℕ) (a : β), k ≤ count x → invariant x k a → (encState a).length ≤ bound x) : ComputableTidilyInPolySpace (fun (x : α) => (count x).fold (fun (i : ℕ) (x_1 : i < count x) (a : β) => step x i a) (init x)) encIn encState ∧ ∀ (x : α), invariant x (count x) ((count x).fold (fun (i : ℕ) (x_1 : i < count x) (a : β) => step x i a) (init x))

A prefix invariant proves the fold's polynomial-space certificate and its final postcondition. The invariant and bound are proof data; only the count, seed and step run.