Finite numeric switches for structured RAM programs

select compiles a finite family of commands into a decrementing decision tree. A valid numeric code in test selects the corresponding branch. The register one must contain one and be distinct from test.

def Complexity.RAM.Structured.Switch.cleared (store : Store) (test : ℕ) : Store

Store presented to the selected branch after the tested code has been decremented to zero.

Equations

• Complexity.RAM.Structured.Switch.cleared store test = Function.update store test 0

def Complexity.RAM.Structured.Switch.select (count test one : ℕ) : (Fin count → Cmd) → Cmd

A finite numeric switch. Invalid codes fall through to skip; correctness theorems use the explicit hypothesis code < count.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.Structured.Switch.select 0 x✝¹ x✝ x_6 = Complexity.RAM.Structured.Cmd.skip

def Complexity.RAM.Structured.Switch.stepCount (code branchSteps : ℕ) : ℕ

Exact compiled/source transition count for selecting code.

Equations

• Complexity.RAM.Structured.Switch.stepCount code branchSteps = 3 * code + branchSteps + 1

def Complexity.RAM.Structured.Switch.costBound (code branchCost width : ℕ) : ℕ

Envelope-based logarithmic-cost bound for selecting code.

Each skipped case pays at most seven envelope widths: three for the nonzero conditional and four for the decrement. The selected zero case pays one.

Equations

• Complexity.RAM.Structured.Switch.costBound code branchCost width = (7 * code + 1) * width + branchCost