TimeM: Time Complexity Monad

TimeM T α represents a computation that produces a value of type α and tracks its time cost.

T is usually instantiated as ℕ to count operations, but can be instantiated as ℝ to count actual wall time, or as more complex types in order to model more general costs.

Design Principles

1. Pure inputs, timed outputs: Functions take plain values and return TimeM results
2. Time annotations are trusted: The time field is NOT verified against actual cost. You must manually ensure annotations match the algorithm's complexity in your cost model.
3. Separation of concerns: Prove correctness properties on .ret, prove complexity on .time

Cost Model

Document your cost model explicitly Decide and be consistent about:

• What costs 1 unit? (comparison, arithmetic operation, etc.)
• What is free? (variable lookup, pattern matching, etc.)
• Recursive calls: Do you charge for the call itself?

Notation

• ✓ : A tick of time, see tick.
• ⟪tm⟫ : Extract the pure value from a TimeM computation (notation for tm.ret)

References

See [Dan08] for the discussion.

structure Cslib.Algorithms.Lean.TimeM (T : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A monad for tracking time complexity of computations. TimeM T α represents a computation that returns a value of type α and accumulates a time cost (represented as a type T, typically ℕ).

• ret : α

  The return value of the computation

• time : T

  The accumulated time cost of the computation

theorem Cslib.Algorithms.Lean.TimeM.ext {T : Type u_1} {α : Type u_2} {x y : TimeM T α} (ret : x.ret = y.ret) (time : x.time = y.time) : x = y

theorem Cslib.Algorithms.Lean.TimeM.ext_iff {T : Type u_1} {α : Type u_2} {x y : TimeM T α} : x = y ↔ x.ret = y.ret ∧ x.time = y.time

def Cslib.Algorithms.Lean.TimeM.pure {T : Type u_1} [Zero T] {α : Type u_2} (a : α) : TimeM T α

Lifts a pure value into a TimeM computation with zero time cost.

Prefer to use pure instead of TimeM.pure.

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instPureOfZero {T : Type u_1} [Zero T] : Pure (TimeM T)

def Cslib.Algorithms.Lean.TimeM.bind {T : Type u_1} {α : Type u_2} {β : Type u_3} [Add T] (m : TimeM T α) (f : α → TimeM T β) : TimeM T β

Sequentially composes two TimeM computations, summing their time costs.

Prefer to use the >>= notation.

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instBindOfAdd {T : Type u_1} [Add T] : Bind (TimeM T)

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instFunctor {T : Type u_1} : Functor (TimeM T)

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instSeqOfAdd {T : Type u_1} [Add T] : Seq (TimeM T)

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instSeqLeftOfAdd {T : Type u_1} [Add T] : SeqLeft (TimeM T)

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instSeqRightOfAdd {T : Type u_1} [Add T] : SeqRight (TimeM T)

@[instance_reducible]

instance Cslib.Algorithms.Lean.TimeM.instMonadOfAddZero {T : Type u_1} [AddZero T] : Monad (TimeM T)

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_pure {T : Type u_1} {α : Type u_2} [Zero T] (a : α) : (pure a).ret = a

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_bind {T : Type u_1} {α β : Type u_2} [Add T] (m : TimeM T α) (f : α → TimeM T β) : (m >>= f).ret = (f m.ret).ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_map {T : Type u_1} {α β : Type u_2} (f : α → β) (x : TimeM T α) : (f <$> x).ret = f x.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_mapConst {T : Type u_1} {α β : Type u_2} (a : α) (x : TimeM T β) : (Functor.mapConst a x).ret = a

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_seqRight {T : Type u_1} {β α : Type u_2} (x : TimeM T α) (y : Unit → TimeM T β) [Add T] : (x *> y ()).ret = (y ()).ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_seqLeft {T : Type u_1} {β α : Type u_2} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) : (x <* y ()).ret = x.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_seq {T : Type u_1} {α β : Type u_2} [Add T] (f : TimeM T (α → β)) (x : Unit → TimeM T α) : (f <*> x ()).ret = f.ret (x ()).ret

theorem Cslib.Algorithms.Lean.TimeM.isMonadHom_pure_ret {T : Type u_1} [AddZero T] : IsMonadHom (TimeM T) Id fun {α : Type u_2} (x : TimeM T α) => pure x.ret

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_bind {T : Type u_1} {α β : Type u_2} [Add T] (m : TimeM T α) (f : α → TimeM T β) : (m >>= f).time = m.time + (f m.ret).time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_pure {T : Type u_1} {α : Type u_2} [Zero T] (a : α) : (pure a).time = 0

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_map {T : Type u_1} {α β : Type u_2} (f : α → β) (x : TimeM T α) : (f <$> x).time = x.time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_seqRight {T : Type u_1} {β α : Type u_2} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) : (x *> y ()).time = x.time + (y ()).time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_seqLeft {T : Type u_1} {β α : Type u_2} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) : (x <* y ()).time = x.time + (y ()).time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_seq {T : Type u_1} {α β : Type u_2} [Add T] (f : TimeM T (α → β)) (x : Unit → TimeM T α) : (f <*> x ()).time = f.time + (x ()).time

instance Cslib.Algorithms.Lean.TimeM.instLawfulMonad {T : Type u_1} [AddMonoid T] : LawfulMonad (TimeM T)

TimeM is lawful so long as addition in the cost is associative and absorbs zero.

def Cslib.Algorithms.Lean.TimeM.tick {T : Type u_1} (c : T) : TimeM T PUnit.{u_2 + 1}

Creates a TimeM computation with a time cost.

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_tick {T : Type u_1} (c : T) : (tick c).ret = ()

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_tick {T : Type u_1} (c : T) : (tick c).time = c

def Cslib.Algorithms.Lean.TimeM.«doElem✓[_]_» : Lean.ParserDescr

✓[c] x adds c ticks, then executes x.

def Cslib.Algorithms.Lean.TimeM.«doElem✓_» : Lean.ParserDescr

✓ x is a shorthand for ✓[1] x, which adds one tick and executes x.

def Cslib.Algorithms.Lean.TimeM.«term⟪_⟫» : Lean.ParserDescr

Notation for extracting the return value from a TimeM computation: ⟪tm⟫