Library AbstractWalk

AbstractWalk.v: An example of probabilistic termination

Related to Vacid0 example of Maze construction


Section Walk.

Abstraction 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) 

Variable Data Input Result: Type.

Variable dData : distr Data.

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.

The random choice of data terminates
Hypothesis d_term : mu dData (fun d => 1) == 1.

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.