Documentation

MIPRE.Foundations.Pipeline.PowDomRun

Runs within a powered monomial #

PRuns W X K c m e p x r: the program p runs from x to r at a cost below (c (W + 1)^m X^e)^{K + 1} (MIPRE.Pipeline.PDom). The combinators follow the program constructors the pipeline's routines are built from — a polynomial-time function's code (ptf), sequencing (seq), a stage keeping a context (stage), hardcoding (hardcode), the universal machine (univ), and the two unary loops (toUnary, pow) — and each returns its constants from those of its arguments, so that a chain of them has constants uniform in W, X, K and the data.

The explicit running times of the unary loops are toUnaryProg_time and powProg_time: they are polynomial in the values involved.

The unary loops #

source
theorem MIPRE.Pipeline.esize_nat_le_four (x : ℕ) :
Cost.esize x ≤ 4 * x + 1
source
theorem MIPRE.Pipeline.sum_range_le_mul {N B : ℕ} {f : ℕ → ℕ} (h : ∀ i ≤ N, f i ≤ B) :
∑ i ∈ Finset.range (N + 1), f i ≤ (N + 1) * B
source
@[reducible, inline]
noncomputable abbrev MIPRE.Pipeline.toUnaryInit :
Cost.PolyTimeFun Cost.Data Cost.Data

The initialization of toUnaryProg.

