Efficient Kleene recursion

The efficient fixed-point theorem efficient_fixed_point (blueprint lem:kleene; [MNY, Lemma 2.3]), by the classical construction: for a polynomial-time map F on programs, let G be the program that on cons x v (with x the description of a program x') computes s(x', x') = hardcode x' (encode x'), applies F to it, and runs the result on v through the universal machine; the fixed point is e = hardcode G (encode G), since e on v is G on cons (encode G) v, which runs F (hardcode G (encode G)) = F e on v. The time transfer is the universal machine's, plus the fixed cost of computing F e and a copy of the input.

theorem MIPRE.Cost.Prog.callVar_runs_rev {env : Env} {i : ℕ} {q : Prog} (hq : WellScoped 1 q) {r : Data} {t : ℕ} (h : Eval env (callVar i q) r t) : ∃ t' ≤ t, q.Runs (env.get i) r t'

Inverting a call: a run of callVar i q is a run of the closed q on the value of variable i.

def MIPRE.Cost.Prog.kleeneProg (univ : Prog) (F : PolyTimeFun Prog Prog) : Prog

The two-argument program of the fixed-point construction: on cons x v, compute the description of hardcode x' (encode x') (where x = encode x'), apply F to it, and run the result on v through the universal program univ.

Equations

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

theorem MIPRE.Cost.Prog.kleeneProg_wellScoped {univ : Prog} (hU : WellScoped 1 univ) (F : PolyTimeFun Prog Prog) : WellScoped 1 (univ.kleeneProg F)

theorem MIPRE.Cost.Prog.kleeneProg_pair_eval (x : Prog) (v : Data) : Eval [encode x, v, (encode x).cons v] ((var 0).cons (var 0)) ((encode x).cons (encode x)) ((encode x).size + 1 + ((encode x).size + 1) + 1)

The run of the pairing prefix of kleeneProg.

theorem MIPRE.Cost.Prog.kleeneProg_smn_eval (x : Prog) (v : Data) : Eval [(encode x).cons (encode x), encode x, v, (encode x).cons v] (callVar 0 smnProg) (encode (hardcode x (encode x))) (((encode x).cons (encode x)).size + 1 + ((encode x).size + (encode x).size + 38) + 1)

The run of the s-m-n step of kleeneProg.

theorem MIPRE.Cost.Prog.kleeneProg_pair2_eval (x : Prog) (v : Data) (F : PolyTimeFun Prog Prog) : Eval [encode (F.toFun (hardcode x (encode x))), encode (hardcode x (encode x)), (encode x).cons (encode x), encode x, v, (encode x).cons v] ((var 0).cons (var 4)) ((encode (F.toFun (hardcode x (encode x)))).cons v) ((encode (F.toFun (hardcode x (encode x)))).size + 1 + (v.size + 1) + 1)

The run of the final pairing step of kleeneProg.

theorem MIPRE.Cost.Prog.kleeneProg_runs (U : UniversalMachine) (F : PolyTimeFun Prog Prog) (x : Prog) {v r : Data} {t : ℕ} (h : (F.toFun (hardcode x (encode x))).Runs v r t) : ∃ T ≤ 6 * esize x + esize (hardcode x (encode x)) + Polynomial.eval (esize (hardcode x (encode x))) F.timeBound + 2 * esize (F.toFun (hardcode x (encode x))) + 2 * v.size + Polynomial.eval (esize (F.toFun (hardcode x (encode x))) + v.size + t) U.bound + 57, (U.univ.kleeneProg F).Runs ((encode x).cons v) r T

Forward run of kleeneProg: a run of F (hardcode x (encode x)) on v yields a run of kleeneProg on cons (encode x) v, at the universal machine's overhead plus the fixed cost of computing F (hardcode x (encode x)) and copies of the input.

theorem MIPRE.Cost.Prog.kleeneProg_halts_of (U : UniversalMachine) (F : PolyTimeFun Prog Prog) (x : Prog) {v r : Data} {T : ℕ} (h : (U.univ.kleeneProg F).Runs ((encode x).cons v) r T) : ∃ (t : ℕ), (F.toFun (hardcode x (encode x))).Runs v r t

Backward: a run of kleeneProg on cons (encode x) v yields a run of F (hardcode x (encode x)) on v (through UniversalMachine.halts_of).

The fixed point, as data

The construction is exposed (kleeneFix) with its overhead spelled out (kleeneFix_runs_of), because the polynomial-time halting reduction (planning/polytime-halting.md) needs the overhead of the fixed point of a family F_M of maps to be bounded uniformly in M: the existential polynomial of efficient_fixed_point below depends on F, and only the explicit form shows how.

def MIPRE.Cost.kleeneFix (U : UniversalMachine) (F : PolyTimeFun Prog Prog) : Prog

The fixed point of F through the universal machine U: hardcode G (encode G) for the program G = kleeneProg U.univ F.

Equations

• MIPRE.Cost.kleeneFix U F = MIPRE.Cost.hardcode (U.univ.kleeneProg F) (MIPRE.Cost.encode (U.univ.kleeneProg F))

theorem MIPRE.Cost.kleeneFix_wellScoped (U : UniversalMachine) (F : PolyTimeFun Prog Prog) : Prog.WellScoped 1 (kleeneFix U F)

theorem MIPRE.Cost.kleeneFix_halts_iff (U : UniversalMachine) (F : PolyTimeFun Prog Prog) (v r : Data) : (∃ (t : ℕ), (kleeneFix U F).Runs v r t) ↔ ∃ (t : ℕ), (F.toFun (kleeneFix U F)).Runs v r t

The fixed point has the input/output behavior of F applied to it.

def MIPRE.Cost.kleeneOverhead (U : UniversalMachine) (F : PolyTimeFun Prog Prog) : ℕ

The fixed part of the overhead of the fixed point: the copies of the program, the computation of F (kleeneFix U F), and constants.

Equations

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

theorem MIPRE.Cost.kleeneFix_runs_of (U : UniversalMachine) (F : PolyTimeFun Prog Prog) {v r : Data} {t : ℕ} (h : (F.toFun (kleeneFix U F)).Runs v r t) : ∃ t' ≤ Polynomial.eval (v.size + t + esize (F.toFun (kleeneFix U F))) U.bound + 3 * v.size + kleeneOverhead U F, (kleeneFix U F).Runs v r t'

The time transfer of the fixed point, explicitly: a run of F (kleeneFix U F) on v in time t yields a run of kleeneFix U F within the universal machine's overhead at v.size + t + esize (F (kleeneFix U F)), plus 3 · v.size, plus the fixed overhead.

The fixed-point theorem (blueprint lem:kleene; [MNY, Lemma 2.3])

theorem MIPRE.Cost.efficient_fixed_point (F : PolyTimeFun Prog Prog) : ∃ (e : Prog) (p : Polynomial ℕ), Prog.WellScoped 1 e ∧ (∀ (v r : Data), (∃ (t : ℕ), e.Runs v r t) ↔ ∃ (t : ℕ), (F.toFun e).Runs v r t) ∧ ∀ (v r : Data) (t : ℕ), (F.toFun e).Runs v r t → ∃ t' ≤ Polynomial.eval (v.size + t) p, e.Runs v r t'

Efficient Kleene fixed point: for a polynomial-time map on programs, a closed program e with the same input/output behavior as F e, whose runs are bounded by the runs of F e at polynomial overhead. The construction is kleeneFix U F, and the polynomial p is the universal machine's bound shifted by the size of F e, plus a linear term and a constant covering the fixed computation of F e and the copies of the input (kleeneFix_runs_of).

Departure from [MNY, Lemma 2.3], which states the runtimes of e and F e as polynomially equivalent: only the direction "runs of F e bound runs of e" is used by the recursive compression argument (it is what makes the fixed point polynomial-time), and only that direction follows from UniversalMachine.time_le. The converse would need a lower-bound clause on the universal machine ("a simulation is never faster than the simulated run"); it is omitted to keep the universal-machine obligation minimal and can be restored with such a clause if a consumer needs it.