2735 lines
57 KiB
Text
2735 lines
57 KiB
Text
arXiv:2007.06327v1 [cs.LO] 13 Jul 2020
|
||
|
||
Generating Functions for Probabilistic
|
||
Programs⋆
|
||
Lutz Klinkenberg1[0000−0002−3812−0572] , Kevin Batz1[0000−0001−8705−2564] ,
|
||
Benjamin Lucien Kaminski1,2[0000−0001−5185−2324] , Joost-Pieter
|
||
Katoen1[0000−0002−6143−1926] , Joshua Moerman1[0000−0001−9819−8374] , and
|
||
Tobias Winkler1[0000−0003−1084−6408]
|
||
1
|
||
|
||
RWTH Aachen University, 52062 Aachen, Germany
|
||
2
|
||
University College London, United Kingdom
|
||
{lutz.klinkenberg, kevin.batz, benjamin.kaminski, katoen, joshua,
|
||
tobias.winkler}@cs.rwth-aachen.de
|
||
|
||
Abstract. This paper investigates the usage of generating functions
|
||
(GFs) encoding measures over the program variables for reasoning about
|
||
discrete probabilistic programs. To that end, we define a denotational
|
||
GF-transformer semantics for probabilistic while-programs, and show
|
||
that it instantiates Kozen’s seminal distribution transformer semantics.
|
||
We then study the effective usage of GFs for program analysis. We show
|
||
that finitely expressible GFs enable checking super-invariants by means
|
||
of computer algebra tools, and that they can be used to determine termination probabilities. The paper concludes by characterizing a class of
|
||
— possibly infinite-state — programs whose semantics is a rational GF
|
||
encoding a discrete phase-type distribution.
|
||
Keywords: probabilistic programs · quantitative verification · semantics · formal power series.
|
||
|
||
1
|
||
|
||
Introduction
|
||
|
||
Probabilistic programs are sequential programs for which coin flipping is a firstclass citizen. They are used e.g. to represent randomized algorithms, probabilistic
|
||
graphical models such as Bayesian networks, cognitive models, or security protocols. Although probabilistic programs are typically rather small, their analysis
|
||
is intricate. For instance, approximating expected values of program variables at
|
||
program termination is as hard as the universal halting problem [15]. Determining higher moments such as variances is even harder. Deductive program verification techniques based on a quantitative version of weakest preconditions [18]
|
||
enable to reason about the outcomes of probabilistic programs, such as what is
|
||
the probability that a program variable equals a certain value. Dedicated analysis techniques have been developed to e.g., determine tail bounds [6], decide
|
||
almost-sure termination [19,8], or to compare programs [1].
|
||
⋆
|
||
|
||
This research was funded by the ERC AdG project FRAPPANT (787914) and the
|
||
DFG RTG 2236 UnRAVeL.
|
||
|
||
2
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
This paper aims at exploiting the well-tried potential of probability generating
|
||
functions (PGFs [14]) for the analysis of probabilistic programs. In our setting,
|
||
PGFs are power series representations — generating functions — encoding discrete probability mass functions of joint distributions over program variables.
|
||
PGF representations — in particular if finite — enable a simple extraction of
|
||
important information from the encoded distributions such as expected values,
|
||
higher moments, termination probabilities or stochastic independence of program variables.
|
||
To enable the usage of PGFs for program analysis, we define a denotational semantics of a simple probabilistic while-language akin to probabilistic
|
||
GCL [18]. Our semantics is defined in a forward manner: given an input distribution over program variables as a PGF, it yields a PGF representing the resulting subdistribution. The “missing” probability mass represents the probability
|
||
of non-termination. More accurately, our denotational semantics transforms formal power series (FPS). Those form a richer class than PGFs, which allows for
|
||
overapproximations of probability distributions. While-loops are given semantics
|
||
as least fixed points of FPS transformers. It is shown that our semantics is in
|
||
fact an instantiation of Kozen’s seminal distribution-transformer semantics [16].
|
||
The semantics provides a sound basis for program analysis using PGFs. Using
|
||
Park’s Lemma, we obtain a simple technique to prove whether a given FPS overapproximates a program’s semantics i.e., whether an FPS is a so-called superinvariant. Such upper bounds can be quite useful: for almost-surely terminating
|
||
programs, such bounds can provide exact program semantics, whereas, if the
|
||
mass of an overapproximation is strictly less than one, the program is provably
|
||
non-almost-surely terminating. This result is illustrated on a non-trivial random
|
||
walk and on examples illustrating that checking whether an FPS is a superinvariant can be automated using computer algebra tools.
|
||
In addition, we characterize a class of — possibly infinite-state — programs
|
||
whose PGF semantics is a rational function. These homogeneous bounded programs (HB programs) are characterized by loops in which each unbounded variable has no effect on the loop guard and is in each loop iteration incremented by
|
||
a quantity independent of its own value. Operationally speaking, HB programs
|
||
can be considered as finite-state Markov chains with rewards in which rewards
|
||
can grow unboundedly large. It is shown that the rational PGF of any program that is equivalent to an almost-surely terminating HB program represents
|
||
a multi-variate discrete phase-type distribution [22]. We illustrate this result by
|
||
obtaining a closed-form characterization for the well-studied infinite-state dueling cowboys example [18].
|
||
Related work. Semantics of probabilistic programs is a well-studied topic. This
|
||
includes the seminal works by Kozen [16] and McIver and Morgan [18]. Other
|
||
related semantics of discrete probabilistic while-programs are e.g., given in several other articles like [18,24,10,23,4]. PGFs have recent scant attention in the
|
||
analysis of probabilistic programs. A notable exception is [5] in which generating
|
||
functions of finite Markov chains are obtained by Padé approximation. Computer
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
3
|
||
|
||
algebra systems have been used to transform probabilistic programs [7], and more
|
||
recently in the automated generation of moment-based loop invariants [2].
|
||
Organization of this paper. After recapping FPSs and PGFs in Sections 2–3,
|
||
we define our FPS transformer semantics in Section 4, discuss some elementary properties and show it instantiates Kozen’s distribution transformer semantics [16]. Section 5 presents our approach for verifying upper bounds to
|
||
loop invariants and illustrates this by various non-trivial examples. In addition,
|
||
it characterizes programs that are representable as finite-state Markov chains
|
||
equipped with rewards and presents the relation to discrete phase-type distributions. Section 6 concludes the paper. All proofs can be found in the appendix.
|
||
|
||
2
|
||
|
||
Formal Power Series
|
||
|
||
Our goal is to make the potential of probability generating functions available
|
||
to the formal verification of probabilistic programs. The programs we consider
|
||
will, without loss of generality, operate on a fixed set of k program variables.
|
||
The valuations of those variables range over N. A program state σ is hence a
|
||
vector in Nk . We denote the state (0, . . . , 0) by 0.
|
||
A prerequisite for understanding probability generating functions are (multivariate) formal power series — a special way of representing a potentially infinite
|
||
k-dimensional array. For k=1, this amounts to representing a sequence.
|
||
Definition 1 (Formal Power Series). Let X = X1 , . . . , Xk be a fixed sequence of k distinct formal indeterminates. For a state σ = (σ1 , . . . , σk ) ∈ Nk ,
|
||
let Xσ abbreviate the formal multiplication X1σ1 · · · Xkσk . The latter object is
|
||
called a monomial and we denote the set of all monomials over X by Mon (X).
|
||
A (multivariate) formal power series (FPS) is a formal sum
|
||
X
|
||
[σ]F · Xσ ,
|
||
where
|
||
[ · ]F : N k → R ∞
|
||
F =
|
||
≥0 ,
|
||
σ∈Nk
|
||
|
||
R∞
|
||
≥0
|
||
|
||
where
|
||
denotes the extended positive real line. We denote the set of all FPSs
|
||
by FPS. Let F, G ∈ FPS. If [σ]F < ∞ for all σ ∈ Nk , we denote this fact
|
||
by F ≪ ∞. The addition F + G and scaling r · F by a scalar r ∈ R∞
|
||
≥0 is
|
||
defined coefficient-wise by
|
||
X
|
||
X
|
||
|
||
F +G =
|
||
[σ]F + [σ]G · Xσ
|
||
r · [σ]F · Xσ .
|
||
and
|
||
r·F =
|
||
σ∈Nk
|
||
|
||
σ∈Nk
|
||
|
||
For states σ = (σ1 , . . . , σk ) and τ = (τ1 , . . . , τk ), we define σ + τ = (σ1 +
|
||
τ1 , . . . , σk + τk ). The multiplication F · G is given as their Cauchy product (or
|
||
discrete convolution)
|
||
X
|
||
[σ]F · [τ ]G · Xσ+τ .
|
||
F ·G =
|
||
σ,τ ∈Nk
|
||
|
||
Drawing coefficients from the extended reals enables us to define a complete lattice on FPSs in Section 4. Our analyses in Section 5 will, however, only consider
|
||
FPSs with F ≪ ∞.
|
||
|
||
4
|
||
|
||
3
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Generating Functions
|
||
A generating function is a device somewhat similar to a bag. Instead of
|
||
carrying many little objects detachedly, which could be embarrassing, we
|
||
put them all in a bag, and then we have only one object to carry, the bag.
|
||
— George Pólya [25]
|
||
|
||
Formal power series pose merely a particular way of encoding an infinite kdimensional array as yet another infinitary object, but we still carry all objects
|
||
forming the array (the coefficients of the FPS) detachedly and there seems to
|
||
be no advantage in this particular encoding. It even seems more bulky. We will
|
||
now, however, see that this bulky encoding can be turned into a one-object bag
|
||
carrying all our objects: the generating function.
|
||
Definition 2 (Generating
|
||
Functions). The generating function of a formal
|
||
P
|
||
power series F = σ∈Nk [σ]F · Xσ ∈ FPS with F ≪ ∞ is defined as the partial
|
||
function
|
||
f:
|
||
|
||
[0, 1]k 99K R≥0 ,
|
||
|
||
(x1 , . . . , xk ) 7→
|
||
|
||
X
|
||
|
||
[σ]F · xσ1 1 · · · xσk k .
|
||
|
||
σ=(σ1 ,...,σk )∈Nk
|
||
|
||
In other words: in order to turn an FPS into its generating function, we merely
|
||
treat every formal indeterminate Xi as an “actual” indeterminate xi , and the
|
||
formal multiplications and the formal sum also as “actual” ones. The generating
|
||
function f of F is uniquely determined by F as we require all coefficients of
|
||
F to be non-negative, and so the ordering of the summands is irrelevant: For
|
||
a given point x ∈ [0, 1]k , the sum defining f (x) either converges absolutely to
|
||
some positive real or diverges absolutely to ∞. In the latter case, f is undefined
|
||
at x and hence f may indeed be partial.
|
||
Since generating functions stem from formal power series, they are infinitely
|
||
often differentiable at 0 = (0, . . . , 0). Because of that, we can recover F from f
|
||
as the (multivariate) Taylor expansion of f at 0.
|
||
Definition 3 (Multivariate Derivatives and Taylor Expansions). For
|
||
σ = (σ1 , . . . , σk ) ∈ Nk , we write f (σ) for the function f differentiated σ1 times
|
||
in x1 , σ2 times in x2 , and so on. If f is infinitely often differentiable at 0, then
|
||
the Taylor expansion of f at 0 is given by
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
f (σ) ( 0 )
|
||
· xσ1 · · · xσk k .
|
||
σ1 ! · · · σk ! 1
|
||
|
||
If we replace every indeterminate xi by the formal indeterminate Xi in the
|
||
Taylor expansion of generating function f of F , then we obtain the formal power
|
||
series F . It is in precisely that sense, that f generates F .
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
5
|
||
|
||
Example 1 (Formal Power Series and Generating Functions). Consider the infinite (1-dimensional) sequence 1/2, 1/4, 1/8, 1/16, . . .. Its (univariate) FPS — the
|
||
entity carrying all coefficients detachedly — is given as
|
||
1
|
||
1
|
||
1
|
||
1
|
||
1
|
||
1
|
||
1 1
|
||
+ X + X2 + X3 + X4 + X5 +
|
||
X6 +
|
||
X7 + . . . .
|
||
2 4
|
||
8
|
||
16
|
||
32
|
||
64
|
||
128
|
||
256
|
||
|
||
(†)
|
||
|
||
On the other hand, its generating function — the bag — is given concisely by
|
||
1
|
||
.
|
||
2−x
|
||
|
||
(♭)
|
||
|
||
Figuratively speaking, (†) is itself the infinite sequence an := 21n , whereas (♭) is a
|
||
bag with the label “infinite sequence an := 21n ”. The fact that (†) generates (♭),
|
||
1
|
||
at 0 being 21 + 41 x + 18 x2 + . . ..
|
||
△
|
||
follows from the Taylor expansion of 2−x
|
||
The potential of generating functions is that manipulations to the functions —
|
||
i.e. to the concise representations — are in a one-to-one correspondence to the
|
||
associated manipulations to FPSs [9]. For instance, if f (x) is the generating
|
||
function of F encoding the sequence a1 , a2 , a3 , . . ., then the function f (x) · x is
|
||
the generating function of F · X which encodes the sequence 0, a1 , a2 , a3 , . . .
|
||
As another example for correspondence between operations on FPSs and
|
||
generating functions, if f (x) and g(x) are the generating functions of F and G,
|
||
respectively, then f (x) + g(x) is the generating function of F + G.
|
||
Example 2 (Manipulating to Generating Functions). Revisiting Example 1, if
|
||
1
|
||
we multiply 2−x
|
||
by x, we change the label on our bag from “infinite sequence
|
||
1
|
||
:= 21n ” and — just by
|
||
:=
|
||
an
|
||
2n ” to “a 0 followed by an infinite sequence an+1
|
||
changing the label — the bag will now contain what it says on its label. Indeed,
|
||
1 4
|
||
x
|
||
at 0 is 0 + 21 x + 41 x2 + 18 x3 + 16
|
||
x + . . . encoding
|
||
the Taylor expansion of 2−x
|
||
the sequence 0, 1/2, 1/4, 1/8, 1/16, . . .
|
||
△
|
||
Due to the close correspondence of FPSs and generating functions [9], we use
|
||
both concepts interchangeably, as is common in most mathematical literature.
|
||
We mostly use FPSs for definitions and semantics, and generating functions in
|
||
calculations and examples.
|
||
Probability Generating Functions. We now use formal power series to represent probability distributions.
|
||
Definition 4 (Probability Subdistribution). A probability subdistribution
|
||
(or simply subdistribution) over Nk is a function
|
||
X
|
||
µ : Nk → [0, 1],
|
||
such that
|
||
|µ| =
|
||
µ(σ) ≤ 1 .
|
||
σ∈Nk
|
||
|
||
We call |µ| the mass of µ. We say that µ is a (full) distribution if |µ| = 1,
|
||
and a proper subdistribution if |µ| < 1. The set of all subdistributions on Nk is
|
||
denoted by D≤ (Nk ) and the set of all full distributions by D(Nk ).
|
||
|
||
6
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
We need subdistributions for capturing non-termination. The “missing” probability mass 1 − |µ| precisely models the probability of non-termination.
|
||
The generating function of a (sub-)distribution is called a probability generating function. Many properties of a distribution µ can be read off from its
|
||
generating function Gµ in a simple way. We demonstrate how to extract a few
|
||
common properties in the following example.
|
||
Example 3 (Geometric Distribution PGF). Recall Example 1. The presented formal power series encodes a geometric distribution µgeo with parameter 1/2 of a
|
||
single variable X. The fact that µgeo is a proper probability distribution, for
|
||
1
|
||
= 1. The expected
|
||
instance, can easily be verified computing Ggeo (1) = 2−1
|
||
1
|
||
′
|
||
△
|
||
value of X is given by Ggeo (1) = (2−1)2 = 1.
|
||
Extracting Common Properties. Important information about probability
|
||
distributions is, for instance, the first and higher moments. In general, the k th
|
||
factorial moment of variable Xi can be extracted from a PGF by computing
|
||
∂kG
|
||
(1, . . . , 1).3 This includes the mass |G| as the 0th moment. The marginal dis∂Xik
|
||
tribution of variable Xi can simply be extracted from G by G(1, . . . , Xi , . . . , 1).
|
||
We also note that PGFs can treat stochastic independence. For instance, for a
|
||
bivariate PGF H we can check for stochastic independence of the variables X
|
||
and Y by checking whether H(X, Y ) = H(X, 1) · H(1, Y ).
|
||
|
||
4
|
||
|
||
FPS Semantics for pGCL
|
||
|
||
In this section, we give denotational semantics to probabilistic programs in terms
|
||
of FPS transformers and establish some elementary properties useful for program
|
||
analysis. We begin by endowing FPSs and PGFs with an order structure:
|
||
Definition 5 (Order on FPS). For all F, G ∈ FPS, let
|
||
F G
|
||
|
||
iff
|
||
|
||
∀ σ ∈ Nk :
|
||
|
||
[σ]G ≤ [σ]F .
|
||
|
||
Lemma 1 (Completeness of on FPS). (FPS, ) is a complete latttice.
|
||
4.1
|
||
|
||
FPS Transformer Semantics
|
||
|
||
Recall that we assume programs to range over exactly k variables with valuations
|
||
in Nk . Our program syntax is similar to Kozen [16] and McIver & Morgan [18].
|
||
Definition 6 (Syntax of pGCL [16,18]). A program P in probabilistic Guarded
|
||
Command Language ( pGCL) adheres to the grammar
|
||
P ::= skip
|
||
|
||
xi := E
|
||
|
||
P;P
|
||
|
||
if(B) {P } else {P }
|
||
3
|
||
|
||
{P } [p] {P }
|
||
|
||
while (B) {P } ,
|
||
|
||
In general, one must take the limit Xi → 1 from below.
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
7
|
||
|
||
where xi ∈ {x1 , . . . , xk } is a program variable, E is an arithmetic expression over
|
||
program variables, p ∈ [0, 1] is a probability, and B is a predicate (called guard)
|
||
over program variables.
|
||
The FPS semantics of pGCL will be defined in a forward denotational style,
|
||
where the program variables x1 , . . . , xk correspond to the formal indeterminates
|
||
X1 , . . . , Xk of FPSs.
|
||
For handling assignments, if-conditionals and while-loops, we need some
|
||
auxiliary functions on FPSs: For an arithmetic expression E over program variables, we denote by evalσ (E) the evaluation of E in program state σ. For a
|
||
predicate B ⊆ Nk and FPS F , we define the restriction of F to B by
|
||
X
|
||
hF iB :=
|
||
[σ]F · Xσ ,
|
||
σ∈B
|
||
|
||
i.e. hF iB is the FPS obtained from F by setting all coefficients [σ]F where σ 6∈ B
|
||
to 0. Using these prerequisites, our FPS transformer semantics is given as follows:
|
||
Definition 7 (FPS Semantics of pGCL). The semantics JP K : FPS → FPS of
|
||
a loop-free pGCL program P is given according to the upper part of Table 1.
|
||
The unfolding operator ΦB,P for the loop while (B) {P } is defined by
|
||
ΦB,P :
|
||
|
||
(FPS → FPS) → (FPS → FPS),
|
||
|
||
|
||
|
||
ψ 7→ λF . hF i¬B + ψ JP K hF iB .
|
||
|
||
|
||
The partial order (FPS, ) extends to a partial order FPS → FPS, ⊑ on FPS
|
||
transformers by a point-wise lifting of . The least element of this partial order is
|
||
the transformer 0 = λF . 0 mapping any FPS F to the zero series. The semantics
|
||
of while (B) {P } is then given by the least fixed point (with respect to ⊑) of its
|
||
unfolding operator, i.e.
|
||
Jwhile (B) {P }K = lfp ΦB,P .
|
||
|
||
Table 1. FPS transformer semantics of pGCL programs.
|
||
P
|
||
|
||
JP K (F )
|
||
|
||
skip
|
||
xi := E
|
||
|
||
F
|
||
P
|
||
|
||
{P1 } [p] {P2 }
|
||
if (B) {P1 } else {P2 }
|
||
P1 # P2
|
||
while(B){P }
|
||
|
||
evalσ (E)
|
||
|
||
σ∈Nk
|
||
|
||
µσ X1σ1 · · · Xi
|
||
|
||
· · · Xkσk
|
||
|
||
p · JP1 K (F ) + (1 − p) · JP2 K (F )
|
||
|
||
|
||
+ JP2 K hF i¬B
|
||
|
||
JP2 K JP1 K (F )
|
||
|
||
JP1 K hF iB
|
||
|
||
|
||
lfp ΦB,P (F ) ,
|
||
|
||
for
|
||
|
||
|
||
|
||
ΦB,P (ψ) = λF . hF i¬B + ψ JP K hF iB
|
||
|
||
8
|
||
|
||
(( G
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Example 4. Consider the program P = {x := 0} [1/2] {x := 1}# c := c + 1 and
|
||
the input PGF G = 1, which denotes a point mass on state σ = 0. Using the
|
||
annotation style shown in the left margin, denoting that JP ′ K (G) = G′ , we
|
||
calculate JP K (G) as follows:
|
||
|
||
P′
|
||
(( G′
|
||
|
||
(( 1
|
||
{x := 0} [1/2] {x := 1}#
|
||
((
|
||
|
||
1
|
||
2
|
||
|
||
+
|
||
|
||
X
|
||
2
|
||
|
||
c := c + 1
|
||
(( C2 + CX
|
||
2
|
||
As for the semantics of c := c + 1, see Table 2.
|
||
|
||
△
|
||
|
||
Before we study how our FPS transformers behave on PGFs in particular, we
|
||
now first argue that our FPS semantics is well-defined. While evident for loopfree programs, we appeal to the Kleene Fixed Point Theorem for loops [17],
|
||
which requires ω-continuous functions.
|
||
Theorem 1 (ω-continuity of pGCL Semantics). The semantic functional J · K
|
||
is ω-continuous, i.e. for all programs P ∈ pGCL and all increasing ω-chains
|
||
F1 F2 . . . in FPS,
|
||
|
||
|
||
= sup JP K (Fn ) .
|
||
JP K sup Fn
|
||
n∈N
|
||
|
||
n∈N
|
||
|
||
Theorem 2 (Well-definedness of FPS Semantics). The semantics functional J · K is well-defined, i.e. the semantics of any loop while (B) {P } exists
|
||
uniquely and can be written as
|
||
Jwhile (B) {P }K = lfp ΦB,P = sup ΦnB,P (0) .
|
||
n∈N
|
||
|
||
4.2
|
||
|
||
Healthiness Conditions of FPS Transformers
|
||
|
||
In this section we show basic, yet important, properties which follow from [16].
|
||
For instance, for any input FPS F , the semantics of a program cannot yield as
|
||
output an FPS with a mass larger than |F |, i.e. programs cannot create mass.
|
||
Table 2. Common assignments and their effects on the input PGF F (X, Y ).
|
||
P
|
||
|
||
JP K (F )
|
||
|
||
x := x + k
|
||
x := k · x
|
||
|
||
X k · F (X, Y )
|
||
|
||
x := x + y
|
||
|
||
F (X, XY )
|
||
|
||
F (X k , Y )
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
9
|
||
|
||
Theorem 3 (Mass Conservation). For every P ∈ pGCL and F ∈ FPS, we
|
||
have JP K (F ) ≤ |F |.
|
||
|
||
A program P is called mass conserving if |JP K (F )| = |F | for all F ∈ FPS. Mass
|
||
conservation has important implications for FPS transformers acting on PGFs:
|
||
given as input a PGF, the semantics of a program yields a PGF.
|
||
|
||
Corollary 1 (PGF Transformers). For every P ∈ pGCL and G ∈ PGF, we
|
||
have JP K (G) ∈ PGF.
|
||
|
||
Restricted to PGF, our semantics hence acts as a subdistribution transformer.
|
||
Output masses may be smaller than input masses. The probability of nontermination of the programs is captured by the “missing” probability mass.
|
||
As observed in [16], semantics of probabilistic programs are fully defined by
|
||
their effects on point masses, thus rendering probabilistic program semantics
|
||
linear. In our setting, this generalizes to linearity of our FPS transformers.
|
||
Definition 8 (Linearity). Let F, G ∈ FPS and r ∈ R∞
|
||
≥0 be a scalar. The function ψ : FPS → FPS is called a linear transformer (or simply linear), if
|
||
ψ(r · F + G) = r · ψ(F ) + ψ(G) .
|
||
Theorem 4 (Linearity of pGCL Semantics). For every program P and
|
||
guard B, the functions h · iB and JP K are linear. Moreover, the unfolding operator ΦB,P maps linear transformers onto linear transformers.
|
||
As a final remark, we can unroll while loops:
|
||
Lemma 2 (Loop Unrolling). For any FPS F ,
|
||
Jwhile (B) {P }K (F ) = hF i¬B + Jwhile (B) {P }K JP K hF iB
|
||
4.3
|
||
|
||
Embedding into Kozen’s Semantics Framework
|
||
|
||
|
||
|
||
.
|
||
|
||
Kozen [16] defines a generic way of giving distribution transformer semantics
|
||
based on an abstract measurable space (X n , M (n) ). Our FPS semantics instantiates his generic semantics. The state space we consider is Nk , so that (Nk , P(Nk ))
|
||
is our measurable space.4 A measure on that space is a countably-additive function µ : P(Nk ) → [0, ∞] with µ(∅) = 0. We denote the set of all measures on our
|
||
space by M. Although, we represent measures by FPSs, the two notions are in
|
||
bijective correspondence τ : FPS → M, given by
|
||
X
|
||
τ (F ) = λS.
|
||
[σ]F .
|
||
σ∈S
|
||
|
||
This map preserves the linear structure and the order .
|
||
Kozen’s syntax [16] is slightly different from pGCL. We compensate for this by
|
||
a translation function T, which maps pGCL programs to Kozen’s. The following
|
||
theorem shows that our semantics agrees with Kozen’s semantics.5
|
||
4
|
||
|
||
5
|
||
|
||
We note that we want each point σ to be measurable, which enforces a discrete
|
||
measurable space.
|
||
Note that Kozen regards a program P itself as a function P : M → M.
|
||
|
||
10
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Theorem 5. The FPS semantics of pGCL is an instance of Kozen’s semantics,
|
||
i.e. for all pGCL programs P , we have
|
||
τ ◦ JP K = T(P ) ◦ τ .
|
||
Equivalently, the following diagram commutes:
|
||
FPS
|
||
|
||
τ
|
||
|
||
M
|
||
|
||
JP K
|
||
|
||
T(P )
|
||
|
||
FPS
|
||
|
||
M
|
||
|
||
τ
|
||
|
||
For more details about the connection between FPSs and measures, as well as
|
||
more information about the actual translation, see Appendix A.3.
|
||
|
||
5
|
||
|
||
Analysis of Probabilistic Programs
|
||
|
||
Our PGF semantics enables the representation of the effect of a pGCL program on
|
||
a given PGF. As a next step, we investigate to what extent a program analysis
|
||
can exploit such PGF representations. To that end, we consider the overapproximation with loop invariants (Section 5.1) and provide examples showing that
|
||
checking whether an FPS transformer overapproximates a loop can be checked
|
||
with computer algebra tools. In addition, we determine a subclass of pGCL programs whose effect on an arbitrary input state is ensured to be a rational PGF
|
||
encoding a phase-type distribution (Section 5.2).
|
||
5.1
|
||
|
||
Invariant-style Overapproximation of Loops
|
||
|
||
In this section, we seek to overapproximate loop semantics, i.e. for a given loop
|
||
W = while (B) {P }, we want to find a (preferably simple) FPS transformer ψ,
|
||
such that JW K ⊑ ψ, meaning that for any input G, we have JW K (G) ψ(G)
|
||
(cf. Definition 7). Notably, even if G is a PGF, we do not require ψ(G) to be
|
||
one. Instead, ψ(G) can have a mass larger than one. This is fine, because it still
|
||
overapproximates the actual semantics coefficient-wise. Such overapproximations
|
||
immediately carry over to reading off expected values (cf. Section 3), for instance
|
||
∂
|
||
∂X
|
||
|
||
JW K (G) (1)
|
||
|
||
≤
|
||
|
||
∂
|
||
∂X ψ(G)(1)
|
||
|
||
.
|
||
|
||
We use invariant-style reasoning for verifying that a given ψ overapproximates
|
||
the semantics of JW K. For that, we introduce the notion of a superinvariant and
|
||
employ Park’s Lemma, a well-known concept from fixed point theory, to obtain
|
||
a conceptually simple proof rule for verifying overapproximations of while loops.
|
||
Theorem 6 (Superinvariants and Loop Overapproximations). Let ΦB,P
|
||
be the unfolding operator of while(B){P } (cf. Def. 7) and ψ : FPS → FPS. Then
|
||
ΦB,P (ψ) ⊑ ψ
|
||
|
||
implies
|
||
|
||
Jwhile (B) {P }K ⊑ ψ .
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
11
|
||
|
||
We call a ψ satisfying ΦB,P (ψ) ⊑ ψ a superinvariant. We are interested in linear
|
||
superinvariants, as our semantics is also linear (cf. Theorem 4). Furthermore,
|
||
linearity allows to define ψ solely in terms of its effect on monomials, which
|
||
makes reasoning considerably simpler:
|
||
Corollary 2. Given a function f : Mon (X) → FPS, let the linear extension fˆ
|
||
of f be defined by
|
||
X
|
||
[σ]F f (Xσ ) .
|
||
fˆ: FPS → FPS, F 7→
|
||
σ∈Nk
|
||
|
||
Let ΦB,P be the unfolding operator of while (B) {P }. Then
|
||
∀ σ ∈ Nk :
|
||
|
||
ΦB,P (fˆ)(Xσ ) ⊑ fˆ(Xσ )
|
||
|
||
implies
|
||
|
||
Jwhile (B) {P }K ⊑ fˆ .
|
||
|
||
We call an f satisfying the premise of the above corollary a superinvariantlet. Notice that superinvariantlets and their extensions agree on monomials, i.e.
|
||
f (Xσ ) = fˆ(Xσ ). Let us examine a few examples for superinvariantlet-reasoning.
|
||
Example 5 (Verifying Precise Semantics). In Program 1.1, in each iteration, a
|
||
fair coin flip determines the value of x. Subsequently, c is incremented by 1.
|
||
Consider the following superinvariantlet:
|
||
(
|
||
C
|
||
, if i = 1;
|
||
f (X i C j ) = C j · 2−C
|
||
X i,
|
||
if i 6= 1.
|
||
To verify that f is indeed a superinvariantlet, we have to show that
|
||
|
||
ΦB,P (fˆ)(X i C j ) = X i C j x6=1 + fˆ JP K X i C j x=1
|
||
!
|
||
|
||
⊑ fˆ X i C j
|
||
|
||
For i 6= 1, we get
|
||
ΦB,P (fˆ)(X i C j ) =
|
||
|
||
X iC j
|
||
|
||
|
||
|
||
.
|
||
|
||
x6=1
|
||
|
||
+ fˆ(JP K (0))
|
||
|
||
= X i C j = f (X i C j ) = fˆ(X i C j ) .
|
||
For i = 1, we get
|
||
ΦB,P (fˆ)(X 1 C j ) = fˆ
|
||
=
|
||
=
|
||
|
||
1 0 j+1
|
||
+ 12 X 1 C j+1
|
||
2X C
|
||
|
||
|
||
0 j+1
|
||
1
|
||
+ 21 f X 1 C j+1
|
||
2f X C
|
||
|
||
|
||
1 j
|
||
C j+1
|
||
= fˆ X 1 C j
|
||
2−C = f X C
|
||
|
||
|
||
|
||
(by linearity of fˆ)
|
||
. (by definition of f )
|
||
|
||
C
|
||
.
|
||
Hence, Corollary 2 yields JW K (X) ⊑ f (X) = 2−C
|
||
For this example, we can state even more. As the program is almost surely
|
||
terminating, and f (X i C j ) = 1 for all (i, j) ∈ N2 , we conclude that fˆ is exactly
|
||
the semantics of W , i.e. fˆ = JW K.
|
||
△
|
||
|
||
12
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
while ( x = 1 ) {
|
||
{x := 0} [ 1/2 ] {x := 1}#
|
||
c := c + 1
|
||
}
|
||
Program 1.1. Geometric distribution generator.
|
||
|
||
while ( x > 0 ) {
|
||
{x := x + 1} [ 1/2 ] {x := x - 1}#
|
||
c := c + 1
|
||
}
|
||
Program 1.2. Left-bounded 1-dimensional random walk.
|
||
|
||
Example 6 (Verifying Proper Overapproximations). Program 1.2 models a one
|
||
dimensional, left-bounded random walk. Given an input (i, j) ∈ N2 , it is evident
|
||
that this program can only terminate in an even (if i is even) or odd (if i
|
||
is odd) number of steps. This information can be encoded into the following
|
||
superinvariantlet:
|
||
f (X 0 C j ) = C j
|
||
f (X i+1 C j ) = C j ·
|
||
|
||
and
|
||
(
|
||
|
||
C
|
||
1−C 2 ,
|
||
1
|
||
1−C 2 ,
|
||
|
||
if i is odd;
|
||
if i is even.
|
||
|
||
It is straightforward to verify that f is a proper superinvariantlet (proper because
|
||
C
|
||
3
|
||
5
|
||
1−C 2 = C + C + C + . . . is not a PGF) and hence f properly overapproximates
|
||
the loop semantics. Another superinvariantlet for Program 1.2 is given by
|
||
√
|
||
|
||
1− 1−C 2 i
|
||
, if i ≥ 1;
|
||
i j
|
||
j
|
||
C
|
||
h(X C ) = C ·
|
||
1,
|
||
if i = 0.
|
||
Given that the program terminates almost-surely [11] and that h is a superinvariantlet yielding only PGFs, it follows that the extension of h is exactly the
|
||
semantics of Program 1.2. An alternative derivation of this formula for the case
|
||
h(X) can be found, e.g., in [12].
|
||
For both f and h, we were able to prove that they are indeed superinvariantlets automatically, using the computer algebra library SymPy [20]. The code
|
||
is included in Appendix B (Program 1.5).
|
||
△
|
||
|
||
Example 7 (Proving Non-almost-sure Termination). In Program 1.3, the branching probability of the choice statement depends on the value of a program variable. This notation is just syntactic sugar, as this behavior can be mimicked by
|
||
loop constructs together with coin flips [3, pp. 115f].
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
13
|
||
|
||
while ( x > 0 ) {
|
||
{x := x - 1} [ 1/x ] {x := x + 1}
|
||
}
|
||
Program 1.3. A non-almost-surely terminating loop.
|
||
|
||
while ( x < 1 and t < 2 ) {
|
||
if ( t = 0 ) {
|
||
{x := 1} [ a ] {t := 1}# c := c + 1
|
||
} else {
|
||
{x := 1} [ b ] {t := 0}# d := d + 1
|
||
}
|
||
}
|
||
Program 1.4. Dueling cowboys.
|
||
|
||
To prove that Program 1.3 does not terminate almost-surely, we consider the
|
||
following superinvariantlet:
|
||
f (X i ) = 1 −
|
||
|
||
i−2
|
||
1 X 1
|
||
·
|
||
,
|
||
e n=0 n!
|
||
|
||
where e = 2.71828 . . . is Euler’s number.
|
||
|
||
Again, the superinvariantlet property was verified automatically, here
|
||
using2Math1
|
||
1
|
||
ematica [13]. Now, consider for instance f (X 3 ) = 1 − 1e · 0!
|
||
+ 1!
|
||
= 1 − e < 1.
|
||
This proves, that the program terminates on X 3 with a probability strictly
|
||
smaller than 1, witnessing that the program is not almost surely terminating. △
|
||
5.2
|
||
|
||
Rational PGFs
|
||
|
||
In several of the examples from the previous sections, we considered PGFs which
|
||
were rational functions, that is, fractions of two polynomials. Since those are a
|
||
particularly simple class of PGFs, it is natural to ask which programs have
|
||
rational semantics. In this section, we present a semantic characterization of a
|
||
class of while-loops whose output distribution is a (multivariate) discrete phasetype dsitribution [21,22]. This implies that the resulting PGF of such programs
|
||
is an effectively computable rational function for any given input state. Let us
|
||
illustrate this by an example.
|
||
Example 8 (Dueling Cowboys). Program 1.4 models two dueling cowboys [18].
|
||
The hit chance of the first cowboy is a percent and the hit chance of the second
|
||
cowboy is b percent, where a, b ∈ [0, 1].6 The cowboys shoot at each other in
|
||
turns, as indicated by the variable t, until one of them gets hit (x is set to 1).
|
||
6
|
||
|
||
These are not program variables.
|
||
|
||
14
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
The variable c counts the number of shots of the first cowboy and d those of the
|
||
second cowboy.
|
||
We observe that Program 1.4 is somewhat independent of the value of c, in
|
||
the sense that moving the statement c := c + 1 to either immediately before
|
||
or after the loop, yields an equivalent program. In our notation, this is expressed
|
||
as JW K (C · H) = C · JW K (H) for all PGFs H. By symmetry, the same applies
|
||
to variable d. Unfolding the loop once on input 1, yields
|
||
JW K (1) = (1 − a)C · JW K (T ) + aCX .
|
||
A similar equation for JW K (T ) involving JW K (1) on its right-hand side holds.
|
||
This way we obtain a system of two linear equations, although the program itself
|
||
is infinite-state. The linear equation system has a unique solution JW K (1) in the
|
||
field of rational functions over the variables C, D, T , and X which is the PGF
|
||
G :=
|
||
|
||
aCX + (1 − a)bCDT X
|
||
.
|
||
1 − (1 − b)(1 − a)CD
|
||
|
||
From G we can easily read off the following: The probability that the first cowboy
|
||
a
|
||
, and the expected total number of
|
||
wins (x = 1 and t = 0) equals 1−(1−a)(1−b)
|
||
1
|
||
∂
|
||
G(1) = a+b−ab
|
||
. Notice that this quantity equals
|
||
shots of the first cowboy is ∂C
|
||
∞ if a and b are both zero, i.e. if both cowboys have zero hit chance.
|
||
If we write GV for the PGF obtained by substituting all but the variables in
|
||
V with 1, then we moreover see that GC · GD 6= GC,D . This means that C and
|
||
D (as random variables) are stochastically dependent.
|
||
△
|
||
|
||
The distribution encoded in the PGF JW K (1) is a discrete phase-type distribution. Such distributions are defined as follows: A Markov reward chain is a
|
||
Markov chain where each state is augmented with a reward vector in Nk . By definition, a (discrete) distribution on Nk is of phase-type iff it is the distribution of
|
||
the total accumulated reward vector until absorption in a Markov reward chain
|
||
with a single absorbing state and a finite number of transient states. In fact,
|
||
Program 1.4 can be described as a Markov reward chain with two states (X 0 T 0
|
||
and X 0 T 1 ) and 2-dimensional reward vectors corresponding to the “counters”
|
||
(c, d): the reward in state X 0 T 0 is (1, 0) and (0, 1) in the other state.
|
||
Each pGCL program describes a Markov reward chain [10]. It is not clear which
|
||
(non-trivial) syntactical restrictions to impose to guarantee for such chains to be
|
||
finite. In the remainder of this section, we give a characterization of while-loops
|
||
that are equivalent to finite Markov reward chains. The idea of our criterion is
|
||
that each variable has to fall into one of the following two categories:
|
||
Definition 9 (Homogeneous and Bounded Variables). Let P ∈ pGCL be a
|
||
program, B be a guard and xi be a program variable. Then:
|
||
– xi is called homogeneous for P if JP K (Xi ·G) = Xi ·JP K (G) for all G ∈ PGF.
|
||
– xi is called bounded by B if the set {σi | σ ∈ B} is finite.
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
15
|
||
|
||
Intuitively, homogeneity of xi means that it does not matter whether one increments the variable before or after the execution of P . Thus, a homogeneous
|
||
variable behaves like an increment-only counter even if this may not be explicit
|
||
in the syntax. In Example 8, the variables c and d in Program 1.4 are homogeneous (for both the loop-body and the loop itself). Moreover, x and t are clearly
|
||
bounded by the loop guard. We can now state our characterization.
|
||
Definition 10 (HB Loops). A loop while (B) {P } is called homogeneousbounded (HB) if for all program states σ ∈ B, the PGF JP K (Xσ ) is a polynomial
|
||
and for all program variables x it either holds that
|
||
– x is homogeneous for P and the guard B is independent of x, or that
|
||
– x is bounded by the guard B.
|
||
In an HB loop, all the possible valuations of the bounded variables satisfying B
|
||
span the finite transient state space of a Markov reward chain in which the
|
||
dimension of the reward vectors equals the number of homogeneous variables.
|
||
The additional condition that JP K (Xσ ) is a polynomial ensures that there is
|
||
only a finite amount of terminal (absorbing) states. Thus, we have the following:
|
||
Proposition 1. Let W be a while-loop. Then JW K (Xσ ) is the (rational) PGF
|
||
of a multivariate discrete phase-type distribution if and only if W is equivalent
|
||
to an HB loop that almost-surely terminates on input σ.
|
||
To conclude, we remark that there are various simple syntactic conditions for
|
||
HB loops: For example, if P is loop-free, then JP K (Xσ ) is always a polynomial.
|
||
Similarly, if x only appears in assignments of the form x := x + k, k ≥ 0, then
|
||
x is homogeneous. Such updates of variables are e.g. essential in constant probability programs [?]. The crucial point is that such conditions are only sufficient
|
||
but not necessary. Our semantic conditions thus capture the essence of phasetype distribution semantics more adequately while still being reasonably simple
|
||
(albeit — being non-trivial semantic properties — undecidable in general).
|
||
|
||
6
|
||
|
||
Conclusion
|
||
|
||
We have presented a denotational distribution transformer semantics for probabilistic while-programs where the denotations are generation functions (GFs).
|
||
Moreover, we have provided a simple invariant-style technique to prove that
|
||
a given GF overapproximates the program’s semantics and identified a class
|
||
of (possibly infinite-state) programs whose semantics is a rational GF ecoding a
|
||
phase-type distribution. Directions for future work include the (semi-)automated
|
||
synthesis of invariants and the development of notions on how precise overapproximations by invariants actually are.
|
||
|
||
|
||
|
||
A
|
||
|
||
Proofs of Section 4
|
||
|
||
A.1
|
||
|
||
Proofs of Section 4.1
|
||
|
||
Lemma 1 (Completeness of on FPS). (FPS, ) is a complete latttice.
|
||
Proof. We start by showing that (FPS, ) is a partial order. Let F, G, H ∈ FPS,
|
||
σ ∈ Nk . For reflexivity, consider the following:
|
||
G G
|
||
|
||
∀σ ∈ Nk : [σ]G ≤ [σ]G
|
||
|
||
iff
|
||
iff
|
||
|
||
true .
|
||
|
||
For antisymmetry, consider the following:
|
||
|
||
implies
|
||
implies
|
||
implies
|
||
|
||
G H and H G
|
||
|
||
∀σ ∈ Nk : [σ]G ≤ [σ]H
|
||
|
||
and
|
||
|
||
[σ]H ≤ [σ]G
|
||
|
||
and
|
||
|
||
[σ]H ≤ [σ]F
|
||
|
||
k
|
||
|
||
∀σ ∈ N : [σ]G = [σ]H
|
||
G = H .
|
||
|
||
For transitivity, consider the following:
|
||
|
||
implies
|
||
implies
|
||
implies
|
||
|
||
G H
|
||
k
|
||
|
||
and H F
|
||
|
||
∀σ ∈ N : [σ]G ≤ [σ]H
|
||
k
|
||
|
||
∀σ ∈ N : [σ]G ≤ [σ]F
|
||
G F .
|
||
|
||
Next, we show that every set S ⊆ FPS has a supremum
|
||
X
|
||
sup [σ]F Xσ
|
||
sup S =
|
||
σ∈Nk
|
||
|
||
F ∈S
|
||
|
||
P
|
||
in FPS. In particular, notice that sup ∅ = σ∈Nk 0 · Xσ . The fact that sup S ∈
|
||
k
|
||
FPS is trivial since supF ∈S [σ]F ∈ R∞
|
||
≥0 for every σ ∈ N . Furthermore, the fact
|
||
that sup S is an upper bound on S is immediate since is defined coefficientwise. Finally, sup S is also the least upper bound, since, by definition of , we
|
||
have [σ]sup S = supF ∈S [σ]F .
|
||
The following proofs rely on the Monotone Sequence Theorem (MST), which
|
||
we recall here: If (an )n∈N is a monotonically increasing sequence in R∞
|
||
≥0 , then
|
||
supn an = limn→∞ an . In particular, if (an )n∈N and (bn )n∈N are monotonically
|
||
increasing sequences in R∞
|
||
≥0 , then
|
||
sup an + sup bn =
|
||
n
|
||
|
||
n
|
||
|
||
lim an + lim bn =
|
||
|
||
n→∞
|
||
|
||
n→∞
|
||
|
||
lim an + bn = sup an + bn .
|
||
|
||
n→∞
|
||
|
||
n
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
19
|
||
|
||
Theorem 1 (ω-continuity of pGCL Semantics). The semantic functional J · K
|
||
is ω-continuous, i.e. for all programs P ∈ pGCL and all increasing ω-chains
|
||
F1 F2 . . . in FPS,
|
||
JP K
|
||
|
||
|
||
|
||
sup Fn
|
||
n∈N
|
||
|
||
|
||
|
||
= sup JP K (Fn ) .
|
||
n∈N
|
||
|
||
Proof. By induction on the structure of P . Let S = {F1 , F2 , . . .} be an increasing
|
||
ω-chain in FPS. First, we consider the base cases.
|
||
The case P = skip. We have
|
||
JP K (sup S) = sup S = sup {F } = sup {JP K (F )} .
|
||
F ∈S
|
||
|
||
F ∈S
|
||
|
||
P
|
||
The case P = xi := E. Let sup S = Ĝ = σ∈Nk [σ]Ĝ · X σ , where for each σ ∈ Nk
|
||
we have [σ]Ĝ = supF ∈S [σ]F . We calculate
|
||
JP K (sup S)
|
||
|
||
= JP K Ĝ
|
||
|
||
|
||
X
|
||
= JP K
|
||
[σ]Ĝ · X σ
|
||
σ∈Nk
|
||
|
||
|
||
|
||
|
||
|
||
= JP K
|
||
|
||
X
|
||
|
||
[σ]Ĝ · X1σ1 · · · Xiσi · · · Xkσk
|
||
|
||
= JP K
|
||
|
||
X
|
||
|
||
[σ]Ĝ · X1σ1 · · · Xiσi · · · Xkσk
|
||
|
||
σ∈Nk
|
||
|
||
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
= sup
|
||
F ∈S
|
||
|
||
sup [σ]F
|
||
|
||
F ∈S
|
||
|
||
X
|
||
|
||
· · · Xkσk
|
||
|
||
evalσ (E)
|
||
|
||
· X1σ1 · · · Xi
|
||
|
||
evalσ (E)
|
||
|
||
σ∈Nk
|
||
|
||
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
= sup JP K (F )
|
||
F ∈S
|
||
|
||
|
||
|
||
[σ]F · X1σ1 · · · Xi
|
||
|
||
= sup JP K
|
||
F ∈S
|
||
|
||
evalσ (E)
|
||
|
||
[σ]Ĝ · X1σ1 · · · Xi
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
|
||
|
||
· · · Xkσk
|
||
|
||
· · · Xkσk
|
||
|
||
(sup on FPS is defined coefficient–wise)
|
||
|
||
|
||
[σ]F · X1σ1 · · · Xiσi · · · Xkσk
|
||
|
||
20
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
As the induction hypothesis now assume that for some arbitrary, but fixed,
|
||
programs P1 , P2 and all increasing ω-chains S1 , S2 in FPS it holds that both
|
||
JP1 K (sup S1 ) =
|
||
|
||
sup JP1 K (F )
|
||
|
||
and
|
||
|
||
F ∈S1
|
||
|
||
JP2 K (sup S2 ) =
|
||
|
||
sup JP2 K (F ) .
|
||
|
||
F ∈S2
|
||
|
||
We continue with the induction step.
|
||
The case P = {P1 } [p] {P2 }. We have
|
||
JP K (sup S)
|
||
= p · JP1 K (sup S) + (1 − p) · JP2 K (sup S)
|
||
|
||
|
||
|
||
|
||
= p · sup JP1 K (F ) + (1 − p) · sup JP2 K (F )
|
||
F ∈S
|
||
F ∈S
|
||
|
||
|
||
|
||
=
|
||
sup p · JP1 K (F ) + sup (1 − p) · JP2 K (F )
|
||
F ∈S
|
||
|
||
(I.H. on P1 and P2 )
|
||
|
||
F ∈S
|
||
|
||
(scalar multiplication is defined point–wise)
|
||
|
||
= sup (p · JP1 K (F ) + (1 − p) · JP2 K (F ))
|
||
|
||
(apply MST coefficient–wise.)
|
||
|
||
F ∈S
|
||
|
||
= sup J{P1 } [p] {P2 }K (F )
|
||
F ∈S
|
||
|
||
= sup JP K (F ) .
|
||
F ∈S
|
||
|
||
The case P = if (B) {P1 } else {P2 }. We have
|
||
JP K (sup S)
|
||
= JP1 K (hsup SiB ) + JP2 K (hsup Si¬B )
|
||
|
||
|
||
|
||
|
||
|
||
|
||
= JP1 K sup hF iB
|
||
+ JP2 K sup hF i¬B
|
||
F ∈S
|
||
|
||
F ∈S
|
||
|
||
(restriction defined coefficient–wise)
|
||
|
||
= sup JP1 K (hF iB ) + sup JP2 K (hF i¬B )
|
||
F ∈S
|
||
|
||
F ∈S
|
||
|
||
= sup (JP1 K (hF iB ) + JP2 K (hF i¬B ))
|
||
|
||
(I.H. on P1 and P2 )
|
||
(apply MST coefficient–wise)
|
||
|
||
F ∈S
|
||
|
||
= sup Jif (B) {P1 } else {P2 }K (F )
|
||
F ∈S
|
||
|
||
= sup JP K (F ) .
|
||
F ∈S
|
||
|
||
The case P = while(B){P1 }. Recall that for every G ∈ FPS,
|
||
JP K (G) = (lfp ΦB,P1 ) (G)
|
||
|
||
= sup ΦnB,P1 (0) (G) .
|
||
n∈N
|
||
|
||
Hence, it suffices to show that
|
||
|
||
|
||
|
||
|
||
|
||
n
|
||
n
|
||
sup ΦB,P1 (0) (sup S) = sup
|
||
sup ΦB,P1 (0) (F ) .
|
||
n∈N
|
||
|
||
F ∈S
|
||
|
||
n∈N
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
21
|
||
|
||
Assume for the moment that for every n ∈ N and all increasing ω-chains S in
|
||
FPS,
|
||
|
||
|
||
ΦnB,P1 (0) (sup S) = sup ΦnB,P1 (0) (F ) .
|
||
(1)
|
||
F ∈S
|
||
|
||
We then have
|
||
|
||
|
||
sup ΦnB,P1 (0) (sup S)
|
||
n∈N
|
||
|
||
= sup ΦnB,P1 (0) (sup S)
|
||
n∈N
|
||
|
||
= sup sup ΦnB,P1 (0) (F )
|
||
n∈N F ∈S
|
||
|
||
= sup sup ΦnB,P1 (0) (F )
|
||
F ∈S n∈N
|
||
|
||
|
||
|
||
|
||
= sup
|
||
,
|
||
sup ΦnB,P1 (0) (F )
|
||
F ∈S
|
||
|
||
(sup for ΦB,P1 is defined point–wise)
|
||
(Equation 1)
|
||
(swap suprema)
|
||
(sup for ΦB,P1 is defined point–wise)
|
||
|
||
n∈N
|
||
|
||
which is what we have to show. It remains to prove Equation 1 by induction on n.
|
||
Base case n = 0. We have
|
||
|
||
|
||
Φ0B,P1 (0) (sup S) = sup S = sup F = sup Φ0B,P1 (0) (F ) .
|
||
F ∈S
|
||
|
||
F ∈S
|
||
|
||
Induction step. We have
|
||
|
||
|
||
Φn+1
|
||
B,P1 (0) (sup S)
|
||
|
||
= ΦB,P1 ΦnB,P1 (0) (sup S)
|
||
|
||
= hsup Si¬B + ΦnB,P1 (0) (JP1 K (hsup SiB ))
|
||
|
||
|
||
= hsup Si¬B + ΦnB,P1 (0) sup JP1 K (hF iB )
|
||
F ∈S
|
||
|
||
= hsup Si¬B + sup ΦnB,P1 (0) (JP1 K (hF iB ))
|
||
F ∈S
|
||
|
||
= sup hF i¬B + ΦnB,P1 (0) (JP1 K (hF iB ))
|
||
F ∈S
|
||
|
||
|
||
= sup Φn+1
|
||
B,P1 (0) (F ) .
|
||
F ∈S
|
||
|
||
(Def. of ΦB,P1 )
|
||
(I.H. on P1 )
|
||
(I.H. on n)
|
||
(apply MST)
|
||
(Def. of ΦB,P1 )
|
||
|
||
This completes the proof.
|
||
Theorem 2 (Well-definedness of FPS Semantics). The semantics functional J · K is well-defined, i.e. the semantics of any loop while (B) {P } exists
|
||
uniquely and can be written as
|
||
Jwhile (B) {P }K = lfp ΦB,P = sup ΦnB,P (0) .
|
||
n∈N
|
||
|
||
22
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Proof. First, we show that the unfolding operator ΦB,P is ω-continuous. For
|
||
that, let f1 ⊑ f2 ⊑ . . . be an ω-chain in FPS → FPS. Then,
|
||
ΦB,P
|
||
|
||
|
||
|
||
sup{fn }
|
||
|
||
n∈N
|
||
|
||
|
||
|
||
|
||
|
||
= λG. hGi¬B + sup{fn } (JP K (hGiB ))
|
||
n∈N
|
||
|
||
= λG. hGi¬B + sup{fn (JP K (hGiB ))}
|
||
n∈N
|
||
|
||
(sup on FPS → FPS is defined point–wise)
|
||
|
||
= sup {λG. hGi¬B + fn (JP K (hGiB ))}
|
||
n∈N
|
||
|
||
(apply monotone sequence theorem coefficient-wise)
|
||
= sup {ΦB,P (fn )} .
|
||
|
||
(Def. of ΦB,P )
|
||
|
||
n∈N
|
||
|
||
Since ΦB,P is ω-continuous and (FPS → FPS, ⊑) forms a complete lattice (Lemma 1),
|
||
we get by the Kleene fixed point Theorem [17] that ΦB,P has a unique least fixed
|
||
point given by supn∈N ΦnB,P (0).
|
||
Theorem 3 (Mass Conservation). For every P ∈ pGCL and F ∈ FPS, we
|
||
have JP K (F ) ≤ |F |.
|
||
Proof. By induction on the structure of P . For the loop–free cases, this is
|
||
straightforward. For the case P = while(B){P1 }, we proceed as follows. For
|
||
every r ∈ R∞
|
||
≥0 , we define the set
|
||
FPSr = {F ∈ FPS | |F | ≤ r}
|
||
of all FPSs whose mass is at most r. First, we define the restricted unfolding
|
||
operator
|
||
ΦB,P1 ,r : (FPSr → FPSr ) → (FPSr → FPSr ),
|
||
|
||
ψ 7→ ΦB,P1 (ψ) .
|
||
|
||
Our induction hypothesis on P1 implies that ΦB,P1 ,r is well–defined.
|
||
It is now only left to show that (FPSr , ) is an ω-complete partial order,
|
||
because then ΦB,P1 ,r has a least fixed point in FPSr for every r ∈ R∞
|
||
≥0 . The
|
||
theorem then follows by letting r = |G|, because
|
||
(lfp ΦB,P1 ) (G) =
|
||
|
||
|
||
lfp ΦB,P1 ,|G| (G)
|
||
|
||
implies
|
||
|
||
|(lfp ΦB,P1 ) (G)| ≤ |G| .
|
||
|
||
(FPSr , ) is an ω-complete partial order. The fact that (FPSr , ) is a partial
|
||
order is immediate. It remains to show ω-completeness. For that, let f1 f2
|
||
. . . be an ω-chain in FPSr . We have to show that supn Fn ∈ FPSr , which is the
|
||
case if and only if
|
||
X
|
||
sup fn =
|
||
sup [σ]fn ≤ r .
|
||
n
|
||
|
||
σ∈Nk
|
||
|
||
n
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
23
|
||
|
||
Now let g : N → Nk be some bijection from N to Nk . We have
|
||
X
|
||
|
||
=
|
||
|
||
sup [σ]fn
|
||
|
||
σ∈Nk
|
||
∞
|
||
X
|
||
|
||
n
|
||
|
||
(series converges absolutely)
|
||
|
||
sup [g(i)]fn
|
||
|
||
i=0
|
||
|
||
= sup
|
||
N
|
||
|
||
n
|
||
|
||
N
|
||
X
|
||
i=0
|
||
|
||
= sup sup
|
||
N
|
||
|
||
n
|
||
|
||
= sup sup
|
||
n
|
||
|
||
N
|
||
|
||
sup [g(i)]fn (rewrite infinite series as supremum of partial sums)
|
||
n
|
||
|
||
N
|
||
X
|
||
|
||
[g(i)]fn
|
||
|
||
(apply monotone sequence theorem)
|
||
|
||
[g(i)]fn
|
||
|
||
(swap suprema)
|
||
|
||
i=0
|
||
|
||
N
|
||
X
|
||
i=0
|
||
|
||
P
|
||
Now observe that supN N
|
||
i=0 [g(i)]fn = |fn |, which is a monotonically increasing
|
||
sequence in n. Moreover, since fn ∈ FPSr , this sequence is bounded from above
|
||
by r. Hence, the least upper bound supn |fn | of the sequence |fn | is no larger
|
||
than r, too. This completes the proof.
|
||
|
||
A.2
|
||
|
||
Proofs of Section 4.2
|
||
|
||
Lemma 3 (Representation of JwhileK). Let W = while (B) {P } be a pGCL
|
||
program. An alternative representation is:
|
||
|
||
JW K = λG.
|
||
|
||
∞
|
||
X
|
||
i=0
|
||
|
||
ϕi (G)
|
||
|
||
¬B
|
||
|
||
,
|
||
|
||
where ϕ(G) = JP K (hGiB ).
|
||
|
||
Proof. First we show by induction, that ΦnB,P (0)(G) =
|
||
Base case. We have
|
||
|
||
Φ0B,P (0)(G) = 0 =
|
||
|
||
−1
|
||
X
|
||
i=0
|
||
|
||
ϕi (G)
|
||
|
||
¬B
|
||
|
||
Pn−1
|
||
i=0
|
||
|
||
.
|
||
|
||
ϕi (G)
|
||
|
||
¬B
|
||
|
||
.
|
||
|
||
24
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Induction step. We have
|
||
|
||
n
|
||
Φn+1
|
||
B,P (0)(G) = ΦB,P ΦB,P (0)(G)
|
||
= hGi¬B + ΦnB,P (0)(JP K hGiB )
|
||
= hGi¬B + ΦnB,P (0)(ϕ(G))
|
||
n−1
|
||
X
|
||
|
||
= hGi¬B +
|
||
|
||
i=0
|
||
n
|
||
X
|
||
|
||
= hGi¬B +
|
||
=
|
||
|
||
n
|
||
X
|
||
|
||
ϕi (G)
|
||
|
||
JW K (G)
|
||
|
||
= sup ΦnB,P (0) (G)
|
||
n∈N
|
||
|
||
= sup ΦnB,P (0)(G)
|
||
n∈N
|
||
)
|
||
( n
|
||
X
|
||
i
|
||
= sup
|
||
ϕ (G) ¬B
|
||
n∈N
|
||
|
||
=
|
||
|
||
∞
|
||
X
|
||
i=0
|
||
|
||
ϕi
|
||
|
||
i=1
|
||
|
||
i=0
|
||
|
||
Overall, we thus get
|
||
|
||
ϕi+1
|
||
|
||
¬B
|
||
|
||
¬B
|
||
|
||
¬B
|
||
|
||
.
|
||
|
||
(sup on FPS → FPS is defined point–wise)
|
||
(see above)
|
||
|
||
i=0
|
||
|
||
ϕi (G)
|
||
|
||
¬B
|
||
|
||
Theorem 4 (Linearity of pGCL Semantics). For every program P and guard B,
|
||
the functions h · iB and JP K are linear. Moreover, the unfolding operator ΦB,P
|
||
maps linear transformers onto linear transformers.
|
||
Proof. Linearity of h·iB . We have
|
||
*
|
||
ha · G + F iB =
|
||
=
|
||
=
|
||
|
||
a·
|
||
|
||
*
|
||
|
||
σ∈Nk
|
||
|
||
X
|
||
|
||
X
|
||
|
||
σ∈B
|
||
|
||
=a·
|
||
|
||
µσ X σ +
|
||
|
||
(a · µσ + νσ ) X σ
|
||
|
||
(a · µσ + νσ )X
|
||
a · µσ X σ
|
||
|
||
X
|
||
|
||
X
|
||
|
||
µσ X
|
||
|
||
νσ X σ
|
||
|
||
σ∈Nk
|
||
|
||
σ∈Nk
|
||
|
||
X
|
||
|
||
σ∈B
|
||
|
||
=
|
||
|
||
X
|
||
|
||
σ
|
||
|
||
+
|
||
|
||
+
|
||
|
||
+
|
||
|
||
B
|
||
|
||
σ
|
||
|
||
X
|
||
|
||
νσ X σ
|
||
|
||
σ∈B
|
||
|
||
+
|
||
|
||
σ∈B
|
||
|
||
= a · hGiB + hF iB
|
||
|
||
X
|
||
|
||
σ∈B
|
||
|
||
νσ X σ
|
||
|
||
B
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
25
|
||
|
||
Linearity of JP K. By induction on the structure of P . First, we consider the
|
||
base cases.
|
||
The case P = skip. We have
|
||
JskipK (r · F + G) = r · F + G = r · JskipK (F ) + JskipK (G)
|
||
The case P = xi := E
|
||
JXi := EK (r · F + G)
|
||
X
|
||
eval (E)
|
||
· · · Xkσk
|
||
[σ]r·F +G X1σ1 · · · Xi σ
|
||
=
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
= r·
|
||
|
||
= r·
|
||
|
||
evalσ (E)
|
||
|
||
· · · Xkσk
|
||
|
||
evalσ (E)
|
||
|
||
· · · Xkσk
|
||
|
||
|
||
|
||
eval (E)
|
||
· · · Xi σ
|
||
|
||
· · · Xkσk
|
||
|
||
|
||
|
||
(r · [σ]F + [σ]G ) · X1σ1 · · · Xi
|
||
|
||
X
|
||
|
||
[σ]F · X1σ1 · · · Xi
|
||
|
||
X
|
||
|
||
X1σ1
|
||
|
||
σ∈Nk
|
||
|
||
σ∈Nk
|
||
|
||
+
|
||
|
||
[σ]F ·
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
evalσ (E)
|
||
|
||
[σ]G · X1σ1 · · · Xi
|
||
|
||
= r · JP K (F ) + JP K (G) .
|
||
|
||
(+ and · defined coefficient–wise)
|
||
|
||
|
||
eval (E)
|
||
· · · Xkσk
|
||
+ [σ]G · X1σ1 · · · Xi σ
|
||
(+ and · defined coefficient–wise)
|
||
|
||
· · · Xkσk
|
||
|
||
|
||
|
||
(+ and · defined coefficient–wise)
|
||
|
||
Next, we consider the induction step.
|
||
The case P = P1 ; P2 . We have
|
||
JP1 ; P2 K (r · F + G)
|
||
= JP2 K (JP1 K (r · F + G))
|
||
|
||
= JP2 K (r · JP1 K (F ) + JP1 K (G))
|
||
= r · JP2 K (JP1 K (F )) + JP2 K (JP1 K (G)) .
|
||
|
||
(I.H. on P1 )
|
||
(I.H. on P2 )
|
||
|
||
The case P = if (B) {P1 } else {P2 }. We have
|
||
Jif (B) {P1 } else {P2 }K (r · F + G)
|
||
|
||
= hJP1 K (r · F + G)iB + hJP2 K (r · F + G)i¬B
|
||
= hr · JP1 K (F ) + JP1 K (G))iB + hr · JP2 K (F ) + JP2 K (G)i¬B
|
||
(I.H. on P1 and P2 )
|
||
|
||
= r · hJP1 K (F )iB + hJP2 K (F )i¬B + hJP1 K (G)iB + hJP2 K (G)i¬B
|
||
(linearity of h·iB and h·i¬B )
|
||
= r · Jif (B) {P1 } else {P2 }K (F ) + Jif (B) {P1 } else {P2 }K (G)
|
||
|
||
26
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
The case P = {P1 } [p] {P2 }.
|
||
J{P1 } [p] {P2 }K (r · F + G)
|
||
|
||
= p · JP1 K (r · F + G) + (1 − p) · JP2 K (r · F + G)
|
||
|
||
= p · (r · JP1 K (F ) + JP1 K (G)) + (1 − p) · (r · JP2 K (F ) + JP2 K (G))
|
||
(I.H. on P1 and P2 )
|
||
= r · (p · JP1 K (F ) + (1 − p) · JP2 K (F )) + p · JP1 K (G) + (1 − p) · JP2 K (G)
|
||
(reorder terms)
|
||
|
||
= r · J{P1 } [p] {P2 }K (F ) + J{P1 } [p] {P2 }K
|
||
The case P = while (B) {P1 }.
|
||
Jwhile (B) {P1 }K (r · F + G)
|
||
|
||
= sup ΦnB,P1 (0) (r · F + G)
|
||
n∈N
|
||
|
||
= sup ΦnB,P1 (0)(r · F + G)
|
||
(sup on FPS → FPS defined point–wise)
|
||
n∈N
|
||
|
||
= sup r · ΦnB,P1 (0)(F ) + ΦnB,P1 (0)(G)
|
||
n∈N
|
||
|
||
(by straightforward induction on n using I.H. on P1 )
|
||
n
|
||
|
||
= r · sup ΦB,P1 (0)(F ) + sup ΦnB,P1 (0)(G)
|
||
n∈N
|
||
|
||
n∈N
|
||
|
||
(apply monotone sequence theorem coefficient–wise)
|
||
|
||
= r · Jwhile (B) {P1 }K (F ) + Jwhile (B) {P1 }K (G)
|
||
Linearity of ΦB,P (f ) for linear f .
|
||
*
|
||
|
||
+
|
||
X
|
||
X
|
||
ΦB,P (f )
|
||
µσ X σ =
|
||
µσ X σ
|
||
σ∈Nk
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
=
|
||
|
||
=
|
||
|
||
*
|
||
|
||
*
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
µσ X σ
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
µσ X σ
|
||
|
||
+
|
||
|
||
+
|
||
|
||
¬B
|
||
|
||
¬B
|
||
|
||
|
||
|
||
*
|
||
+
|
||
X
|
||
|
||
+ f JP K
|
||
µσ X σ
|
||
|
||
|
||
+f
|
||
+
|
||
|
||
¬B
|
||
|
||
σ∈Nk
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
B
|
||
|
||
|
||
|
||
µσ JP K (hX σ iB )
|
||
|
||
(1. & 2.)
|
||
|
||
µσ · f (JP K (hX σ iB ))
|
||
(f lin.)
|
||
|
||
µσ hX σ i¬B + µσ · f (JP K (hX σ iB ))
|
||
µσ · hX σ i¬B + f (JP K (hX σ iB ))
|
||
µσ · ΦB,P (f )(X σ )
|
||
|
||
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
27
|
||
|
||
Lemma 2 (Loop Unrolling). For any FPS F ,
|
||
Jwhile (B) {P }K (F ) = hF i¬B + Jwhile (B) {P }K JP K hF iB
|
||
Proof. Let W, W ′ be as described in Lemma 2.
|
||
|
||
|
||
|
||
.
|
||
|
||
JW K (G) = (lfp ΦB,P ) (G)
|
||
= ΦB,P (lfp ΦB,P ) (G)
|
||
= hGi¬B + (lfp ΦB,P ) JP K hGiB
|
||
|
||
|
||
|
||
= Jif (B) {P ; W } else {skip}K (G)
|
||
= JW ′ K (G)
|
||
|
||
A.3
|
||
|
||
Proofs of Section 4.3
|
||
|
||
Lemma 4. The mapping τ is a bijection. The inverse τ −1 of τ is given by
|
||
X
|
||
µ ({σ}) · Xσ
|
||
τ −1 : M → FPS, µ 7→
|
||
σ∈Nk
|
||
|
||
Proof. We show this by showing τ −1 ◦ τ = id and τ ◦ τ −1 = id.
|
||
|
||
|
||
!
|
||
X
|
||
X
|
||
−1
|
||
−1
|
||
σ
|
||
|
||
λN .
|
||
ασ
|
||
=τ
|
||
τ ◦τ
|
||
ασ X
|
||
σ∈N
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
X X
|
||
|
||
σ∈Nk s∈{σ}
|
||
|
||
|
||
|
||
τ ◦ τ −1 (µ) = τ
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
ασ · Xσ =
|
||
|
||
X
|
||
|
||
ασ Xσ
|
||
|
||
σ∈Nk
|
||
|
||
|
||
|
||
µ({σ}) · Xσ = λN .
|
||
|
||
X
|
||
|
||
µ({σ}) = µ(N ) = µ
|
||
|
||
σ∈N
|
||
|
||
Lemma 5. The mappings τ and τ −1 are monotone linear maps.
|
||
Proof. First, we show that τ −1 is linear (and hence τ , due to bijectivity):
|
||
X
|
||
(µ + ν)({σ}) · Xσ
|
||
τ −1 (µ + ν) =
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
X
|
||
|
||
(µ({σ}) + ν({σ})) · Xσ
|
||
|
||
X
|
||
|
||
(µ({σ}) · Xσ + ν({σ}) · Xσ )
|
||
|
||
σ∈Nk
|
||
|
||
=
|
||
|
||
σ∈Nk
|
||
|
||
|
||
|
||
=
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
(as M forms a vector space with standard +)
|
||
|
||
|
||
|
||
|
||
|
||
µ({σ}) · Xσ +
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
|
||
|
||
ν({σ}) · Xσ = τ −1 (µ) + τ −1 (ν)
|
||
|
||
28
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Second, we show that τ is monotone:
|
||
Assume Gµ ⊑ Gµ′ .
|
||
|
||
|
||
|
||
τ (Gµ ) = τ
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
≤ λS.
|
||
|
||
X
|
||
|
||
µ({σ}) · X
|
||
µ′ ({σ})
|
||
|
||
|
||
|
||
σ
|
||
|
||
= λS.
|
||
|
||
X
|
||
|
||
µ({σ})
|
||
|
||
σ∈S
|
||
|
||
σ∈S
|
||
|
||
|
||
|
||
=τ
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
(as µ({σ}) ≤ µ′ ({σ}) per definition of ⊑)
|
||
|
||
µ′ ({σ}) · Xσ = τ (Gµ′ )
|
||
|
||
Third, we show that τ −1 is monotone:
|
||
Assume µ ⊑ µ′ .
|
||
|
||
τ −1 (µ) =
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
⊑
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
µ({σ}) · Xσ
|
||
µ′ ({σ}) · Xσ (as µ({σ}) ≤ µ′ ({σ}) per definition of ⊑)
|
||
|
||
= τ −1 (µ′ )
|
||
Lemma 6. Let f : (P, ≤) → (Q, ≤) be a monotone isomorphism for any partially ordered sets P and Q. Then,
|
||
f ∗ : Hom(P, P ) → Hom(Q, Q),
|
||
|
||
φ 7→ f ◦ ϕ ◦ f −1
|
||
|
||
is also a monotone isomorphism.
|
||
Proof. Let f be such a monotone isomorphism, and f ∗ the corresponding lifting.
|
||
First, we note that f ∗ is also bijective. Its inverse is given by (f ∗ )−1 = (f −1 )∗ .
|
||
Second, f ∗ is monotone, as shown in the following calculation.
|
||
f ≤ g =⇒ ∀x.
|
||
|
||
=⇒ ∀x.
|
||
=⇒ ∀x.
|
||
|
||
f (x) ≤ g(x)
|
||
|
||
|
||
|
||
τ ◦ f τ −1 ◦ τ (x) ≤ τ ◦ g τ −1 ◦ τ (x)
|
||
τ ∗ ◦ f (τ (x)) ≤ τ ∗ ◦ g (τ (x))
|
||
|
||
=⇒ ∀y. τ ∗ ◦ f (y) ≤ τ ∗ ◦ g(y)
|
||
=⇒ τ ∗ (f ) ≤ τ ∗ (g)
|
||
|
||
Lemma 7. Let P, Q be complete lattices, and τ a monotone isomorphism. Also
|
||
let lfp be the least fixed point operator. Then the following diagram commutes.
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
Hom(P, P )
|
||
|
||
τ∗
|
||
|
||
lfp
|
||
|
||
29
|
||
|
||
Hom(Q, Q)
|
||
lfp
|
||
|
||
P
|
||
|
||
τ
|
||
|
||
Q
|
||
|
||
Proof. Let ϕ ∈ Hom(P, P ) be arbitrary.
|
||
|
||
lfp ϕ = inf p ϕ(p) = p
|
||
|
||
|
||
τ (lfp ϕ) = τ inf p ϕ(p) = p
|
||
|
||
= inf τ (p) ϕ(p) = p
|
||
|
||
= inf τ (p) ϕ(τ −1 ◦ τ (p)) = τ −1 ◦ τ (p)
|
||
|
||
= inf τ (p) τ ◦ ϕ(τ −1 ◦ τ (p)) = τ (p)
|
||
|
||
= inf q τ ◦ ϕ(τ −1 (q)) = q
|
||
|
||
= inf q τ ∗ (ϕ)(q) = q
|
||
= lfp τ ∗ (ϕ)
|
||
Definition 11. Let T be the program translation from pGCL to a modified Kozen
|
||
syntax, defined inductively:
|
||
T(skip) = skip
|
||
T(xi := E) = xi := fE (x1 , . . . , xk )
|
||
T({P } [p] {Q}) = {T(P )} [p] {T(Q)}
|
||
T(P # Q) = T(P ); T(Q)
|
||
T(if (B) {P } else {Q}) = if B then T(P ) else T(Q) fi
|
||
T(while (B) {P }) = while B do T(P ) od ,
|
||
where p is a probability, k = |Var(P )|, B is a Boolean expression and P, Q are
|
||
pGCL programs. The extended construct skip as well as {P } [p] {Q} is only syntactic sugar and can be simulated by the original Kozen semantics. The intended
|
||
semantics of these constructs are
|
||
and
|
||
|
||
[skip] = id
|
||
[{P } [p] {Q}] = p · T(P ) + (1 − p) · T(Q).
|
||
|
||
Lemma 8. For all guards B, the following identity holds: eB ◦ τ = τ ◦ h·iB .
|
||
P
|
||
Proof. For all Gµ = σ∈Nk µ ({σ}) · Xσ ∈ FPS:
|
||
eB ◦ τ (Gµ ) = eB (µ)
|
||
|
||
= λS. µ(S ∩ B)
|
||
|
||
|
||
X
|
||
X
|
||
τ ◦ hGµ iB = τ
|
||
µ ({σ}) · Xσ +
|
||
0 · Xσ
|
||
σ∈B
|
||
|
||
= λS. µ(S ∩ B)
|
||
|
||
σ6∈B
|
||
|
||
30
|
||
|
||
=⇒
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
∀Gµ ∈ FPS. eB ◦ τ (Gµ ) = τ ◦ hGµ iB
|
||
|
||
Theorem 5. The FPS semantics of pGCL is an instance of Kozen’s semantics,
|
||
i.e. for all pGCL programs P , we have
|
||
τ ◦ JP K = T(P ) ◦ τ .
|
||
Proof. The proof is done via induction on the program structure. We omit the
|
||
loop-free cases, as they are straightforward.
|
||
By definition, T(while (B) {P }) = while B do P od. Hence, the corresponding Kozen semantics is equal to lfp TB,P , where
|
||
T : (M → M) → (M → M),
|
||
|
||
S 7→ eB̄ + (S ◦ P ◦ eB ) .
|
||
|
||
First, we show that τ −∗ ◦ TB,P ◦ τ ∗ = ΦB,P , where τ ∗ is the canonical lifting
|
||
of τ , i.e., τ ∗ (S) = τ ◦ S ◦ τ −1 for all S ∈ (FPS → FPS).
|
||
|
||
−∗
|
||
τ ◦ TB,P ◦ τ ∗ (S) = τ −∗ ◦ TB,P ◦ τ ◦ S ◦ τ −1
|
||
|
||
= τ −∗ eB̄ + τ ◦ S ◦ τ −1 ◦ P ◦ eB
|
||
= τ −1 ◦ eB̄ ◦ τ + τ −1 ◦ τ ◦ S ◦ τ −1 ◦ P ◦ eB ◦ τ
|
||
|
||
= τ −1 ◦ eB̄ ◦ τ + S ◦ τ −1 ◦ P ◦ eB ◦ τ
|
||
|
||
= τ −1 ◦ τ ◦ h·iB̄ + S ◦ τ −1 ◦ P ◦ τ ◦ h·iB
|
||
|
||
= h·iB̄ + S ◦ τ −1 ◦ τ ◦ JP K ◦ h·iB
|
||
(Using I.H. on P ◦ τ )
|
||
|
||
= h·iB̄ + S ◦ JP K ◦ h·iB
|
||
|
||
= ΦB,P (S)
|
||
|
||
Having this equality at hand, we can easily proof the correspondence of our
|
||
while semantics to the one defined by Kozen in the following manner:
|
||
τ ◦ Jwhile (B) {P }K = T(while (B) {P }) ◦ τ
|
||
|
||
⇔ τ ◦ lfp ΦB,P = lfp TB,P ◦ τ
|
||
|
||
⇔ lfp ΦB,P = τ −1 ◦ lfp TB,P ◦ τ
|
||
|
||
⇔ lfp ΦB,P = τ −∗ (lfp TB,P )
|
||
|
||
⇔ lfp ΦB,P = lfp τ −∗ ◦ TB,P ◦ τ
|
||
⇔ lfp ΦB,P = lfp ΦB,P
|
||
|
||
B
|
||
|
||
(Definition of τ ∗ )
|
||
|
||
∗
|
||
|
||
(cf. Lemma 7)
|
||
|
||
Proofs of Section 5
|
||
|
||
Theorem 6 (Superinvariants and Loop Overapproximations). Let ΦB,P
|
||
be the unfolding operator of while(B){P } (cf. Def. 7) and ψ : FPS → FPS. Then
|
||
ΦB,P (ψ) ⊑ ψ
|
||
|
||
implies
|
||
|
||
Jwhile (B) {P }K ⊑ ψ .
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
31
|
||
|
||
Proof. Instance of Park’s Lemma [?].
|
||
|
||
Corollary 2. Given a function f : Mon (X) → FPS, let the linear extension fˆ
|
||
of f be defined by
|
||
fˆ:
|
||
|
||
FPS → FPS,
|
||
|
||
F 7→
|
||
|
||
X
|
||
|
||
[σ]F f (Xσ ) .
|
||
|
||
σ∈Nk
|
||
|
||
Let ΦB,P be the unfolding operator of while (B) {P }. Then
|
||
∀ σ ∈ Nk :
|
||
|
||
ΦB,P (fˆ)(Xσ ) ⊑ fˆ(Xσ )
|
||
|
||
implies
|
||
|
||
Jwhile (B) {P }K ⊑ fˆ .
|
||
|
||
Proof. Let G ∈ FPS be arbitrary.
|
||
ΦB,P (fˆ)(G) =
|
||
|
||
X
|
||
|
||
[σ]G ΦB,P (fˆ)(Xσ )
|
||
|
||
(By Theorem 4)
|
||
|
||
[σ]G f (Xσ )
|
||
|
||
(By assumption)
|
||
|
||
σ∈Nk
|
||
|
||
⊑
|
||
|
||
=⇒
|
||
|
||
X
|
||
|
||
σ∈Nk
|
||
|
||
= fˆ(G)
|
||
JW K ⊑ fˆ
|
||
|
||
(By Theorem 6)
|
||
|
||
Proof of Example 6.
|
||
|
||
|
||
|
||
ΦB,P fˆ X i C j =
|
||
X iC j
|
||
|
||
i=0
|
||
|
||
|
||
1
|
||
+ fˆ
|
||
X iC j
|
||
2
|
||
|
||
·
|
||
i>0
|
||
|
||
case i = 0 : ⇒ (C j + fˆ(0)) = C j = f (X 0 C j )
|
||
|
||
C ˆ i−1 j
|
||
f (X C ) + fˆ X i+1 C j
|
||
case i > 0 : ⇒
|
||
2 (
|
||
1
|
||
i even
|
||
2,
|
||
= C j · 1−C
|
||
= f (X i C j )
|
||
C
|
||
,
|
||
i odd
|
||
1−C 2
|
||
|
||
=⇒ ΦB,P fˆ (X i C j ) ⊑ f (X i C j ).
|
||
|
||
C
|
||
1
|
||
+
|
||
X iC j
|
||
X
|
||
2
|
||
|
||
· XC
|
||
i>0
|
||
|
||
|
||
|
||
32
|
||
|
||
L. Klinkenberg et al.
|
||
|
||
Thus fˆ is a superinvariant.
|
||
i
|
||
|
||
j
|
||
|
||
ΦB,P (ĥ)(X C ) =
|
||
|
||
i
|
||
|
||
X C
|
||
|
||
j
|
||
i=0
|
||
|
||
+ ĥ
|
||
|
||
|
||
|
||
1
|
||
X iC j
|
||
2
|
||
|
||
C
|
||
1
|
||
·
|
||
X iC j
|
||
+
|
||
i>0 X
|
||
2
|
||
|
||
i>0
|
||
|
||
· XC
|
||
|
||
case i = 0 : ⇒ (C j + ĥ(0)) = 1 = h(X 0 C j )
|
||
|
||
|
||
C
|
||
case i > 0 : ⇒
|
||
ĥ X i−1 C j + ĥ X i+1 C j
|
||
2
|
||
|
||
!i−1
|
||
!i+1
|
||
√
|
||
√
|
||
C j+1 1 − 1 − C 2
|
||
1 − 1 − C2
|
||
|
||
=
|
||
+
|
||
·
|
||
2
|
||
C
|
||
C
|
||
j
|
||
|
||
= C ·
|
||
|
||
1−
|
||
|
||
!i
|
||
√
|
||
1 − C2
|
||
= h(X i C j )
|
||
C
|
||
|
||
=⇒ ΦB,P (ĥ)(X i C j ) = h(X i C j )
|
||
Thus fˆ is a superinvariant.
|
||
Verification Python Script
|
||
from sympy import ∗
|
||
i nit p rint ing ()
|
||
x , c = sy m b o l s ( ’ x , c ’ )
|
||
i , j = sy m b o l s ( ’ i , j ’ , i n t e g e r=True )
|
||
#d e f i n e t h e h i g h e r o r d e r t r a n s f o r m e r
|
||
def Phi ( f ) :
|
||
return c /2 ∗ ( f . s u b s ( i , i −1) + f . s u b s ( i , i +1) )
|
||
def c o m p u t e d i f f e r e n c e ( f ) :
|
||
return ( Phi ( f ) − f ) . s i m p l i f y ( )
|
||
#d e f i n e P o l yno m ia l v e r i f y e r
|
||
def v e r i f y p o l y ( p o l y ) :
|
||
p r i n t ( ” Check c o e f f i c i e n t s f o r non−p o s i t i v i t y : ” )
|
||
for c o e f f in poly . c o e f f s ( ) :
|
||
i f coeff > 0:
|
||
return F a l s e
|
||
return True
|
||
# a c t u a l v e r i f i c a t i o n method
|
||
def v e r i f y ( f ) :
|
||
p r i n t ( ” Check i n v a r i a n t : ” )
|
||
pprint ( f )
|
||
result = compute difference( f )
|
||
if result . is zero :
|
||
print ( ” I n v a r i a n t i s a f i x p o i n t ! ” )
|
||
return True
|
||
else :
|
||
print ( ” I n v a r i a n t i s not a f i x p o i n t − check
|
||
try :
|
||
return v e r i f y p o l y ( Poly ( r e s u l t ) )
|
||
except P o l i f i c a t i o n F a i l e d :
|
||
p r i n t ( ” I n v a r i a n t i s n o t a Poly ! ” )
|
||
return F a l s e
|
||
except :
|
||
p r i n t ( ” Unexpected E r r o r ” )
|
||
raise
|
||
|
||
if
|
||
|
||
r e m a i n d e r i s Poly ” )
|
||
|
||
|
||
|
||
Generating Functions for Probabilistic Programs
|
||
|
||
33
|
||
|
||
# d e f i n e t h e l o o p i n v a r i a n t g u e s s ( i != 0) c a s e
|
||
f = c ∗∗ j ∗ ( ( c / (1− c ∗ ∗ 2 ) ) ∗ ( i % 2 ) + (1/(1 − c ∗ ∗ 2 ) ) ∗ ( ( i +1) % 2 ) )
|
||
# Second i n v a r i a n t :
|
||
h = c ∗∗ j ∗ ( ( 1 − s q r t ( 1 − c ∗ ∗ 2 ) ) / c ) ∗∗ i
|
||
print ( ” I n v a r i a n t v e r i f i e d ” i f
|
||
print ( ” I n v a r i a n t v e r i f i e d ” i f
|
||
|
||
v e r i f y ( f ) e l s e ”Unknown ” )
|
||
v e r i f y ( h ) e l s e ”Unknown ” )
|
||
|
||
Program 1.5. Python program checking the invariants
|
||
|
||
Proof of Example 7.
|
||
ΦB,P (fˆ)(X i ) =
|
||
|
||
Xi
|
||
|
||
i=0
|
||
|
||
+
|
||
|
||
1 ˆ
|
||
·f
|
||
i
|
||
|
||
|
||
|
||
Xi
|
||
|
||
·
|
||
i>0
|
||
|
||
case i = 0 : ⇒ 1 + ∞ · fˆ(0) + − ∞ · fˆ(0)
|
||
|
||
1
|
||
X
|
||
|
||
|
||
|
||
+
|
||
|
||
|
||
|
||
1
|
||
1−
|
||
· fˆ X i
|
||
i
|
||
|
||
|
||
= 1 + ∞ · 0 + − ∞ · 0 = 1 = f Xi
|
||
|
||
|
||
|
||
1 ˆ i−1
|
||
1
|
||
case i > 0 : ⇒ 0 +
|
||
· fˆ X i+1
|
||
+ 1−
|
||
·f X
|
||
i
|
||
i
|
||
!
|
||
!
|
||
|
||
|
||
i−3
|
||
i−1
|
||
1
|
||
1 X 1
|
||
1 X 1
|
||
1
|
||
+ 1−
|
||
· 1− ·
|
||
· 1− ·
|
||
=
|
||
i
|
||
e n=0 n!
|
||
i
|
||
e n=0 n!
|
||
!
|
||
!
|
||
i−3
|
||
i−1
|
||
1 X 1
|
||
1
|
||
1
|
||
1 X 1
|
||
+
|
||
1− ·
|
||
−
|
||
−
|
||
·
|
||
+
|
||
=
|
||
i
|
||
ei n=0 n!
|
||
e n=0 n!
|
||
i
|
||
!
|
||
|
||
|
||
i−1
|
||
1 X 1
|
||
1
|
||
1
|
||
1
|
||
=
|
||
1− ·
|
||
+
|
||
·
|
||
+
|
||
e n=0 n!
|
||
ei
|
||
(i − 2)! (i − 1)!
|
||
!
|
||
!
|
||
i−1
|
||
i−2
|
||
1
|
||
1 X 1
|
||
1 X 1
|
||
+
|
||
=
|
||
1− ·
|
||
=
|
||
1− ·
|
||
e n=0 n!
|
||
e(i − 1)!
|
||
e n=0 n!
|
||
|
||
= f Xi
|
||
=⇒ ΦB,P (fˆ)(X i ) = f (X i )
|
||
|
||
i>0
|
||
|
||
·X
|
||
|
||
|
||
|
||
i−1
|
||
1 X 1
|
||
·
|
||
ei n=0 n!
|
||
|
||
Mathematica input query:
|
||
Input:
|
||
Output:
|
||
|
||
1
|
||
·
|
||
k
|
||
0
|
||
|
||
k−3
|
||
1 X 1
|
||
1− ·
|
||
e n=0 n!
|
||
|
||
!
|
||
|
||
1
|
||
+ (1 − ) ·
|
||
k
|
||
|
||
k−1
|
||
1 X 1
|
||
1− ·
|
||
e n=0 n!
|
||
|
||
!
|
||
|
||
−
|
||
|
||
k−2
|
||
1 X 1
|
||
1− ·
|
||
e n=0 n!
|
||
|
||
!
|
||
|
||
!
|
||
|
||
|