Running word-RAM programs over a larger or simulating basis

A map of bases φ : B.Hom B' (Cslib.WordRAM.Basis.Hom) sends every operation of B to an operation of B' with the same meaning at every word size. Replacing each operation of a program by its image (Cslib.WordRAM.Program.mapOp, Cslib.WordRAM.Code.mapOp) leaves every other instruction in place, so the translated program takes exactly the same steps: the same states, faults, outputs and instruction counts (Cslib.WordRAM.step_mapOp). Decision procedures and the classes of Cslib.WordRAM.LinearTime and Cslib.WordRAM.PolynomialTime therefore grow with the basis. This is the word-RAM analogue of translating circuits along a map of signatures (Cslib.Circuits.Circuit.mapOp), with a budget of one instruction for every operation.

A result proved over a small basis thus holds over every basis containing it: over Cslib.WordRAM.Basis.standard, and over any other basis that interprets the same operations in the same way. More generally, a defined-evaluation simulation ψ : B.Simulates B' (Cslib.WordRAM.Basis.Simulates) only requires B' to agree with B on operations that evaluate to some v in B, allowing B' to define values on inputs where B faults (as in Cslib.WordRAM.Basis.Simulates.exactStandard : Basis.Simulates .exact .standard). Every non-faulting structured execution transfers instruction-for-instruction along ψ (Cslib.WordRAM.Exec.mapSimulates, Cslib.WordRAM.ExecWithin.mapSimulates), and every basis homomorphism φ : B.Hom B' induces a simulation Basis.Simulates.ofHom φ with Op.mapOp φ = Op.mapSimulates (.ofHom φ) and Code.mapOp φ = Code.mapSimulates (.ofHom φ).

Main definitions

• Cslib.WordRAM.Basis.Simulates, Cslib.WordRAM.Basis.Simulates.ofHom, Cslib.WordRAM.Basis.Simulates.exactStandard: defined-evaluation basis simulation and the canonical simulation of Basis.exact by Basis.standard.
• Cslib.WordRAM.Op.mapSimulates, Cslib.WordRAM.Code.mapSimulates: translation of data instructions and structured programs along a defined-evaluation simulation.
• Cslib.WordRAM.Op.mapOp, Cslib.WordRAM.Instr.mapOp, Cslib.WordRAM.Program.mapOp, Cslib.WordRAM.Code.mapOp, Cslib.WordRAM.WordSizeDependentProgram.mapOp: translation along a map of bases.

Main results

• Cslib.WordRAM.Op.eval_mapSimulates_of_some, Cslib.WordRAM.Exec.mapSimulates, Cslib.WordRAM.ExecWithin.mapSimulates: non-faulting structured executions transfer along a defined-evaluation simulation.
• Cslib.WordRAM.Op.eval_mapOp, Cslib.WordRAM.step_mapOp: translated instructions have the same effect.
• Cslib.WordRAM.executes_mapOp_iff, Cslib.WordRAM.Exec.mapOp: translated programs halt in the same way, with the same instruction count.
• Cslib.WordRAM.Code.assemble_mapOp: translation commutes with assembly.
• Cslib.WordRAM.DecidableInTime.mapOp, Cslib.WordRAM.LinearTime.mapOp, Cslib.WordRAM.PolynomialTime.mapOp: decision transfers to a larger basis with the same time bound and word-size threshold.

References

• T. Hagerup, Sorting and searching on the word RAM

Defined-evaluation basis simulation

structure Cslib.WordRAM.Basis.Simulates (B B' : Basis) extends B.Hom B'.toSignature : Type

B is simulated by B' on defined evaluations when every non-faulting operation in B evaluates to the same value in B' without introducing ReadsWidth. Unlike Basis.Hom, B' may define values on inputs where B faults (such as Basis.exact vs Basis.standard).

• toFun : B.Op → B'.Op
• arity_eq (op : B.Op) : B'.Arity (self.toFun op) = B.Arity op
• eval_some (w : ℕ) (f : B.Op) (args : Fin (B.Arity f) → ℕ) {v : ℕ} : B.interp w f args = some v → (B'.interp w (self.toHom f) fun (a : Fin (B'.Arity (self.toHom f))) => args (Fin.cast ⋯ a)) = some v

  Every defined operation value in B is preserved in B'.

