Operation bases for word RAMs

Word-RAM models differ in their arithmetic and logical instructions. Hagerup distinguishes the restricted RAM, without multiplication, from the multiplication RAM Hagerup, and the AC⁰ RAM allows only operations computed by polynomial-size constant-depth circuits, which excludes multiplication Andersson, Miltersen and Thorup. Linear-time and data-structure bounds can depend on this choice.

A basis (Cslib.WordRAM.Basis) fixes these operations, as a circuit basis does: a signature of operation symbols with arities (Cslib.Circuits.Signature), and the value of every symbol on natural numbers at each word size w, which may be undefined (none). The machine itself, its registers, memory, control flow and faults are the same for every basis; an operation faults when its value is undefined or does not fit a word. A basis also marks the operations that are exempt from word-size monotonicity: every other operation keeps each value that fits a word at every larger word size, so that a successful run of a program avoiding the marked operations succeeds in the same way at every larger word size.

Bases are compared by meaning-preserving maps of their operations (Cslib.WordRAM.Basis.Hom), built on Cslib.Circuits.Signature.Hom. A program over a basis runs instruction for instruction over a larger one; Cslib.WordRAM.Basis.restrict gives the sub-bases of a basis.

Main definitions

• Cslib.WordRAM.Basis: operation symbols, their meaning at each word size, and the symbols exempt from word-size monotonicity.
• Cslib.WordRAM.BinOp, Cslib.WordRAM.StandardOp, Cslib.WordRAM.Basis.standard: the standard word-RAM operations: addition, subtraction, multiplication, bitwise operations and shifts as in Hagerup, together with division, remainder and the word size, with truncated subtraction and Lean's division by zero.
• Cslib.WordRAM.BinOp.evalExact, Cslib.WordRAM.Basis.exact: the same operations with their exact values: subtraction below zero and division and remainder by zero are undefined.
• Cslib.WordRAM.Basis.Hom: a map of bases that keeps the meaning of every operation.
• Cslib.WordRAM.Basis.restrict: the sub-basis of the operations satisfying a predicate.
• Cslib.WordRAM.Basis.additive, Cslib.WordRAM.Basis.arithmetic: addition and subtraction; and these with multiplication, division and remainder, the operation symbols of the bounded-word RAM of MIT–ULB CompGeom Group, on unsigned words with truncated subtraction.

Main results

• Cslib.WordRAM.Basis.Hom.interp_map: the image of an operation under a map of bases has the operation's value.
• Cslib.WordRAM.Basis.arithmeticHomStandard_comp_additiveHomArithmetic: the inclusions of the named bases commute.

References

• A. Andersson, P. B. Miltersen and M. Thorup, Fusion trees can be implemented with AC⁰ instructions only
• M. L. Fredman and D. E. Willard, Surpassing the information theoretic bound with fusion trees
• T. Hagerup, Sorting and searching on the word RAM
• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

structure Cslib.WordRAM.Basis extends Cslib.Circuits.Signature : Type 1

A basis of word operations: a signature of operation symbols, the value of each operation at each word size, none where it is undefined, and the operations that may read the word size. An operation that does not read the word size keeps each value that fits a word at every larger word size. Whether a value fits a word is checked by the machine, not by the basis.

• Op : Type
• Arity : self.Op → ℕ
• decEq : DecidableEq self.Op

  Operation symbols have decidable equality, so that programs do.

• ReadsWidth : self.Op → Prop

  The operations exempt from word-size monotonicity (interp_mono_of_not_readsWidth), such as one that returns the word size.

• decReadsWidth : DecidablePred self.ReadsWidth

  Whether an operation reads the word size is decidable.

• interp : ℕ → (f : self.Op) → (Fin (self.Arity f) → ℕ) → Option ℕ

  The value of every operation at word size w, or none if it is undefined.

• interp_mono_of_not_readsWidth (f : self.Op) (hf : ¬self.ReadsWidth f) {w w' : ℕ} (hw : w ≤ w') {args : Fin (self.Arity f) → ℕ} {v : ℕ} (h : self.interp w f args = some v) (hv : v < 2 ^ w) : self.interp w' f args = some v

  An operation that does not read the word size keeps each value that fits a word at every larger word size.