Equations
Instances For
    source
    theorem MIPRE.Pipeline.toUnaryProg_time (x : ℕ) :
    ∃ t ≤ Polynomial.eval (4 * x + 1) toUnaryInit.timeBound + (x + 1) * (Polynomial.eval (4 * x + 3) toUnaryStep.timeBound + 1) + 1, toUnaryProg.Runs (Cost.encode x) (Cost.encode (Cost.unary x)) t

    The running time of toUnaryProg, polynomial in the value x.

    source
    @[reducible, inline]
    noncomputable abbrev MIPRE.Pipeline.powInit :
    Cost.PolyTimeFun Cost.Data Cost.Data

    The initialization of powProg.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Pipeline.powProg_time (b : Cost.Unary) (e : ℕ) (hb : 1 ≤ List.length b) :
      ∃ t ≤ Polynomial.eval (2 * List.length b + 4 * e + 3) powInit.timeBound + (e + 1) * (Polynomial.eval (4 * e + 2 * List.length b ^ e + 2 * List.length b + 5) powStep.timeBound + 1) + 1, powProg.Runs (Cost.encode (b, e)) (Cost.encode (Cost.unary (List.length b ^ e))) t

      The running time of powProg, polynomial in e, |b| and |b|^e.

      source
      theorem MIPRE.Pipeline.esize_hardcode (p : Cost.Prog) (d : Cost.Data) :
      Cost.esize (Cost.hardcode p d) = Cost.esize p + d.size + 35

      The size of a hardcoded program.

      Sizes #

      source
      theorem MIPRE.Pipeline.PDom.consSize (c m e c' m' e' : ℕ) :
      ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (x r : Cost.Data), 1 ≤ X → PDom W X K c m e x.size → PDom W X K c' m' e' r.size → PDom W X K C M E (x.cons r).size

      A pair of dominated data is dominated.

      source
      theorem MIPRE.Pipeline.PDom.indexInput :
      ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X K : ℕ} (n : ℕ) (d : Cost.Data), 1 ≤ X → n ≤ W → d.size + 1 ≤ X → PDom W X K c m e ((Cost.encode n).cons d).size

      An index and a datum of size below X.

      Runs within a powered monomial #

      source
      def MIPRE.Pipeline.PRuns (W X K c m e : ℕ) (p : Cost.Prog) (x r : Cost.Data) :
      Prop

      p runs from x to r at a cost below (c (W + 1)^m X^e)^{K + 1}.

      Equations
      Instances For
        source
        theorem MIPRE.Pipeline.PRuns.size_le {W X K c m e : ℕ} {p : Cost.Prog} {x r : Cost.Data} (h : PRuns W X K c m e p x r) :
        PDom W X K c m e r.size
        source
        theorem MIPRE.Pipeline.PRuns.mono {W X K : ℕ} (hX : 1 ≤ X) {c m e c' m' e' : ℕ} {p : Cost.Prog} {x r : Cost.Data} (h : PRuns W X K c m e p x r) (hc : c ≤ c') (hm : m ≤ m') (he : e ≤ e') :
        PRuns W X K c' m' e' p x r
        source
        theorem MIPRE.Pipeline.PRuns.seq {W X K : ℕ} (hX : 1 ≤ X) {c₁ m₁ e₁ c₂ m₂ e₂ : ℕ} {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x y r : Cost.Data} (h₁ : PRuns W X K c₁ m₁ e₁ p x y) (h₂ : PRuns W X K c₂ m₂ e₂ q y r) :
        PRuns W X K (c₁ + c₂ + 2) (max (max m₁ m₂) 0) (max (max e₁ e₂) 0) (Cost.seqProg p q) x r
        source
        theorem MIPRE.Pipeline.PRuns.ptf {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (f : Cost.PolyTimeFun α β) (c m e : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (a : α), 1 ≤ X → PDom W X K c m e (Cost.esize a) → PRuns W X K C M E f.code (Cost.encode a) (Cost.encode (f.toFun a))

        A polynomial-time function's code, on an input of dominated size.

        source
        theorem MIPRE.Pipeline.PRuns.ptf_size {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (f : Cost.PolyTimeFun α β) (c m e : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (a : α), 1 ≤ X → PDom W X K c m e (Cost.esize a) → PDom W X K C M E (Cost.esize (f.toFun a))

        A polynomial-time function's value, of dominated size.

        source
        theorem MIPRE.Pipeline.PRuns.stage (pre : Cost.PolyTimeFun Cost.Data Cost.Data) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (c m e c' m' e' : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} {p : Cost.Prog}, Cost.Prog.WellScoped 1 p → ∀ (x a ctx r : Cost.Data), 1 ≤ X → pre.toFun x = a.cons ctx → PDom W X K c m e x.size → PRuns W X K c' m' e' p a r → PRuns W X K C M E (stageProg pre p post) x (post.toFun (ctx, r))

        A stage keeping a context: stageProg pre p post on x, with pre x = (a, ctx).

        source
        theorem MIPRE.Pipeline.PRuns.hardcode {W X K : ℕ} (hX : 1 ≤ X) {c m e c₁ m₁ e₁ c₂ m₂ e₂ : ℕ} {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) {d x r : Cost.Data} (h : PRuns W X K c m e p (d.cons x) r) (hd : PDom W X K c₁ m₁ e₁ d.size) (hx : PDom W X K c₂ m₂ e₂ x.size) :
        PRuns W X K (c + c₁ + c₂ + 4) (max (max (max m m₁) m₂) 0) (max (max (max e e₁) e₂) 0) (Cost.hardcode p d) x r

        Hardcoding a datum d.

        source
        theorem MIPRE.Pipeline.PRuns.univ (c m e : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (q : Cost.Prog) (v r : Cost.Data) (t : ℕ), 1 ≤ X → q.Runs v r t → PDom W X K c m e (Cost.esize q + v.size + t) → PRuns W X K C M E Cost.selfUniversal.univ ((Cost.encode q).cons v) r

        The universal machine, simulating a run of dominated cost.

        source
        theorem MIPRE.Pipeline.PRuns.toUnary (c m e : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (x : ℕ), 1 ≤ X → PDom W X K c m e x → PRuns W X K C M E toUnaryProg (Cost.encode x) (Cost.encode (Cost.unary x))

        Writing a dominated number in unary.

        source
        theorem MIPRE.Pipeline.PRuns.pow (c m e : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (b : Cost.Unary) (k : ℕ), 1 ≤ X → 1 ≤ List.length b → PDom W X K c m e (List.length b) → PDom W X K c m e k → PDom W X K c m e (List.length b ^ k) → PRuns W X K C M E powProg (Cost.encode (b, k)) (Cost.encode (Cost.unary (List.length b ^ k)))

        A unary power |b|^e, all three of |b|, e and |b|^e dominated.

        source
        theorem MIPRE.Pipeline.PRuns.routeCall (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (c m e c' m' e' : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} {p : Cost.Prog}, Cost.Prog.WellScoped 1 p → ∀ (x a ctx r : Cost.Data), 1 ≤ X → route.toFun x = (true, a.cons ctx) → PDom W X K c m e x.size → PRuns W X K c' m' e' p a r → PRuns W X K C M E (Cost.Prog.routeOneCall route p post) x (post.toFun (ctx, r))

        A routed call: routeOneCall route p post on x, when the router calls p on a with the context ctx.

        source
        theorem MIPRE.Pipeline.PRuns.routeDirect (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (c m e : ℕ) :
        ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (p : Cost.Prog) (x r : Cost.Data), 1 ≤ X → route.toFun x = (false, r) → PDom W X K c m e x.size → PRuns W X K C M E (Cost.Prog.routeOneCall route p post) x r

        A direct answer of a router.