• readsWidth_of_map (f : B.Op) : B'.ReadsWidth (self.toHom f) → B.ReadsWidth f

  Simulation does not introduce word-size reads.

@[reducible, inline]

abbrev Cslib.WordRAM.Basis.Simulates.map {B B' : Basis} (φ : B.Simulates B') (f : B.Op) : B'.Op

Image of an operation symbol under a simulation.

theorem Cslib.WordRAM.Basis.Simulates.arity_map {B B' : Basis} (φ : B.Simulates B') (f : B.Op) : B'.Arity (φ.map f) = B.Arity f

Simulation preserves operation arity.

def Cslib.WordRAM.Basis.Simulates.id (B : Basis) : B.Simulates B

Identity basis simulation.

def Cslib.WordRAM.Basis.Simulates.comp {B B' B'' : Basis} (ψ : B'.Simulates B'') (φ : B.Simulates B') : B.Simulates B''

Composition of basis simulations.

def Cslib.WordRAM.Basis.Simulates.ofHom {B B' : Basis} (φ : B.Hom B') : B.Simulates B'

Every exact basis homomorphism induces a defined-evaluation simulation.

def Cslib.WordRAM.Basis.Simulates.exactStandard : exact.Simulates standard

Every non-faulting Basis.exact operation evaluates to the same value in Basis.standard.

Instructions

def Cslib.WordRAM.Op.mapSimulates {B B' : Basis} {r : ℕ} (φ : B.Simulates B') : Op B r → Op B' r

The data instruction applying φ f in place of each operation f along a basis simulation.

@[reducible, inline]

abbrev Cslib.WordRAM.Op.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') : Op B r → Op B' r

The data instruction applying φ f in place of each operation f.

def Cslib.WordRAM.Instr.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') : Instr B r → Instr B' r

The instruction applying φ f in place of each operation f.

def Cslib.WordRAM.Program.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (p : Program B r) : Program B' r

The program applying φ f in place of each operation f, instruction for instruction.

def Cslib.WordRAM.Code.mapSimulates {B B' : Basis} {r : ℕ} (φ : B.Simulates B') : Code B r → Code B' r

The structured program applying φ f in place of each operation f along a basis simulation.

@[reducible, inline]

abbrev Cslib.WordRAM.Code.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') : Code B r → Code B' r

The structured program applying φ f in place of each operation f.

@[simp]

theorem Cslib.WordRAM.Program.length_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (p : Program B r) : List.length (mapOp φ p) = List.length p

Translating a program along a basis homomorphism preserves its length.

@[simp]

theorem Cslib.WordRAM.Code.size_mapSimulates {B B' : Basis} {r : ℕ} (ψ : B.Simulates B') (c : Code B r) : (mapSimulates ψ c).size = c.size

Translating along a basis simulation preserves compiled program size.

theorem Cslib.WordRAM.Code.size_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (c : Code B r) : (mapOp φ c).size = c.size

Translating a structured program along a basis homomorphism preserves its size.

theorem Cslib.WordRAM.Op.eval_mapSimulates_of_some {B B' : Basis} {r w : ℕ} (ψ : B.Simulates B') {o : Op B r} {x y : Data r} (h : eval w o x = some y) : eval w (mapSimulates ψ o) x = some y

Any non-faulting evaluation of a data instruction is preserved under Op.mapSimulates.

@[simp]

theorem Cslib.WordRAM.Op.eval_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (o : Op B r) (w : ℕ) (x : Data r) : eval w (mapOp φ o) x = eval w o x

A translated data instruction has the same effect.

theorem Cslib.WordRAM.Op.readsWidth_of_mapSimulates {B B' : Basis} {r : ℕ} (ψ : B.Simulates B') {o : Op B r} (h : (mapSimulates ψ o).ReadsWidth) : o.ReadsWidth

A data instruction translated along a simulation reads the word size only if the instruction does.

theorem Cslib.WordRAM.Op.readsWidth_of_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {o : Op B r} (h : (mapOp φ o).ReadsWidth) : o.ReadsWidth

A translated data instruction reads the word size only if the instruction does.

theorem Cslib.WordRAM.Instr.readsWidth_of_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {i : Instr B r} (h : (mapOp φ i).ReadsWidth) : i.ReadsWidth

A translated instruction reads the word size only if the instruction does.

theorem Cslib.WordRAM.Program.readsWidth_of_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {p : Program B r} (h : (mapOp φ p).ReadsWidth) : p.ReadsWidth

A translated program reads the word size only if the program does.

theorem Cslib.WordRAM.Code.readsWidth_of_mapSimulates {B B' : Basis} {r : ℕ} (ψ : B.Simulates B') {c : Code B r} (h : (mapSimulates ψ c).ReadsWidth) : c.ReadsWidth

A structured program translated along a simulation reads the word size only if the program does.

theorem Cslib.WordRAM.Code.readsWidth_of_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {c : Code B r} (h : (mapOp φ c).ReadsWidth) : c.ReadsWidth

A translated structured program reads the word size only if the program does.

@[simp]

theorem Cslib.WordRAM.Instr.isRandFree_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (i : Instr B r) : (mapOp φ i).IsRandFree ↔ i.IsRandFree

Translating an instruction along a basis homomorphism preserves IsRandFree.

@[simp]

theorem Cslib.WordRAM.Program.isRandFree_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (p : Program B r) : (mapOp φ p).IsRandFree ↔ p.IsRandFree

Translating a flat program along a basis homomorphism preserves IsRandFree.

@[simp]

theorem Cslib.WordRAM.Code.isRandFree_mapSimulates {B B' : Basis} {r : ℕ} (ψ : B.Simulates B') (c : Code B r) : (mapSimulates ψ c).IsRandFree ↔ c.IsRandFree

Translating a structured program along a basis simulation preserves IsRandFree.

theorem Cslib.WordRAM.Code.isRandFree_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (c : Code B r) : (mapOp φ c).IsRandFree ↔ c.IsRandFree

Translating a structured program along a basis homomorphism preserves IsRandFree.

Runs

@[simp]

theorem Cslib.WordRAM.step_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) (s : State r) : step w (Program.mapOp φ p) s = step w p s

