Iterating a polynomial-time step, and running programs in sequence

Two program combinators for routines whose running time is not polynomial in the size of their input, such as the computation of (λn + 1)^μ from binary λ, n, μ:

• whileProg f iterates a total step f : Data → Bool × Data from a state, continuing on (true, s') with the state s' and stopping on (false, r) with the result r; a run of N + 1 steps costs the sum of the steps' bounds (whileProg_runs);
• seqProg p q runs q on the output of p (seqProg_runs).

def MIPRE.Cost.whileProg (f : PolyTimeFun Data (Bool × Data)) : Prog

Iterate the step f until it stops.

Equations

• MIPRE.Cost.whileProg f = f.code.loop

theorem MIPRE.Cost.whileProg_closed (f : PolyTimeFun Data (Bool × Data)) : Prog.WellScoped 1 (whileProg f)

theorem MIPRE.Cost.whileProg_runs (f : PolyTimeFun Data (Bool × Data)) (N : ℕ) (s : ℕ → Data) (r : Data) (hcont : ∀ i < N, f.toFun (s i) = (true, s (i + 1))) (hstop : f.toFun (s N) = (false, r)) : ∃ t ≤ ∑ i ∈ Finset.range (N + 1), (Polynomial.eval (s i).size f.timeBound + 1), (whileProg f).Runs (s 0) r t

A run of the loop through the states s 0, …, s N, stopping at s N with r.

def MIPRE.Cost.seqProg (p q : Prog) : Prog

Run q on the output of p.

Equations

• MIPRE.Cost.seqProg p q = p.let_ q

theorem MIPRE.Cost.seqProg_closed {p q : Prog} (hp : Prog.WellScoped 1 p) (hq : Prog.WellScoped 1 q) : Prog.WellScoped 1 (seqProg p q)

theorem MIPRE.Cost.seqProg_runs {p q : Prog} (hq : Prog.WellScoped 1 q) {x y r : Data} {s t : ℕ} (hp : p.Runs x y s) (hq' : q.Runs y r t) : (seqProg p q).Runs x r (s + t + 1)