Fibonacci numbers: memoization using the state monad

The naive way of computing Fibonacci numbers is very inefficient because it recomputes the same values many times. We can use the state monad to store the values of the Fibonacci numbers we have already computed. This is a simple example of memoization.

We will also take a more complicated example: Catalan numbers. The Catalan numbers are a sequence of natural numbers that occur in various counting problems, often involving recursively defined objects. They satisfy the recurrence relation:

• $C_0 = 1`,
• $C_n = \sum_{i=1}^n C_{i-1} C_{n-i}$, for $n \geq 0.$

@[reducible, inline]

abbrev FibState : Type

Equations

• FibState = Std.HashMap Nat Nat

@[reducible, inline]

abbrev FibM (α : Type) : Type

Equations

• FibM = StateM FibState

def fib (n : Nat) : FibM Nat

Equations

• One or more equations did not get rendered due to their size.
• fib 0 = pure 1
• fib 1 = pure 1

Catalan numbers

@[reducible, inline]

abbrev Catalan.CatState : Type

Equations

• Catalan.CatState = Std.HashMap Lean.Name (Std.HashMap Nat Nat)

@[reducible, inline]

abbrev Catalan.CatM (α : Type) : Type

Equations

• Catalan.CatM = StateM Catalan.CatState

@[irreducible]

def Catalan.cat (n : Nat) : Catalan.CatM Nat

Equations

• One or more equations did not get rendered due to their size.
• Catalan.cat 0 = pure 1

@[reducible, inline]

abbrev CatalanSimple.CatState : Type

Equations

• CatalanSimple.CatState = Std.HashMap Nat Nat

@[reducible, inline]

abbrev CatalanSimple.CatM (α : Type) : Type

Equations

• CatalanSimple.CatM = StateM CatalanSimple.CatState

@[irreducible]

def CatalanSimple.cat (n : Nat) : CatalanSimple.CatM Nat

Equations

• One or more equations did not get rendered due to their size.
• CatalanSimple.cat 0 = pure 1

structure CatalanOps.CatState : Type

• memo : Std.HashMap Nat Nat
• natOps : Nat
• count : Nat

instance CatalanOps.instInhabitedCatState : Inhabited CatalanOps.CatState

Equations

• CatalanOps.instInhabitedCatState = { default := { memo := default, natOps := default, count := default } }

instance CatalanOps.instReprCatState : Repr CatalanOps.CatState

Equations

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

@[reducible, inline]

abbrev CatalanOps.CatM (α : Type) : Type

Equations

• CatalanOps.CatM = StateM CatalanOps.CatState

def CatalanOps.addOps (n : Nat := 1) : CatalanOps.CatM Unit

Equations

• CatalanOps.addOps n = modify fun (s : CatalanOps.CatState) => { memo := s.memo, natOps := s.natOps + n, count := s.count }

def CatalanOps.withCount {α : Type} (x : CatalanOps.CatM α) : CatalanOps.CatM α

Equations

• CatalanOps.withCount x = do modify fun (s : CatalanOps.CatState) => { memo := s.memo, natOps := s.natOps, count := s.count + 1 } x

@[irreducible]

def CatalanOps.cat (n : Nat) : CatalanOps.CatM Nat

Equations

• One or more equations did not get rendered due to their size.
• CatalanOps.cat 0 = pure 1

structure MyStateM (σ α : Type) : Type

• run : σ → α × σ

def MyStateM.pure {σ α : Type} (a : α) : MyStateM σ α

Equations

• MyStateM.pure a = { run := fun (s : σ) => (a, s) }

def MyStateM.bind {σ α β : Type} (x : MyStateM σ α) (f : α → MyStateM σ β) : MyStateM σ β

Equations

• x.bind f = { run := fun (s : σ) => match x.run s with | (a, s') => (f a).run s' }

instance MyStateM.instMonad {σ : Type} : Monad (MyStateM σ)

Equations

• MyStateM.instMonad = Monad.mk

def MyStateM.get {σ : Type} : MyStateM σ σ

Equations

• MyStateM.get = { run := fun (s : σ) => (s, s) }

def MyStateM.set {σ : Type} (s : σ) : MyStateM σ Unit

Equations

• MyStateM.set s = { run := fun (x : σ) => ((), s) }

def MyStateM.modify {σ : Type} (f : σ → σ) : MyStateM σ Unit

Equations

• MyStateM.modify f = { run := fun (s : σ) => ((), f s) }

def MyStateM.run' {σ α : Type} (x : MyStateM σ α) (s : σ) : α

Equations

• x.run' s = match x.run s with | (a, snd) => a