Translation preserves steps. The translated program takes the same step from every state: the same next state, output or fault.

theorem Cslib.WordRAM.next_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) : Next w (Program.mapOp φ p) = Next w p

theorem Cslib.WordRAM.runs_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) : Runs w (Program.mapOp φ p) = Runs w p

@[simp]

theorem Cslib.WordRAM.executes_mapOp_iff {B B' : Basis} {r : ℕ} (φ : B.Hom B') {w : ℕ} {p : Program B r} {s : State r} {v n : ℕ} : Executes w (Program.mapOp φ p) s v n ↔ Executes w p s v n

Translation preserves halting runs. The translated program halts with the same output after the same number of instructions.

@[simp]

theorem Cslib.WordRAM.run_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) (fuel : ℕ) (s : State r) : run w (Program.mapOp φ p) fuel s = run w p fuel s

Fuel-bounded execution of a translated program agrees with the original program.

Structured programs

theorem Cslib.WordRAM.Exec.mapSimulates {B B' : Basis} {r w : ℕ} (ψ : B.Simulates B') {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n) : Exec w (Code.mapSimulates ψ c) x y n

Non-faulting structured executions transfer instruction-for-instruction along Simulates.

theorem Cslib.WordRAM.Exec.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n) : Exec w (Code.mapOp φ c) x y n

A translated structured program runs in the same way, with the same instruction count.

theorem Cslib.WordRAM.ExecWithin.mapSimulates {B B' : Basis} {r w T : ℕ} (ψ : B.Simulates B') {c : Code B r} {x y : Data r} (h : ExecWithin w c x y T) : ExecWithin w (Code.mapSimulates ψ c) x y T

Bounded-step structured executions transfer along Simulates.

theorem Cslib.WordRAM.ExecWithin.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {w T : ℕ} {c : Code B r} {x y : Data r} (h : ExecWithin w c x y T) : ExecWithin w (Code.mapOp φ c) x y T

Bounded-step execution of a structured program transfers along a basis homomorphism.

theorem Cslib.WordRAM.Code.assemble_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (c : Code B r) (pc : ℕ) : (mapOp φ c).assemble pc = Program.mapOp φ (c.assemble pc)

Translation commutes with assembly.

theorem Cslib.WordRAM.Code.program_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (c : Code B r) (out : Fin r) : (mapOp φ c).program out = Program.mapOp φ (c.program out)

Translation commutes with compiling a structured program into a complete halting program.

