Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.Program.Bounds.Defs

Sparse RAM decision-machine resource-bound definitions #

The concrete simulator has fixed control once its RAM program is fixed. The only program-dependent quantities that matter asymptotically are therefore collected in programResourceMagnitude. programDecisionScale combines that constant with the public input length and the charged logarithmic RAM time. The fourth-power envelope is deliberately coarse: it keeps the public class-transfer theorem independent of low-level controller constants while still recording a genuine polynomial simulation.

source
def Complexity.RAM.RegisterStore.Machine.instructionResourceMagnitude :
Instr → ℕ

A positive magnitude containing every natural literal of one instruction.

Equations
Instances For
    source
    def Complexity.RAM.RegisterStore.Machine.programResourceMagnitude (program : Program) :
    ℕ

    One positive fixed constant containing the program length and every hardwired register, immediate, and jump literal.

    Equations
    Instances For
      source
      def Complexity.RAM.RegisterStore.Machine.programDecisionScale (program : Program) (inputLength cost : ℕ) :
      ℕ

      Common width/count scale for a run with charged logarithmic time cost.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.RAM.RegisterStore.Machine.programDecisionEnvelope (program : Program) (inputLength cost : ℕ) :
        ℕ

        Coarse checked polynomial envelope for the complete concrete simulation.

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