Complete sparse RAM decision machine -- definitions #
def
Complexity.RAM.RegisterStore.Machine.programDecisionTM
{n : ℕ}
(tapes : ControlInstructionTapes n)
(program : Program)
:
Initialize the public RAM configuration, execute one fixed program through
its first halt, and extract the Boolean verdict from sparse register R₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Complexity.RAM.RegisterStore.Machine.programDecisionTime
{n : ℕ}
(tapes : ControlInstructionTapes n)
(program : Program)
(input : List Bool)
(fuel : ℕ)
:
Exact compositional bound for one fuel-certified RAM decision run.
Equations
- One or more equations did not get rendered due to their size.