theorem Cslib.WordRAM.Code.Answers.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {c : Code B r} {out : Fin r} {w : ℕ} {input : List ℕ} {b : Prop} {time : ℕ} (h : c.Answers out w input b time) : (Code.mapOp φ c).Answers out w input b time

A structured program that answers a question continues to answer it after translation.

Decision

@[simp]

theorem Cslib.WordRAM.Program.answers_mapOp_iff {B B' : Basis} {r : ℕ} (φ : B.Hom B') {p : Program B r} {w : ℕ} {input : List ℕ} {b : Prop} {time : ℕ} : (mapOp φ p).Answers w input b time ↔ p.Answers w input b time

A translated flat program answers a question within time steps if and only if the original program does.

theorem Cslib.WordRAM.Program.DecidesInTime.mapOp {B B' : Basis} {r : ℕ} {α : Type u_1} (φ : B.Hom B') {p : Program B r} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (h : p.DecidesInTime encode A time allowed) : (Program.mapOp φ p).DecidesInTime encode A time allowed

A flat decision procedure transfers along a basis homomorphism with the same time bound.

def Cslib.WordRAM.WordSizeDependentProgram.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (P : WordSizeDependentProgram B r) : WordSizeDependentProgram B' r

Translate each member of a width-indexed family.

theorem Cslib.WordRAM.WordSizeDependentProgram.BoundedCode.mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') {P : WordSizeDependentProgram B r} (h : P.BoundedCode) : (WordSizeDependentProgram.mapOp φ P).BoundedCode

Translation preserves the code-length bound.

theorem Cslib.WordRAM.WordSizeDependentProgram.DecidesInTime.mapOp {B B' : Basis} {r : ℕ} {α : Type u_1} (φ : B.Hom B') {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (h : P.DecidesInTime encode A time allowed) : (WordSizeDependentProgram.mapOp φ P).DecidesInTime encode A time allowed

Translation preserves family decision at the same width and instruction count.

theorem Cslib.WordRAM.DecidableInTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (φ : B.Hom B') (h : DecidableInTime B A encode time allowed) : DecidableInTime B' A encode time allowed

Nonuniform decision grows with the operation basis, preserving code length.

theorem Cslib.WordRAM.UniformDecidableInTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (φ : B.Hom B') (h : UniformDecidableInTime B A encode time allowed) : UniformDecidableInTime B' A encode time allowed

Uniform decision grows with the operation basis.

theorem Cslib.WordRAM.LinearTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (φ : B.Hom B') (h : LinearTime B A encode size) : LinearTime B' A encode size

Linear time over a basis is linear time over every larger basis.

theorem Cslib.WordRAM.UniformLinearTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (φ : B.Hom B') (h : UniformLinearTime B A encode size) : UniformLinearTime B' A encode size

Uniform linear time grows with the operation basis.

theorem Cslib.WordRAM.PolynomialTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (φ : B.Hom B') (h : PolynomialTime B A encode size) : PolynomialTime B' A encode size

Polynomial time over a basis is polynomial time over every larger basis.

theorem Cslib.WordRAM.UniformPolynomialTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (φ : B.Hom B') (h : UniformPolynomialTime B A encode size) : UniformPolynomialTime B' A encode size

Uniform polynomial time grows with the operation basis.

Functoriality

@[simp]

theorem Cslib.WordRAM.Op.mapOp_id {B : Basis} {r : ℕ} (o : Op B r) : mapOp (Basis.Hom.id B) o = o

Translating a data instruction along the identity basis homomorphism leaves it unchanged.

theorem Cslib.WordRAM.Op.mapOp_comp {B B' B'' : Basis} {r : ℕ} (ψ : B'.Hom B'') (φ : B.Hom B') (o : Op B r) : mapOp (ψ.comp φ) o = mapOp ψ (mapOp φ o)

Translating a data instruction along a composition of basis homomorphisms composes the translations.

@[simp]

theorem Cslib.WordRAM.Program.mapOp_id {B : Basis} {r : ℕ} (p : Program B r) : mapOp (Basis.Hom.id B) p = p

Translating a program along the identity basis homomorphism leaves it unchanged.

theorem Cslib.WordRAM.Program.mapOp_comp {B B' B'' : Basis} {r : ℕ} (ψ : B'.Hom B'') (φ : B.Hom B') (p : Program B r) : mapOp (ψ.comp φ) p = mapOp ψ (mapOp φ p)

Translating a program along a composition of basis homomorphisms composes the translations.