Incorporated pruning into simulation

Author: bwbush

analysis/markov/Linleios/Evolve.lean

@@ -129,6 +129,9 @@ def step {env : Environment} : List (State → Outcomes) :=
   [@certify env, @vote env]
 
 
+def prune (ε : Float) : Probabilities → Probabilities :=
+  HashMap.filter (fun _ p => p > ε)
+
 def evolve (transition : State → Outcomes) : Probabilities → Probabilities :=
   HashMap.fold
     (
@@ -145,13 +148,10 @@ def chain (transitions : List (State → Outcomes)) : Probabilities → Probabil
   | [] => id
   | (t :: ts) => chain ts ∘ evolve t
 
-def simulate (env : Environment) (start : Probabilities) : Nat → Probabilities
+def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat → Probabilities
 | 0     => start
-| n + 1 => let state' := chain (@step env) start
-           simulate env state' n
-
-def prune (ε : Float) : Probabilities → Probabilities :=
-  HashMap.filter (fun _ p => p > ε)
+| n + 1 => let state' := prune ε $ chain (@step env) start
+           simulate env state' ε n
 
 def totalProbability (states : Probabilities) : Probability :=
   states.values.sum

analysis/markov/Main.lean

@@ -5,11 +5,11 @@ import Linleios
 def env : Environment := makeEnvironment 0.05 0.95 0.90 600 0.75 1 4 7
 
 def s0 : Probabilities := default
-def sn := simulate env s0 2
+def sn := simulate env s0 1e-6 2
 def pn := totalProbability sn
 
 def main : IO Unit :=
   do
     let print {α : Type} [Repr α] (x : α) : IO Unit := IO.println (reprPrec x 0).pretty
-    print $ prune 0 sn
-    print pn
+    print sn
+    print $ 1 - pn