Commit 9f0f0c19 authored by Nicola Botta's avatar Nicola Botta
Browse files

Adding example and memoisation.

parent d1f4e8b4
> module SequentialDecisionProblems.NaiveTheory
> import Data.Fin
> import Data.Vect
> import Isomorphism.Isomorphism
> -- infixr 7 <+>
> infixr 7 <++>
* Monadic sequential decision process:
> M : Type -> Type
......@@ -211,8 +217,37 @@ correct. With
> s4 = s3
* Example
** Memoisation
A type is finite if it is isomorphic to |Fin n| for some |n : Nat|:
> interface Finite t where
> card : Nat
> iso : Iso t (Fin card)
For finite types, we have a number of useful results, among others
> namespace Memoisation
If all states are finite, we can represent policies with policy tables
> PolicyTable : (t : Nat) -> Finite (X t) -> Type
> PolicyTable t fX = Vect (card {t = X t}) (DPair (X t) (Y t))
and policy sequences with sequences of policy tables
> data PolicyTableSeq : (t : Nat) -> (n : Nat) -> Type where
> Nil : {t : Nat} -> PolicyTableSeq t Z
> (::) : {t, n : Nat} -> {fX : Finite (X t)} -> PolicyTable t fX -> PolicyTableSeq (S t) n -> PolicyTableSeq t (S n)
> {-
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment