Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

We want to implement expected running time analysis in Isabelle/HOL based on Kaminski et al. [9]. They present semantics and proof rules to analyse the expected running time of probabilistic guarded command language (pGCL) programs. pGCL is an interesting programming language as it admits probabilistic and non-deterministic choice, as well as unbounded while loops [12].

Following [9], in Sect. 3 we formalise two running time semantics for pGCL and show their equivalence: a denotational one expressed as expectation transformer of type , and a operational one defining a Markov decision process (MDP). This proof follows the equivalence proof of pGCL semantics on the expectation of program variables in [4] derived from the pen-and-paper proof by Gretz et al. [3].

Based on these formalisations we analyse the simple symmetric random walk, and show that the expected running time is infinite. We started with the proof provided in [9], but we discovered a flaw in the proof of the lower \(\omega \)-invariant based on the denotational semantics. Now, our solution combines results from the probability measure of the operational semantics and the fixed point solution from the denotational semantics.

Both proofs are based on our formalisation of Markov chains and MDPs [4]. The formalisation in this paper is on BitBucketFootnote 1.

2 Preliminaries

The formulas in this paper are oriented on Isabelle’s syntax: type annotations are written , type variables can be annotated with type classes (i.e. t has type \(\tau \) which is in type class tc), and type constructors are written in post-fix notation: e.g. . We write int for integers, ennreal for extended non-negative real numbers: \([0, \infty ]\), \(\alpha \) stream for infinite streams of \(\alpha \), \(\alpha \) pmf for probability mass functions (i.e. discrete distributions) on \(\alpha \). The state space is usually the type variable \(\sigma \). On infinite streams sdrop \(n\,\,\omega \) drops the first n elements from the stream \(\omega \): and .

Least Fixed Points. A central tool to define semantics are least fixed points on complete lattices: , bool, enat, and ennreal. Least fixed points are defined as . For a monotone function f, we get the equations . Fixed point theory also gives nice algebraic rules: the rolling rule “rolls” a composed fixed point: for monotone f and g, and the diagonal rule for nested fixed points: , for f monotone in both arguments.

To use least fixed points in measure theory, countable approximations are necessary. This is possible if the function f is sup-continuous: \(f\,(\bigsqcup _i C\,i) = \bigsqcup _i f\,(C\,i)\) for all chains C. Then f is monotone and . For our proofs we also need an induction and a transfer ruleFootnote 2:

figure a

Markov Chains (MCs) and Markov Decision Processes (MDPs). An overview of Isabelle’s MC and MDP theory is found in [4, 5]. A MC is defined by a transition function , inducing an expectation: is the expectation of f over all traces in K starting in s. A MDP is defined by a transition function , inducing the maximal expectation: is the supremum of all expectation of f over all traces in K starting in s. Both expectations and have values in ennreal, which is a complete lattice. Both are sup-continuous on measurable functions (called monotone convergent in measure theory), which allows us to apply the transfer rule when f is defined as a least fixed point. Also both expectations support an iteration rule, i.e. we can compute them by first taking a step in K and then continue in the resulting state t:

figure b

Where \(t\cdot \omega \) is the stream constructor and \(\int f\mathsf {d}D\) is the integral over the pmf D.

3 Probabilistic Guarded Command Language (pGCL)

The probabilistic guarded command language (pGCL) is a simple programming language allowing probabilistic assignment, non-deterministic choice and arbitrary While-loops. A thorough description of it using the weakest pre-expectation transformer (wp) semantics is found in McIver and Morgan [12]. Gretz et al. [3] shows the equivalence of wp with a operational semantics based on MDPs. Hurd et al. [8] and Cock [2] provide a shallow embedding of pGCL in HOL4 and Isabelle/HOL. We follow the definition in Kaminski et al. [9].

Fig. 1.
figure 1

pGCL syntax

Full size image
Fig. 2.
figure 2

Expectation transformer semantics for pGCL running times

Full size image

