Documentation

Complexitylib.Models.RandomAccessMachine

Random access machines (surface) #

This is the public entry point for the library's Random Access Machine (RAM) model: a register machine with indirect addressing, executed under a logarithmic-cost time measure and a matching space measure. The model, its executable semantics, and both cost measures are defined in Complexitylib.Models.RandomAccessMachine.Defs; the operational metatheory is proved in …/Internal; the soundness of the cost convention is established in …/Soundness.

Main definitions #

Main results #

Relationship to the Turing-machine models #

The RAM shares the library's Language interface, so RAM.DTIME/RAM.DSPACE and the Turing-machine classes DTIME/DSPACE speak about the same objects. The classical two-way simulation bounds that make the models polynomially equivalent are (Cook–Reckhow, Time bounded random access machines, JCSS 7 (1973), 354–375; van Emde Boas, Machine models and simulations, Handbook of Theoretical Computer Science A, 1990):

Both overheads are polynomial, so RAM.DTIME and DTIME yield the same polynomial-time class: RAM-P = P. Under the unit-cost measure the RAM → TM direction fails — RAM.logGap_squaring exhibits a program whose unit-time is linear but whose output already needs exponentially many Turing steps to write — which is precisely why the model is defined with logarithmic cost. The bounded dense transition block is proved end to end, including selected actions, nested dispatch, concrete compilation, and explicit resource bounds. That block is a bounded program family: its register layout depends on the tape window, so it cannot by itself witness RAM.DTIME, whose program must be fixed. The uniform replacement now has a fixed sparse interleaved representation, checked runtime address/loading and action/dispatch layers, a fixed compiled loop that follows an arbitrary exact halting TM run, and a checked public-ABI marshaller and verdict extractor. The remaining TM-to-RAM work is now narrower: the repeated sparse core and complete public marshaller/extractor share a concrete envelope, a linear-times-word-width cost theorem, and a checked logarithmic word-width bound. The fixed compiled program now transfers TM.DecidesInTime to RAM.Program.DecidesInTime, packages the result in RAM.DTIME at its explicit transformed bound, and proves the class theorem P ⊆ RAM.P. The sharper parametric DTIME(T) statement still requires an explicit input-length domination hypothesis: the public marshaller necessarily costs O(n · log n), while an arbitrary stated time bound T need not dominate n. The reverse simulation is now checked end to end. Finite-support register functions have canonical sparse snapshots whose binary tape codec round-trips with an explicit length bound. Fixed lookup, update, binary-arithmetic, control, cleanup, initialization, iteration, and output machines realize every RAM instruction and complete halting run on twenty work tapes. The original sparse public-input ABI retains an explicit fourth-degree envelope as a simple fallback. The optimized machine instead leaves the dense public input on its read-only tape and maintains a positive-tagged sparse mutable overlay. Selected-width step accounting and a decreasing square potential give a checked O((n + T(n))²) public-ABI bound. Consequently, RAM_DTIME_subset_DTIME_sq gives the textbook RAM.DTIME(T) ⊆ DTIME(T²) under the explicit hypothesis n + 1 = O(T(n)). Choosing the least halting fuel also transfers every RAM.P decider to P; together with the fixed sparse forward simulator this proves RAM.RegisterStore.Machine.RAM_P_eq_P.

A worked decider #

The two-instruction program ⟨imm 0 1⟩ overwrites the verdict register with 1 and then halts (its program counter runs off the end). It decides the universal language in constant logarithmic time, exercising the full DecidesInTime API end to end.

source
def Complexity.RAM.acceptProg :
Program

The always-accept program: set the verdict register to 1.

Equations
Instances For
    source
    theorem Complexity.RAM.acceptProg_run (x : List Bool) :
    (run acceptProg 1 (initCfg x)).verdict = 1

    On any input, acceptProg halts after one step with verdict 1.

    source
    theorem Complexity.RAM.acceptProg_decides :
    acceptProg.DecidesInTime Set.univ fun (x : ℕ) => 2

    acceptProg decides the universal language in constant logarithmic time.

    source
    theorem Complexity.RAM.univ_mem_DTIME :
    Set.univ ∈ DTIME fun (x : ℕ) => 2

    The universal language is in RAM.DTIME at a constant bound: a witness that the RAM time classes are inhabited over the shared Language interface.

    source
    def Complexity.RAM.rejectProg :
    Program

    The always-reject program: set the verdict register to 0.

    Equations
    Instances For
      source
      theorem Complexity.RAM.rejectProg_run (x : List Bool) :
      (run rejectProg 1 (initCfg x)).verdict = 0

      On any input, rejectProg halts after one step with verdict 0.

      source
      theorem Complexity.RAM.rejectProg_decides :
      rejectProg.DecidesInTime ∅ fun (x : ℕ) => 2

      rejectProg decides the empty language in constant logarithmic time, exercising the rejection side of the DecidesInTime API.

      source
      theorem Complexity.RAM.empty_mem_DTIME :
      ∅ ∈ DTIME fun (x : ℕ) => 2

      The empty language is in RAM.DTIME at a constant bound (the rejection counterpart of univ_mem_DTIME).