The standard basis

inductive Cslib.WordRAM.BinOp : Type

The binary operations of the word RAM.

• add : BinOp

  Addition.

• sub : BinOp

  Subtraction.

• mul : BinOp

  Multiplication.

• div : BinOp

  Division, rounding down.

• mod : BinOp

  Remainder.

• and : BinOp

  Bitwise and.

• or : BinOp

  Bitwise or.

• xor : BinOp

  Bitwise exclusive or.

• shiftLeft : BinOp

  Shift left: x <<< y = x * 2 ^ y.

• shiftRight : BinOp

  Shift right: x >>> y = x / 2 ^ y.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqBinOp : DecidableEq BinOp

def Cslib.WordRAM.instReprBinOp.repr : BinOp → ℕ → Std.Format

@[instance_reducible]

instance Cslib.WordRAM.instReprBinOp : Repr BinOp

def Cslib.WordRAM.BinOp.eval : BinOp → ℕ → ℕ → ℕ

The value of a binary operation on natural numbers. Subtraction is truncated, and division and remainder by zero follow Lean's conventions x / 0 = 0 and x % 0 = x. Whether the value fits a word is checked by the instruction that writes it.

inductive Cslib.WordRAM.StandardOp : Type

The operations of the standard basis: the binary operations, and reading the word size.

• bin (f : BinOp) : StandardOp

  A binary operation.

• width : StandardOp

  The word size, an operation without arguments.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqStandardOp : DecidableEq StandardOp

def Cslib.WordRAM.instDecidableEqStandardOp.decEq (x✝ x✝¹ : StandardOp) : Decidable (x✝ = x✝¹)

def Cslib.WordRAM.instReprStandardOp.repr : StandardOp → ℕ → Std.Format

@[instance_reducible]

instance Cslib.WordRAM.instReprStandardOp : Repr StandardOp

def Cslib.WordRAM.StandardOp.arity : StandardOp → ℕ

The number of arguments of a standard operation.

def Cslib.WordRAM.StandardOp.eval (w : ℕ) (f : StandardOp) : (Fin f.arity → ℕ) → Option ℕ

The value of a standard operation at word size w.

@[reducible, inline]

abbrev Cslib.WordRAM.Basis.standard : Basis

The standard word-RAM basis: addition, subtraction, multiplication, bitwise operations and shifts as in Hagerup, together with division and remainder, and the word size, which word-RAM algorithms may read Fredman and Willard. Only the word size reads the word size.

theorem Cslib.WordRAM.Basis.standard_op : standard.Op = StandardOp

@[simp]

theorem Cslib.WordRAM.Basis.standard_interp_bin (w : ℕ) (f : BinOp) (x : Fin 2 → ℕ) : standard.interp w (StandardOp.bin f) x = some (f.eval (x 0) (x 1))

@[simp]

theorem Cslib.WordRAM.Basis.standard_interp_width (w : ℕ) (x : Fin 0 → ℕ) : standard.interp w StandardOp.width x = some w

@[simp]

theorem Cslib.WordRAM.Basis.standard_readsWidth (f : StandardOp) : standard.ReadsWidth f ↔ f = StandardOp.width

The exact basis

def Cslib.WordRAM.BinOp.evalExact : BinOp → ℕ → ℕ → Option ℕ

The exact value of a binary operation on natural numbers: subtraction below zero, and division and remainder by zero, are undefined. Elsewhere it is BinOp.eval.

def Cslib.WordRAM.StandardOp.evalExact (w : ℕ) (f : StandardOp) : (Fin f.arity → ℕ) → Option ℕ

The exact value of a standard operation at word size w.

@[reducible, inline]

abbrev Cslib.WordRAM.Basis.exact : Basis

The exact word-RAM basis: the operations of Basis.standard, where every operation computes its exact value, so that subtraction below zero and division and remainder by zero are undefined and fault. Only the word size reads the word size. The bounded-word RAM of MIT–ULB CompGeom Group does not reject a negative difference or a zero divisor as such: it subtracts signed words, its division and remainder by zero follow Lean's integer conventions x / 0 = 0 and x % 0 = x, and only its usual check that the result fits a signed word applies.