In Fig. 1 we define a datatype representing pGCL programs over an arbitrary program state of type \(\sigma \). Empty has not running time. Halt immediately aborts the program. Seq is for sequential composition. Par is for non-deterministic choice, i.e. both commands are executed and then one of the results is chosen. Assign, If, and While have the expected behaviour, and all three commands require one time step. A probabilistic choice is possible with Assign u, where u is a probabilistic state transformer (). The expected running time of Assign u weights each possible running time with the outcome of u. The assignment is deterministic is u is a Dirac distribution, i.e. assigning probability 1 to exactly one value. We need the datatype to have a deep embedding of pGCL programs, which is necessary for the construction of the MDP.

Fig. 3.
figure 3

MDP semantics for pGCL running times

Full size image

Expected Running Time. The denotational semantics for the running time is given as an expectation transformer, which is similar to the denotational semantics for the expectation of program variables as weakest pre-expectation transformers. Again we follow the definition in Kaminski et al. [9]. In Fig. 2 we define the expectation transformer ert taking a pGCL command c and an expectation f, where f assigns an expected running time to each terminal state of c. This gives a simple recursive definition of the Seq case, for the expected running time of a pGCL program we will set \(f = 0\). We proved some validating theorems about expectation transformer ert, i.e. continuity and monotonicity of ert c, closed under constant addition for Halt-free programs, sub-additivitiy, etc.

MDP Semantics. For the operational small-step semantics we introduce a MDP constructed per pGCL program, and compute the expected number of steps until the program terminates. In Fig. 3 we define the MDP by its transition function K and the per-state cost function cost f c s x. The per-state cost cost f c s x computes the running time cost associated with the program c at state s. Here the program is seen as a list of statements, hence we walk along a list of Seq and only look at its left-most leaf. If the program is Empty the MDP is stopped and we return f s containing further running time cost we want to associated to a finished state s (in most cases this will be 0, but it is essential in the induction case of Theorem 1). When the execution continues we also add x, c.f. the definition of .

The transition function K induces now a set of trace spaces, one for each possible resolution of the non-deterministic choices introduced by Par. We write \(\hat{\mathbb {E}}^{K}_{(c, s)}[f]\) for the maximal expectation of when the MDP starts in (c, s). We define the cost of a trace as the sum of cost over all states in the trace:

figure c

Finally the maximal expectation of computes ert:

Theorem 1

Proof

(Induction on c). The interesting cases are Seq and While. For Seq we prove the equation , by fixed point induction in both directions. For While we prove

figure d

by equating it to a completely unrolled version using fixed point induction and then massaging it in the right form using the rolling and diagonal rules.    \(\square \)

4 Simple Symmetric Random Walk

As an application for the expected running time analysis Kaminski et al. [9] chose the simple random walk. As difference to [9] we do not use \(\omega \)-invariants to prove the infinite running time, but the correspondence of the program with a Markov chain (there is no non-deterministic choice).

The simple symmetric random walk (srw) is a Markov chain on \(\mathbb {Z}\), in each step i it goes uniformly to \(i + 1\) or \(i - 1\) (i.e. in both cases with probability 1 / 2). Surprisingly, but well known (and formalised by Hurd [7]), it reaches each point with probability 1. Equally surprising, the expected time for the srw to go from i to \(i + 1\) is infinite! Kaminski et al. [9] prove this by providing a lower \(\omega \)-invariant. Unfortunately, this proof has a flaw: in Appendix B.1 of [10] (the extended version of [9]), the equation \(1 + \llbracket x> 0 \rrbracket \cdot 2 + \llbracket 1< x \le n + 1 \rrbracket \cdot \infty + \llbracket 0< x \le n - 1 \rrbracket \cdot \infty = 1 + \llbracket x > 0 \rrbracket \cdot 2 + \llbracket 0 < x \le n + 1 \rrbracket \cdot \infty \) does not hold for \(n=0\) and \(x=1\). The author knows from private communication with Kaminski et al. that it still is possible to use a lower \(\omega \)-invariant. Unfortunately, the necessary invariant gets much more complicated.

