Running word-RAM programs over a larger 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. The converse direction, simulating an operation by a program over a smaller basis with an instruction budget, is not formalized here.

Main definitions

• Cslib.WordRAM.Op.mapOp, Cslib.WordRAM.Instr.mapOp, Cslib.WordRAM.Program.mapOp, Cslib.WordRAM.Code.mapOp: translation along a map of bases.

Main results

• 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

Instructions

def 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.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

@[simp]

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

@[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_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

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_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.

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

Structured programs

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.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

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)

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

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

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

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

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)

@[simp]

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

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)