Documentation

MIPRE.Foundations.Cost.Basic

The ambient cost model #

This file fixes the cost model in which every polynomial-time statement of the project is made: the transformations of the compression pipeline (introspection, oracularization, answer reduction, parallel repetition), the Compress map, the efficient computability toolkit (universal machine, s-m-n, Kleene fixed point; blueprint Section sec:rr-computability), and the recursive compression lemma (blueprint lem:recursive-compression, [MNY] Lemma 5.1).

The model #

Data are binary trees (Data: nil and cons), the S-expressions in which bit strings, numbers, pairs and programs are all encoded (Cost.Encoding). Data.size counts nodes; it is the bit-length of the preorder serialization Data.toBits, so sizes are additive under pairing (R4 below).

Programs (Prog) form a minimal first-order language with de Bruijn variables over an environment of Data values: var i reads a variable, nil, const d and cons h t build values, elim i n c inspects the i-th variable (binding the two components of a cons), let_ e b binds, and loop b iterates b on the state held in variable 0 until it signals stop. The timed big-step semantics Eval env p r t charges one unit per rule, except that reading a variable or a literal costs the size of the value: values are copied when read and inspected in place by elim. Consequently a run of cost t produces a result of size at most t (Eval.size_le), so every value occurring in a computation is polynomially bounded by the running time โ€” which is what makes the unit costs honest under a pointer-machine, and then Turing-machine, simulation with polynomial overhead (meta-remark below).

Why this model (decision record) #

The choice is driven by the requirements extracted from the JNVWY pipeline:

Three natural alternatives fail:

Prog sits in the sweet spot: cons builds and elim destructs anywhere in a value, so string algorithms and recursion on notation are direct (R1); programs are trees, hence data with additive sizes (Prog.toData in Cost.Encoding), and hardcoding an argument is let_ (cons (const d) (var 0)) at linear cost (R2, R4); and the language is small enough for its metatheory and for a self-interpreter โ€” the universal machine of Cost.Toolkit โ€” to be manageable, and to be compiled to the machine model for R3. The design follows the "rose tree machine" idea of C. Reitwiessner (CSLib issue #611) with binary trees in place of rose trees and a time-only semantics.

Meta-remark (not formalized). A pointer machine represents values as DAGs of cons cells: cons, elim and let_ are constant-time, var i and const d copy a value in time proportional to its size (exactly the charged cost), so a run of cost t takes O(t) pointer-machine time on O(t + input) cells, and Turing-machine time polynomial in that. This justifies reading PolyTimeFun as honest "polynomial time"; nothing in the project depends on it formally, since the final theorem only claims Computable.

Main definitions #

Blueprint: this file is part of sec:rr-computability (efficient computability toolkit), infrastructure level.

source
inductive MIPRE.Cost.Data :
Type

Binary trees: the data of the ambient model.

Instances For
    source
    def MIPRE.Cost.instDecidableEqData.decEq (xโœ xโœยน : Data) :
    Decidable (xโœ = xโœยน)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.Cost.instDecidableEqData :
      DecidableEq Data
      Equations
      source
      @[instance_reducible]
      instance MIPRE.Cost.instReprData :
      Repr Data
      Equations
      source
      def MIPRE.Cost.instReprData.repr :
      Data โ†’ โ„• โ†’ Std.Format
      Equations
      Instances For
        source
        @[instance_reducible]
        instance MIPRE.Cost.instInhabitedData :
        Inhabited Data
        Equations
        source
        def MIPRE.Cost.Data.size :
        Data โ†’ โ„•

        Size: the number of nodes, nil counting one.

        Equations
        Instances For
          source
          @[simp]
          theorem MIPRE.Cost.Data.size_nil :
          nil.size = 1
          source
          @[simp]
          theorem MIPRE.Cost.Data.size_cons (a b : Data) :
          (a.cons b).size = a.size + b.size + 1
          source
          theorem MIPRE.Cost.Data.size_pos (d : Data) :
          0 < d.size
          source
          def MIPRE.Cost.Data.toBits :
          Data โ†’ List Bool

          Preorder serialization, one bit per node: nil โ†ฆ 0, cons a b โ†ฆ 1 ยท a ยท b. It is a prefix code, and its length is the size.

          Equations
          Instances For
            source
            @[simp]
            theorem MIPRE.Cost.Data.length_toBits (d : Data) :
            d.toBits.length = d.size
            source
            def MIPRE.Cost.Data.ofNat :
            โ„• โ†’ Data

            Unary numerals: ofNat n is the list of n copies of nil. Used for tags, counters and budgets.

            Equations
            Instances For
              source
              @[simp]
              theorem MIPRE.Cost.Data.size_ofNat (n : โ„•) :
              (ofNat n).size = 2 * n + 1
              source
              def MIPRE.Cost.Data.toNat? :
              Data โ†’ Option โ„•

              Reading a unary numeral back.

              Equations
              Instances For
                source
                @[simp]
                theorem MIPRE.Cost.Data.toNat?_ofNat (n : โ„•) :
                (ofNat n).toNat? = some n
                source
                inductive MIPRE.Cost.Prog :
                Type

                Programs of the ambient model, with de Bruijn variables (var 0 is the innermost bound variable; the input of a program is var 0).

                • var (i : โ„•) : Prog

                  Read variable i (copying it: cost 1 + size).

                • nil : Prog

                  The atom.

                • const (d : Data) : Prog

                  Literal data: evaluates to d, at cost d.size (the value is built).

                • cons (h t : Prog) : Prog

                  Build a node from the values of h and t.

                • elim (i : โ„•) (n c : Prog) : Prog

                  Inspect variable i in place: if it is nil, run n; if it is cons a b, run c with a and b bound as variables 0 and 1.

                • let_ (e b : Prog) : Prog

                  Bind the value of e as variable 0 and run b.

                • loop (b : Prog) : Prog

                  Iterate b on the state held in variable 0: b returns cons flag s'; if flag is nil the loop stops with result s', otherwise it continues with state s'. (A body result nil stops with result nil.)

                Instances For
                  source
                  @[instance_reducible]
                  instance MIPRE.Cost.instDecidableEqProg :
                  DecidableEq Prog
                  Equations
                  source
                  def MIPRE.Cost.instDecidableEqProg.decEq (xโœ xโœยน : Prog) :
                  Decidable (xโœ = xโœยน)
                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance MIPRE.Cost.instReprProg :
                    Repr Prog
                    Equations
                    source
                    def MIPRE.Cost.instReprProg.repr :
                    Prog โ†’ โ„• โ†’ Std.Format
                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance MIPRE.Cost.instInhabitedProg :
                      Inhabited Prog
                      Equations
                      source
                      def MIPRE.Cost.Prog.WellScoped :
                      โ„• โ†’ Prog โ†’ Prop

                      WellScoped n p: every variable of p is bound in an environment of length n.

                      Equations
                      Instances For
                        source
                        theorem MIPRE.Cost.Prog.WellScoped.mono {n m : โ„•} (h : n โ‰ค m) (p : Prog) :
                        WellScoped n p โ†’ WellScoped m p
                        source
                        @[reducible, inline]
                        abbrev MIPRE.Cost.Env :
                        Type

                        Environments: the values of the variables, innermost (index 0) first.

                        Equations
                        Instances For
                          source
                          def MIPRE.Cost.Env.get (env : Env) (i : โ„•) :
                          Data

                          Variable lookup; reading beyond the environment gives nil, so that the semantics is total.

                          Equations
                          Instances For
                            source
                            @[simp]
                            theorem MIPRE.Cost.Env.get_cons_zero (v : Data) (env : Env) :
                            get (v :: env) 0 = v
                            source
                            @[simp]
                            theorem MIPRE.Cost.Env.get_cons_succ (v : Data) (env : Env) (i : โ„•) :
                            get (v :: env) (i + 1) = env.get i
                            source
                            @[simp]
                            theorem MIPRE.Cost.Env.get_nil (i : โ„•) :
                            get [] i = Data.nil
                            source
                            theorem MIPRE.Cost.Env.get_append {env extra : Env} {i : โ„•} (h : i < List.length env) :
                            (env ++ extra).get i = env.get i
                            source
                            inductive MIPRE.Cost.Eval :
                            Env โ†’ Prog โ†’ Data โ†’ โ„• โ†’ Prop

                            Timed big-step semantics: Eval env p r t means that p, in environment env, halts with result r at cost t. One unit per rule; reading a variable or a literal additionally costs the size of the value.

                            Instances For
                              source
                              theorem MIPRE.Cost.Eval.pos {env : Env} {p : Prog} {r : Data} {t : โ„•} (h : Eval env p r t) :
                              0 < t

                              Costs are positive.

                              source
                              theorem MIPRE.Cost.Eval.deterministic {env : Env} {p : Prog} {r r' : Data} {t t' : โ„•} (h : Eval env p r t) (h' : Eval env p r' t') :
                              r = r' โˆง t = t'

                              The semantics is deterministic in both result and cost.

                              source
                              theorem MIPRE.Cost.Eval.size_le {env : Env} {p : Prog} {r : Data} {t : โ„•} (h : Eval env p r t) :
                              r.size โ‰ค t

                              A run of cost t produces a result of size at most t: every node of the result was either built (cons, nil) or copied (var, const) at unit cost per node.

                              source
                              theorem MIPRE.Cost.Eval.append_of_wellScoped {env : Env} {p : Prog} {r : Data} {t : โ„•} (h : Eval env p r t) (hp : Prog.WellScoped (List.length env) p) (extra : Env) :
                              Eval (env ++ extra) p r t

                              Extra environment entries are inert for a well-scoped program (weakening).

                              source
                              theorem MIPRE.Cost.Eval.of_append_of_wellScoped {env extra : Env} {p : Prog} {r : Data} {t : โ„•} (h : Eval (env ++ extra) p r t) (hp : Prog.WellScoped (List.length env) p) :
                              Eval env p r t

                              Extra environment entries are inert for a well-scoped program (strengthening).

                              source
                              def MIPRE.Cost.evalFuel :
                              โ„• โ†’ Env โ†’ Prog โ†’ Option (Data ร— โ„•)

                              Executable evaluator with fuel (one unit of fuel per rule), returning the result and its cost.

                              Equations
                              Instances For
                                source
                                theorem MIPRE.Cost.evalFuel_sound (f : โ„•) (env : Env) (p : Prog) (r : Data) (t : โ„•) :
                                evalFuel f env p = some (r, t) โ†’ Eval env p r t

                                The fuel evaluator is sound for the semantics.

                                source
                                def MIPRE.Cost.Halts (p : Prog) (x : Data) :
                                Prop

                                p halts on input x (run in the environment [x]).

                                Equations
                                Instances For
                                  source
                                  def MIPRE.Cost.HaltsWithin (p : Prog) (x : Data) (t : โ„•) :
                                  Prop

                                  p halts on x within cost t.

                                  Equations
                                  Instances For
                                    source
                                    def MIPRE.Cost.TimeBound (p : Prog) (T : โ„• โ†’ โ„•) :
                                    Prop

                                    A (total) time bound for p as a function of the input size. This is the notion TIME_๐’ฎ, TIME_๐’Ÿ โ‰ค โ‹ฏ of blueprint def:lambda-bounded specializes.

                                    Equations
                                    Instances For