@[simp]

theorem Cslib.WordRAM.Basis.exact_interp_bin (w : ℕ) (f : BinOp) (x : Fin 2 → ℕ) : exact.interp w (StandardOp.bin f) x = f.evalExact (x 0) (x 1)

@[simp]

theorem Cslib.WordRAM.Basis.exact_interp_width (w : ℕ) (x : Fin 0 → ℕ) : exact.interp w StandardOp.width x = some w

@[simp]

theorem Cslib.WordRAM.Basis.exact_readsWidth (f : StandardOp) : exact.ReadsWidth f ↔ f = StandardOp.width

Maps of bases

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

A map of bases: a map of signatures (Cslib.Circuits.Signature.Hom) such that at each word size the image of every operation has the operation's value, and that sends an operation not marked as reading the word size to one not so marked. Programs over B then run instruction for instruction over B'.

• toFun : B.Op → B'.Op
• arity_eq (op : B.Op) : B'.Arity (self.toFun op) = B.Arity op
• preserves (w : ℕ) (f : B.Op) (x : Fin (B.Arity f) → ℕ) : (B'.interp w (self.toHom f) fun (a : Fin (B'.Arity (self.toHom f))) => x (Fin.cast ⋯ a)) = B.interp w f x

  At each word size, the image of each operation, applied to arguments reindexed along Signature.Hom.arity_eq, has the operation's value.

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

  An operation whose image reads the word size reads it itself.

@[reducible, inline]

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

The image of an operation under a map of bases.

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

theorem Cslib.WordRAM.Basis.Hom.interp_map {B B' : Basis} (φ : B.Hom B') (w : ℕ) (f : B.Op) (x : Fin (B.Arity f) → ℕ) : (B'.interp w (φ.map f) fun (a : Fin (B'.Arity (φ.map f))) => x (Fin.cast ⋯ a)) = B.interp w f x

The image of an operation, applied to arguments reindexed along arity_map, has the value of the operation.

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

The identity map of a basis.

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

The composition of maps of bases.

@[simp]

theorem Cslib.WordRAM.Basis.Hom.id_map {B : Basis} (f : B.Op) : (Hom.id B).map f = f

@[simp]

theorem Cslib.WordRAM.Basis.Hom.comp_map {B B' B'' : Basis} (ψ : B'.Hom B'') (φ : B.Hom B') (f : B.Op) : (ψ.comp φ).map f = ψ.map (φ.map f)

Sub-bases

def Cslib.WordRAM.Basis.restrict (B : Basis) (P : B.Op → Prop) : Basis

The sub-basis of B consisting of the operations satisfying P.

def Cslib.WordRAM.Basis.restrictHom (B : Basis) (P : B.Op → Prop) : (B.restrict P).Hom B

The inclusion of a sub-basis.

def Cslib.WordRAM.Basis.additive : Basis

Addition and truncated subtraction.

def Cslib.WordRAM.Basis.arithmetic : Basis

Addition, truncated subtraction, multiplication, division and remainder: the operation symbols of the bounded-word RAM of MIT–ULB CompGeom Group, without bitwise operations, shifts or the word size. Words here are unsigned and subtraction is truncated, whereas the source subtracts signed words; on the other operations and nonnegative arguments the two agree.

def Cslib.WordRAM.Basis.additiveHomArithmetic : additive.Hom arithmetic

The additive operations are arithmetic.

def Cslib.WordRAM.Basis.arithmeticHomStandard : arithmetic.Hom standard

The arithmetic operations are standard.

def Cslib.WordRAM.Basis.additiveHomStandard : additive.Hom standard

The additive operations are standard.

theorem Cslib.WordRAM.Basis.arithmeticHomStandard_comp_additiveHomArithmetic (f : additive.Op) : (arithmeticHomStandard.comp additiveHomArithmetic).map f = additiveHomStandard.map f

The two inclusions of the additive operations in the standard ones agree.