Termination of a random walk
An example of probabilistic termination related to Vacid0 example of Maze construction.
Auteurs: Christine Paulin-Mohring
Catégories: Randomized Algorithms
Références: The VACID-0 Benchmarks
see also the index (by topic, by tool, by reference, by year)
AbstractWalk.v: An example of probabilistic termination
Related to Vacid0 example of Maze constructionAbstraction of maze scheme
If the process is not terminated then a random value is chosen in Data, under a certain condition on input and the data, the process is iterated on the same input, otherwise the input is changed. The change in the input decreases it strictly and the probability to stay with the same input is bounded by k<1, then the process terminates.
let rec iter u = if finished u then output u else let d = dData in if cond u d then iter u else iter (step d u)
Termination is taken using a measure on integer but could be generalized
to an arbitrary well-founded ordering
Variable size : Input -> nat.
Variable finished : Input -> bool.
Axiom finished_size : forall u, size u = O -> finished u = true.
Variable output : Input -> Result.
Variable cond : Input -> Data -> bool.
Variable step : Input -> Data -> Input.
When the process is not terminated, the probability to stay in the same state
is bounded by k<1
Variable k : U.
Hypothesis knot1 : k < 1.
Hypothesis d_true_bounded
: forall x, finished x = false -> mu dData (fun d => B2U (cond x d)) <= k.
Hypothesis knot1 : k < 1.
Hypothesis d_true_bounded
: forall x, finished x = false -> mu dData (fun d => B2U (cond x d)) <= k.
The random choice of data terminates
Hypothesis that the size decreases, when a step is taken
Hypothesis size_step : forall (u:Input) (x:Data),
finished u = false -> cond u x = false -> (size (step u x) < size u)%nat.
Lemma d_if_bound :
forall x, finished x = false -> forall a b, a <= b ->
k * a + [1-]k * b
<= mu dData (fun d => B2U (cond x d)) * a
+ mu dData (fun d => NB2U (cond x d)) * b.
Instance iter_mon :
monotonic
(fun (f:Input -> distr Result) (u:Input) =>
if (finished u) then Munit (output u)
else (Mlet dData
(fun d => if (cond u d) then (f u) else (f (step u d))))).
Save.
Lemma mu_if : forall A (b:bool) (dt de : distr A) (f:MF A),
mu (if b then dt else de) f = if b then (mu dt f) else (mu de f).
Definition Fiter : (Input -> distr Result) -m> (Input -> distr Result)
:= mon (fun (f:Input -> distr Result) (u:Input) =>
fif (finished u) (Munit (output u))
(Mlet dData
(fun d => fif (cond u d) (f u) (f (step u d))))).
Lemma Fiter_simpl : forall f u,
Fiter f u = fif (finished u) (Munit (output u))
(Mlet dData
(fun d => fif (cond u d) (f u) (f (step u d)))).
Lemma Fiter_cont : continuous Fiter.
Definition iter : Input -> distr Result := Mfix Fiter.
Lemma iter_eq : forall u:Input,
iter u == fif (finished u) (Munit (output u))
(Mlet dData (fun d => fif (cond u d) (iter u) (iter (step u d)))).
Hint Resolve iter_eq.
Building the invariant sequence
x is the size of the input and n the number of iterations:
pw x 0 = 0 pw 0 n = 1 pw (x+1) (n+1) = k (pw (x+1) n) + (1-k) (pw x n)
Fixpoint pw_ (x n : nat) : U :=
match n with O => 0
| (S n) => match x with
O => 1
| S y => k * pw_ x n + ([1-] k) * pw_ y n
end
end.
Lemma pw_decrS_x : forall n x, pw_ (S x) n <= pw_ x n.
Hint Resolve pw_decrS_x.
Lemma pw_decr_x : forall n x y, (x <= y)%nat -> pw_ y n <= pw_ x n.
Hint Resolve pw_decr_x.
Lemma pw_incr : forall x n, pw_ x n <= pw_ x (S n).
Hint Resolve pw_incr.
Definition pw : nat -> nat -m> U
:= fun x => fnatO_intro (pw_ x) (pw_incr x).
Lemma pw_pw_ : forall x n, pw x n = pw_ x n.
Lemma pw_simpl : forall x n, pw x n =
match n with O => 0
| (S n) => match x with
O => 1
| S y => k * pw x n + ([1-] k) * pw y n
end
end.
Lemma pwS_simpl : forall x n, pw (S x) (S n) = k * pw (S x) n + [1-]k * (pw x n).
Lemma lim_pw_one : forall x, lub (pw x) == 1.
Lemma iter_term : forall u, 1 <= mu (iter u) (fun r => 1).
End Walk.