structure MDPs.MDP : Type

Markov decision process

• S : ℕ

  states

• S_ne : 0 < self.S
• A : ℕ

  actions

• A_ne : 0 < self.A
• P : Fin self.S → Fin self.A → Findist.Δ self.S

  transition probability s, a, s'

• r : Fin self.S → Fin self.A → Fin self.S → ℝ

  reward function s, a, s'

inductive MDPs.Hist (M : MDP) : Type

Represents a history. The state is type ℕ and action is type ℕ.

• init {M : MDP} : Fin M.S → Hist M
• foll {M : MDP} : Hist M → Fin M.A → Fin M.S → Hist M

instance MDPs.instCoeFinSHist (M : MDP) : Coe (Fin M.S) (Hist M)

Coerces a state to a history

Equations

• MDPs.instCoeFinSHist M = { coe := fun (s : Fin M.S) => MDPs.Hist.init s }

@[reducible]

def MDPs.Hist.length (M : MDP) : Hist M → ℕ

The length of the history corresponds to the zero-based step of the decision

Equations

• MDPs.Hist.length M (MDPs.Hist.init a) = 0
• MDPs.Hist.length M (h.foll a a_1) = 1 + MDPs.Hist.length M h

@[reducible, inline]

abbrev MDPs.HistNE (m : MDP) : Type

Nonempty histories

Equations

• MDPs.HistNE m = { h : MDPs.Hist m // MDPs.Hist.length m h ≥ 1 }

def MDPs.Hist.last (M : MDP) : Hist M → Fin M.S

Returns the last state of the history

Equations

• MDPs.Hist.last M (MDPs.Hist.init a) = a
• MDPs.Hist.last M (h.foll a a_1) = a_1

def MDPs.Hist.append (M : MDP) (h : Hist M) (as : Fin M.A × Fin M.S) : Hist M

Appends the state and action to the history -

Equations

• MDPs.Hist.append M h as = h.foll as.1 as.2

def MDPs.Hist.one (M : MDP) (s₀ : Fin M.S) (a : Fin M.A) (s : Fin M.S) : Hist M

Equations

• MDPs.Hist.one M s₀ a s = (MDPs.Hist.init s₀).foll a s

def MDPs.Hist.prefix (M : MDP) (k : ℕ) (h : Hist M) : Hist M

Return the prefix of hist of length k

Equations

• MDPs.Hist.prefix M k (MDPs.Hist.init a) = MDPs.Hist.init a
• MDPs.Hist.prefix M k (h_1.foll a a_1) = if MDPs.Hist.length M h_1 + 1 ≤ k then h_1.foll a a_1 else MDPs.Hist.prefix M k h_1