TimeM: Time Complexity Monad

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

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 (α : Type u_1) : Type u_1

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

• ret : α

  The return value of the computation

• time : ℕ

  The accumulated time cost of the computation

def Cslib.Algorithms.Lean.TimeM.pure {α : Type u_1} (a : α) : TimeM α

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

Equations

• Cslib.Algorithms.Lean.TimeM.pure a = { ret := a, time := 0 }

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

Sequentially composes two TimeM computations, summing their time costs.

Equations

• m.bind f = { ret := (f m.ret).ret, time := m.time + (f m.ret).time }

instance Cslib.Algorithms.Lean.TimeM.instMonad : Monad TimeM

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Algorithms.Lean.TimeM.tick {α : Type u_1} (a : α) (c : ℕ := 1) : TimeM α

Creates a TimeM computation with a specified value and time cost. The time cost defaults to 1 if not provided.

Equations

• Cslib.Algorithms.Lean.TimeM.tick a c = { ret := a, time := c }

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

Notation for tick with explicit time cost: ✓ a, c

Equations

• One or more equations did not get rendered due to their size.

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

Notation for tick with default time cost of 1: ✓ a

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Algorithms.Lean.TimeM.tickUnit : TimeM Unit

A unit computation with time cost 1.

Equations

• Cslib.Algorithms.Lean.TimeM.tickUnit = Cslib.Algorithms.Lean.TimeM.tick ()

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_of_pure {α : Type u_1} (a : α) : (pure a).time = 0

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_of_bind {α : Type u_1} {β : Type u_2} (m : TimeM α) (f : α → TimeM β) : (m.bind f).time = m.time + (f m.ret).time

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.time_of_tick {α : Type u_1} (a : α) (c : ℕ) : (tick a c).time = c

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_bind {α : Type u_1} {β : Type u_2} (m : TimeM α) (f : α → TimeM β) : (m.bind f).ret = (f m.ret).ret