After discovering the flaw in the proof, we tried a more traditional proof. The usual approach in random walk theory uses the generating function of the first hitting time. Unfortunately, this would require quite some formalizations in combinatorics, e.g. Stirling numbers and more theorems about generating functions than available in [4]. Finally, we choose an approach similar to [7], i.e. we set up a linear equation system and prove that the only solution is infinity.

Now, is the transition function for the simple symmetric random walk. The expected time to reach j when started in i is written , where is the first hitting time. Now we need to prove the following rules: (I) if , (II) , (III) and (VI) . From these rules we can derive \(H~i~j = \infty \) for \(i \not = j\).

Rule (VI) is derived the expectation transformer semantics. But it is not clear to us how to prove rule (I) by only applying fixed point transformations or induction. Instead we prove (I) in a measure theoretic way:

$$\begin{aligned} H~j~k + H~k~i&= \mathbb {E}^{\mathsf {srw}}_j[f~j + H~k~i] \nonumber \\&= \sum _n (n + H~k~i)\cdot \Pr _j(f~k = n) \end{aligned}$$
(1)
$$\begin{aligned}&= {\sum _n \mathbb {E}^{\mathsf {srw}}_j[\lambda \omega .~(n + f~i~(\mathsf {sdrop}~n~\omega )) \cdot \llbracket f~k~\omega = n\rrbracket ]} \nonumber \\&= {\sum _n \mathbb {E}^{\mathsf {srw}}_j[f~i]} = H~j~i \end{aligned}$$
(2)

Equation 1 requires that f k is finite with probability 1, we do a case distinction: if it is not finite a.e. the result follows from \(H~j~i \ge H~j~k = \infty \). Equation 2 is now simply proved by induction on n. The proofs for Eqs. 1 and 2 essentially operate on each trace \(\omega \) in our probability space, making them inherently dependent on the trace space.

Theorem 2

(The running time of srw is infinite). \( H~i~j = \infty ~\text {if}~i \not = j. \)

Fig. 4.
figure 4

The Coupon Collector in pGCL and its refinement

Full size image

5 Coupon Collector

Another example we formalised is the coupon collector example from [9]. The idea is to compute the expected time until we collect N different coupons from a uniform, independent and infinite source of coupons. The left side of Fig. 4 shows our concrete implementation \(\mathtt {CC}_N\), the right side is its refinement (there is no array cp necessary). By fixed point transformations we show that the (refined) inner loop’s running time has a Geometric distribution, and hence the expected running time for \(\mathtt {CC}_N\) is: for \(N>0\).

6 Related Work

The first formalisation of probabilistic programs was by Hurd [7] in hol98, formalising a trace space for a stream of probabilistic bits. Hurd et al. [8] is different approach, formalising the weakest pre-expectation transformer semantics of pGCL in HOL4. Both formalisations are not related. Audebaud and Paulin-Mohring [1] use a shallow embedding of a probability monad in Coq.

Cock [2] provides a VCG for pGCL in Isabelle/HOL. Hölzl and Nipkow [5, 6] formalises MCs and analyses the expected running time of the ZeroConf protocol. On the basis of [5] formalises MDPs and shows the equivalence of the weakest pre-expectation transformer (based on the pen-and-paper proof in [3]).

Unlike Theorem 1, these formalisations either define denotational semantics [1, 2, 8], or operational semantics [5–7], none of them relate both semantics.

7 Conclusion and Future Work

While formalising the random walk example in [9] we found an essential flaw in the proof in [10]. Our solution seams to indicate, that for the verification of expected running times an \(\omega \)-invariant approach is not enough. While the expectation transformer gives us a nice verification condition generator (e.g. [2]), the trace space might be required to get additional information i.e. fairness and termination. The equivalence between the expectation transformer semantics and the MDP semantics provides the required bridge between both worlds. Also we might require a probabilistic, relational Hoare logic (maybe based on [11]) to automate tasks like Fig. 4.