Documentation

MIPRE.Foundations.Introspection.ClockCompiler

A binary compiler for the complete clocked source decider #

The compiler constructs the actual program syntax from the source description and binary parameter. Both compilation time and output description size are polynomial in their encoded lengths, for fixed exponent and universal machine.

source
noncomputable def MIPRE.Introspection.ClockSimulation.codeConst :
Cost.PolyTimeFun Cost.Data Cost.Prog
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Introspection.ClockSimulation.codeCons :
    Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.Introspection.ClockSimulation.codeLet :
      Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.Introspection.ClockSimulation.codeElim :
        Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.Introspection.ClockSimulation.codeCall (i : ℕ) :
          Cost.PolyTimeFun Cost.Prog Cost.Prog
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MIPRE.Introspection.ClockSimulation.codeContext :
            Cost.PolyTimeFun (Cost.Prog × Cost.Prog) Cost.Prog
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def MIPRE.Introspection.ClockSimulation.codeRoute (route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) :
              Cost.PolyTimeFun Cost.Prog Cost.Prog
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def MIPRE.Introspection.ClockSimulation.clockStageCompiler (k : ℕ) :
                Cost.PolyTimeFun ℕ Cost.Prog
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def MIPRE.Introspection.ClockSimulation.simulationInputCompiler :
                  Cost.PolyTimeFun Cost.Prog Cost.Prog
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def MIPRE.Introspection.ClockSimulation.reindexStageCompiler :
                    Cost.PolyTimeFun Cost.Prog Cost.Prog
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def MIPRE.Introspection.ClockSimulation.compiler (k : ℕ) (U : Cost.ClockedUniversalMachine) :
                      Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Prog

                      An actual ambient compiler for the existing clocked decider program.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem MIPRE.Introspection.ClockSimulation.compiler_apply (k : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (lam : ℕ) :
                        (compiler k U).toFun (source, lam) = (decider k lam U source).prog
                        source
                        theorem MIPRE.Introspection.ClockSimulation.compiler_runs (k : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (lam : ℕ) :
                        ∃ time ≤ Polynomial.eval (Cost.esize source + Cost.esize lam + 1) (compiler k U).timeBound, (compiler k U).code.Runs (Cost.encode (source, lam)) (Cost.encode (decider k lam U source).prog) time
                        source
                        theorem MIPRE.Introspection.ClockSimulation.decider_size_le (k : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (lam : ℕ) :
                        Cost.esize (decider k lam U source).prog ≤ Polynomial.eval (Cost.esize source + Cost.esize lam + 1) (compiler k U).timeBound
                        source
                        theorem MIPRE.Introspection.ClockSimulation.compiler_binary_bounds (k : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (lam : ℕ) :
                        Cost.esize (decider k lam U source).prog ≤ Polynomial.eval (Cost.esize source + 4 * lam.size + 2) (compiler k U).timeBound ∧ ∃ time ≤ Polynomial.eval (Cost.esize source + 4 * lam.size + 2) (compiler k U).timeBound, (compiler k U).code.Runs (Cost.encode (source, lam)) (Cost.encode (decider k lam U source).prog) time

                        The parameter enters both compiler cost and description length through its bits.