Almost Sure Productivity∗
Alejandro Aguirre1 , Gilles Barthe1 ,
Justin Hsu2 , and Alexandra Silva2
1
2

IMDEA Software, Madrid, Spain
University College London, London, UK

arXiv:1802.06283v1 [] 17 Feb 2018

Abstract
We define Almost Sure Productivity (ASP), a probabilistic generalization of the productivity
condition for coinductively defined structures. Intuitively, a probabilistic coinductive stream
or tree is ASP if it produces infinitely many outputs with probability 1. Formally, we define
almost sure productivity using a final coalgebra semantics of programs inspired from Kerstan
and König. Then, we introduce a core language for probabilistic streams and trees, and provide
two approaches to verify ASP: a sufficient syntactic criterion, and a reduction to model-checking
pCTL∗ formulas on probabilistic pushdown automata. The reduction shows that ASP is decidable
for our core language.
1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs, F.3.2 Semantics of Programming Languages, D.3.1 Formal Definitions and Theory
Keywords and phrases Coinduction, Probabilistic Programming, Productivity
Digital Object Identifier 10.4230/LIPIcs.ICALP.2018.

1

Introduction

The study of probabilistic programs has a long history, especially in connection with semantics [25] and verification [26, 20, 32]. Over the last decade, the field of probabilistic
programming has undergone impressive developments, with the emergence of practical probabilistic programming languages and novel applications in machine learning, privacy-preserving
data mining, and modeling of complex systems. On the more theoretical side, many semantical and syntactic tools have been developed for modeling and verifying probabilistic
programs. In particular, significant attention has been devoted to termination of probabilistic
programs, focusing on the complexity of the different termination classes [22], and on practical
methods for proving that a program terminates [18, 29, 2, 31]. The latter class of works
generally focuses on almost sure termination, which guarantees that a program terminates
with probability 1.
Coinductive probabilistic programming is an emerging computational paradigm that
extends probabilistic programming to infinite objects such as streams and infinite trees
and provides a natural setting for programming and reasoning about probabilistic infinite
processes such as Markov chains or Markov decision processes. Rather surprisingly, the
study of coinductive probabilistic programming was initiated only very recently [3], and little
is known about generalizations of coinductive concepts and methods to the probabilistic
setting. In this paper, we focus on the notion of productivity, which informally ensures
that one can compute arbitrarily precise finite approximations of infinite objects in finite

∗

This is the full version of the paper.
EA

TC S

© Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva;
licensed under Creative Commons License CC-BY
45th International Colloquium on Automata, Languages, and Programming (ICALP 2018).
Editors: Ioannis Chatzigiannakis, Christos Kaklamanis, Daniel Marx, and Don Sannella;
Article No. ; pp. :1–:23
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

XX:2

Almost Sure Productivity

time. Productivity has been studied extensively for standard, non-probabilistic coinductive
languages [21, 16, 1, 13, 8], and the probabilistic setting introduces new challenges.

Contributions
Our first contribution is definitional. We introduce almost sure productivity (ASP), a
probabilistic counterpart to productivity. In the simplest setting of streams, a probabilistic
computation is almost surely productive if it produces an infinite stream of outputs with
probability 1. For instance, consider the stream defined by the equation
σ = (a : σ) ⊕p σ
Viewed as a program, this stream repeatedly flips a coin with bias p ∈ (0, 1), producing the
value a if the coin comes up heads and retrying if the coin comes up tails. This computation
is almost surely productive since the probability it fails to produce outputs for n steps is
(1 − p)n , which tends to zero as n increases. In contrast, consider the stream defined by the
equation
σ = ā ⊕p 
This computation flips a single biased coin and returns an infinite stream of a’s if the coin
comes up heads, and the empty stream  if the coin comes up tails. This process is not
almost surely productive since its probability of outputting an infinite stream is only p, which
is strictly less than 1.
We define almost sure productivity for an abstract language that can be equipped with
a final coalgebra semantics, in the style of Kerstan and König [23], and give a semantic
characterization. Although intuitive, the definition involves measure-theoretic technicalities
(Section 3). We instantiate our semantics on a concrete, core probabilistic language for
computing over streams and trees (Section 4). Then, we propose two methods for proving
almost sure productivity.
1. We begin with a syntactic method that assigns to each expression e a measure in R
(Section 5). Intuitively, the measure represents the expected difference between the
number of outputs produced and consumed per evaluation step of the expression. For
instance, the computation that repeatedly flips a fair coin and outputs a value if the coin
is heads has measure 12 —with probability 1/2 it produces an output, with probability 0
it produces no outputs. More complex terms in our language can also consume outputs
internally, leading to possibly negative values for the productivity mesaure.
We show that every expression whose measure is strictly positive is almost surely productive. The proof of soundness of the method uses concentration results from martingale
theory. However, the method is incomplete—it does not yield any information for
expressions with non-positive measure.
2. To give a more sophisticated analysis, we give an encoding into probabilistic modelchecking for both streams and trees (Section 6). We define an interpretation of expressions
as probabilistic pushdown automata and show that almost sure productivity of the
expression can be characterized by a logical formula in the qualitative fragment of pCTL∗ .
This fragment is known to be decidable [28], giving a decision procedure for the almost
sure productivity property.
We consider more advanced generalizations and extensions in Section 7, survey related work
in Section 8, and conclude in Section 9.

A. Aguirre, G. Barthe, J. Hsu, A. Silva

2

XX:3

Mathematical Preliminaries

This section reviews basic notation and definitions from measure theory and category theory
(though we assume some familiarity with these areas).
Given a set A we will denote by A⊥ the coproduct of A with a one-element set containing
a distinguished element ⊥, i.e., A⊥ = A + {⊥}.

Streams, Trees, Coalgebra
We will denote by Oω the set of infinite streams of elements of O (alternatively characterized
as functions N → O). We have functions head : Oω → O and tail : Oω → Oω that enable
observation of the elements of the stream. In fact, they provide Oω with a one-step structure
that is canonical: given any two functions h : S → O and t : S → S there exists a unique
stream function associating semantics to elements of S:
S

J−K

/ Oω

id×J−K


/ O × Oω

<h,t>


O×S

<head,tail>

Formally, this uniqueness property is known as finality: Oω is the final coalgebra of the
functor F (X) = O × X and the above diagram gives rise to a coinductive definition principle.
A similar principle can be obtained for infinite binary trees and other algebraic datatypes.
The above diagrams are in the category of sets and functions, but infinite streams and trees
have a very rich algebraic structure and they are also the carrier of final coalgebras in other
categories. For the purpose of this paper, we will be particularly interested in a category
where the maps are probabilistic—the Kleisli category of the distribution (or Giry) monad.

Probability Distributions, σ-algebras, Measurable Spaces
Given an arbitrary set X we call a set Σ of subsets of X a σ-algebra if it contains the empty
set and is closed under complement and countable union. A measurable space is a pair (X, Σ).
A probability measure or distribution µ over such a space is a function µ : Σ → [0, 1] that
assigns probabilities µ(A) ∈ [0, 1] to the measurable sets A ∈ Σ, and satisfies the following
conditions:
µ(X) = 1
S
P
µ( i∈I Ai ) = i∈I µ(Ai ) whenever {Ai }i∈I is a countable collection of disjoint measurable sets.
The collection D(X) of probability distributions over a measurable space X forms the socalled Giry monad. The monad unit η : X → D(X) maps a ∈ X to the point mass (or Dirac
measure) δa on a. The monad multiplication m : DD(X) → D(X) is given by integration:
Z
m(P )(S) = evS dP, where evS (µ) = µ(S)
Given measurable spaces (X, ΣX ) and (Y, ΣY ), a Markov kernel is a function P : X × ΣY →
[0, 1] (equivalently, X → ΣY → [0, 1]) that maps each source state x ∈ X to a distribution
over target states P (x, −) : ΣY → [0, 1].
Markov kernels form the arrows in the Kleisli category K`(D) of the D monad; we denote
P
such arrows by X ◦ / Y . Composition in the Kleisli category is given by integration:
Z
Q
P
◦ / Z
X ◦ /Y
(P ◦ Q)(x, A) =
P (x, dy) · Q(y, A)
y∈Y

ICALP 2018

XX:4

Almost Sure Productivity

Associativity of composition is essentially Fubini’s theorem.

3

Defining Almost Sure Productivity

We will consider programs that denote probability distributions over coinductive types,
such as infinite streams or trees. In this section, we focus on the definitions for programs
producing streams and binary trees for simplicity, but all the results below can be generalized
to arbitrary polynomial functors (see Section 7).
First, we introduce the semantics of programs. Rather than fix a concrete programming
language at this point, we let T denote the space of programs and suppose we have a discrete
global clock. At each time step, with some probability, we will either observe a concrete
output a : A or nothing ⊥. Intuitively, a program p ∈ T is ASP if its probability of producing
unboundedly many outputs is 1. Formally, we will endow programs in T with a denotational
semantics J−K : T → D((A⊥ )ω ). We will define this global semantics coinductively, starting
from a given one-step semantics function that maps each term to an output in A⊥ and
the resulting term. The subtlety in the definition is that since the step function will be
probabilistic, we need to work in the Kleisli category for the distribution monad; final
coalgebras in this category are more difficult to compute. We take the work on probabilistic
streams by Kerstan and König [23] as our starting point, and then generalize to probabilistic
trees.
I Theorem 1 (Finality for streams [23]). Given a set of programs T endowed with a probabilistic
step function st : T → D(A⊥ × T), there is a unique semantics function J−K assigning to
each program a probability distribution of output streams such that the following diagram
commutes in the Kleisli category K`(D).
T

/ (A⊥ )ω

J−K
◦

st ◦


A⊥ × T

◦ <head,tail>

id×J−K
◦


/ A⊥ × (A⊥ )ω

I Definition 2 (ASP for streams). A stream program p ∈ T is almost surely productive (ASP)
if
Pr [σ has finitely many concrete output elements a ∈ A] = 0.
σ∼JpK

For this to be a sensible definition, the event in the probability must be a measurable set
in some σ-algebra on (A⊥ )ω . Following Kerstan and König, we take the σ-algebra generated
by cones, sets of the form uAω = {v ∈ (A⊥ )ω | u prefix of v, u ∈ (A⊥ )∗ }. We stress that our
definition of ASP is independent of the way we defined J−K : T → D(A⊥ )ω . Working with
a coinductive definition principle will be useful later for showing soundness when verifying
ASP, but our definition is sensible for any semantic function J−K.
I Example 3. As an example let us consider the following program defining a stream σ
recursively, in which each recursion step is determined by a coin flip with bias p. If the coin
flip results in heads we add an element a, otherwise we don’t output and we compute the
tail.
σ = (a : σ) ⊕p tail(σ)

A. Aguirre, G. Barthe, J. Hsu, A. Silva

XX:5

The above program will output infinite many a’s when p > 1/2 (that is, the probability of
heads is greater than tails). Hence, the above program is ASP for p > 1/2. In the sequel we
will show two methods to prove this fact.
For the purpose of generalizing the above to other datatypes and also for developing
methods to check ASP, it will be convenient to use a different representation for the functor
F (X) = A⊥ × X ∼
= A × X + X. In the rest of this paper we will often use the latter
representation and refer to the final coalgebra as observation streams OS = (A⊥ )ω with
structure OS o

<out,unf>
∼
=

A × OS + OS given by out(a, σ) = a : σ and unf(σ) = ⊥ : σ.

Now, we can generalize to infinite trees by using the functor F (X) = A × X × X + X.
I Theorem 4 (Finality for trees). Given a set of programs T endowed with a probabilistic
step function st : T → D(A × T × T + T), there is a unique semantics function J−K assigning
to each program a probability distribution of output trees such that the following diagram
commutes in the Kleisli category K`(D).
/ Trees(A⊥ )

J−K
◦

T
st ◦


A×T×T+T

◦ <out,unf>−1

id×J−K×J−K+J−K
◦


/ A × Trees(A⊥ ) × Trees(A⊥ ) + Trees(A⊥ )

Trees(A⊥ ) are infinite trees where the nodes are either elements of A or ⊥. An a-node has
two children whereas a ⊥-node only has one child. Formally, we can construct these trees
with the two maps out and unf:

a

⊥

unf(

σ

)=

σ

out(a,

σ

,

τ

)=

σ

τ

Defining ASP for trees is a bit more subtle than for streams. Due to measurability issues,
our definition will only take the probability along one path at a time in the tree. A bit
more formally, let w ∈ {L, R}ω be an infinite word on alphabet {L, R}. Given any tree
t ∈ Trees(A⊥ ), w induces a single path tw in the tree—starting from the root, the path
follows the left or right child of a-nodes as indicated by w, and the single child of ⊥-nodes.
Then, we can define the following notion of ASP.
I Definition 5 (ASP for trees). A tree program p : T is almost surely productive (ASP) if
∀w ∈ {L, R}ω . Pr [tw has infinitely many concrete output nodes a ∈ A] = 1.
t∼JpK

We have omitted the σ-algebra structure on Trees(A⊥ ) for lack of space, but it is quite
similar to the one for streams: it is generated by the cones uTrees(A⊥ ) = {t ∈ Trees(A⊥ ) |
t is an extension of the finite tree u}. For every w ∈ {L, R}ω , the above event is measurable
in this σ-algebra.
I Example 6. Consider the probabilistic tree defined by the following equation:
τ = mk(a, τ, τ ) ⊕p left(τ )

ICALP 2018

XX:6

Almost Sure Productivity

The mk(a, t1 , t2 ) constructor produces a tree with the root labeled by a and children t1 and
t2 , while the left(t) destructor consumes the output at the root of t and steps to the left
child of t. While this example is more difficult to work out informally, it has similar ASP
behavior as the previous example we saw for streams. When p > 1/2 this program is ASP,
since it has strictly higher probability of constructing a node (and producing an output)
than destructing a node (and consuming an output). In the following two sections, we will
present two methods to verify this property.

4

A Calculus for Probabilistic Streams and Trees

Now that we have introduced almost sure productivity, we consider how to verify this property.
We work with a simple calculus for probabilistic coinductive programming, separated into
languages for streams and for trees. We suppose that outputs are drawn from some finite
alphabet A. The language for streams considers terms of the following form:
e ∈ T ::= σ | e ⊕p e | u : e (u ∈ P) | tail(e)
The distinguished variable σ represents a recursive occurrence of the stream so that streams
can be defined via equations σ = e. The operation e1 ⊕p e2 selects e1 with probability p and
e2 with probability 1 − p. We consider a set P of primitive streams, represented by sequences
in Aω . The constructor u : e builds a stream with head given by the first element in u and
tail e. The first element of u is consumed, so that further occurrences of u in e draw from
the tail of u. The destructor tail(e) computes the tail of a stream.
The language for trees is similar, with terms of the following form:
e ∈ T ::= τ | e ⊕p e | mk(u, e, e) (u ∈ P) | left(e) | right(e)
The distinguished variable τ represents a recursive occurrence of the tree, so that trees can
be defined as τ = e. The set P of primitive trees now contains infinite binary trees labeled by
A; the constructor mk(u, e1 , e2 ) builds a tree with root labeled by the root of u and children
e1 and e2 , where e1 and e2 draw from the left and right children of u. The destructors left(e)
and right(e) extract the left and right children of e, respectively.
We interpret these terms coalgebraically by first giving a step function from ste : T →
D(F (T)) for an appropriate functor, and then taking the semantics as the map to the final
coalgebra as defined in the previous section. In the case of streams, we take the functor
F (X) = A × X + X: a term steps to a distribution over either an output in A and a resulting
term, or just a resulting term (with no output). To describe how the recursive occurrence σ
steps, we parametrize the step function ste by the top level stream term e; this term remains
fixed throughout the evaluation. We also assume each primitive stream term u is associated
with an output au ∈ A and primitive stream u0 ∈ P, representing the rest of the stream.
In the step relation, probabilistic choice terms are reduced by scaling the result of
stepping e and the result of stepping e0 by p and 1 − p respectively, and then combining the
distributions:
ste (e1 ⊕p e2 ) , p · ste (e1 ) + (1 − p) · ste (e2 )
The next cases push destructors into terms:
ste (tailk (u : e)) , ste (tailk−1 (e[u0 /u]))
ste (tailk (e1 ⊕p e2 )) , ste (tailk (e1 ) ⊕p tailk (e2 ))

A. Aguirre, G. Barthe, J. Hsu, A. Silva

XX:7

Observe that after the output in the constructor is consumed in the first case, occurences of
u in the tail term e are replaced by a new primitive stream u0 . The remaining cases return
a point distribution. If we have reached a constructor then we produce a single output.
Otherwise, we replace σ by the top level stream term, unfolding a recursive occurrence.
ste (u : e0 ) , δ(inl(au , e0 [u0 /u]))
ste (e0 ) , δ(inr(e0 [e/σ])) otherwise

(e0 = σ, e0 = tailk (σ))

Note that a stream may produce multiple outputs in a single step but only first output is
recorded during the step. However, the remaining outputs are preserved and recorded in
later steps.
The semantics is similar for trees. We take the functor F (X) = (A × X × X) + X: a
term reduces to a distribution over either an output in A and two child terms, or a resulting
term and no output. We also assume each primitive tree term u is associated with an output
au ∈ A and two primitive terms ul , ur .
The main changes are in the constructors and destructors. The constructor mk(u, e1 , e2 )
reduces to δ(inl(au , e1 [ul /u], e2 [ur /u])), representing an output au this step. Destructors
are handled similar to tail for streams, where left(mk(u, e1 , e2 )) reduces to e1 [ul /u] and
right(mk(u, e1 , e2 )) reduces to e2 [ur /u], and tailk (−) is generalized to any finite combination
of left(−) and right(−).
Concretely, let C[e0 ] be any (possibly empty) combination of left and right applied to e0 .
We have the following step rules:
ste (C[left(mk(u, el , er ))]) , ste (C[el ])
ste (C[right(mk(u, el , er ))]) , ste (C[er ])
ste (C[e1 ⊕p e2 ]) , p · ste (C[e1 ]) + (1 − p) · ste (C[e2 ])
ste (mk(u, el , er )) , δ(inl(au , el [ul /u], er [ur /u]))
ste (C[τ ]) , δ(inr(C[e]))

5

Syntactic Conditions for ASP

With the language and semantics in hand, we now turn to proving ASP. While it is theoretically
possible to reason directly on the semantics using our definitions from Section 3, in practice
it is much easier to work with the language. In this section we present a syntactic sufficient
condition for ASP. Intuitively, the idea is to approximate the expected number of outputs
every step. If this measure is strictly positive, then the program is ASP.

5.1

A Syntactic Measure

We define a syntactic measure #(−) : T → R by induction on stream terms:
#(σ) , 0
#(e1 ⊕p e2 ) , p · #(e1 ) + (1 − p) · #(e2 )
#(u : e) , #(e) + 1
#(tail(e)) , #(e) − 1
The measure # describes the expected difference between the number of outputs produced
(by constructors) and the number of outputs consumed (by destructors) in each unfolding of

ICALP 2018

XX:8

Almost Sure Productivity

the term. Likewise, we can define a measure for tree terms.
#(τ ) , 0
#(e1 ⊕p e2 ) , p · #(e1 ) + (1 − p) · #(e2 )
#(mk(u, e1 , e2 )) , min(#(e1 ), #(e2 )) + 1
#(left(e)) = #(right(e)) , #(e) − 1
We can now state conditions for ASP for streams.
I Theorem 7. Let e be a stream term with γ = #(e). If γ > 0, e is ASP.
Note that we cannot conclude anything positive or negative when γ = 0. Likewise, we
can give similar sufficient conditions for tree terms.
I Theorem 8. Let e be a tree term with γ = #(e). If γ > 0, e is ASP.

5.2

Soundness

The main idea behind the proof for streams is that by construction of the step relation, each
step either produces an output or unfolds a fixed point (if there is no output). In unfolding
steps, the expected measure of the term plus the number of outputs increases by γ. By
defining an appropriate martingale and applying the Azuma-Hoeffding inequality, the sum of
the measure and the number of outputs must increase linearly as the term steps when γ > 0.
Since the measure is bounded above—when the measure is large the stream outputs instead
of unfolding—the number of outputs must increase linearly and the stream is ASP.
We will need a few standard constructions and results from probability theory.
I Definition 9 (See, e.g., [14]). A filtration {Fi }i∈N of a σ-algebra F on a measurable space
A is an sequence of σ-algebras such that Fi ⊆ Fi+1 and Fi ⊆ F, for all i ∈ N. A stochastic
process is a sequence of random variables {Xi : A → B}i∈N for B some measurable space,
and the process is adapted to the filtration if every Xi is Fi -measurable.
Intuitively, a filtration gives each event a time i at which the event starts to have a
well-defined probability. A stochastic process is adapted to the filtration if its value at time i
only depends on events that are well-defined at time i or before (and not events at future
times).
An important class of stochastic processes are martingales.
I Definition 10 (See, e.g., [14]). Let {Xi : A → R} be a real-valued stochastic process
adapted to some filtration on A, and let µ be a measure on A. Suppose that Eµ [Xi ] < ∞ for
all Xi . The sequence is a martingale if for all i ∈ N, we have
Eµ [Xi+1 | Fi ] = Xi .
The conditional expectation turns Xi+1 from an Fi+1 -measurable map to an Fi -measurable
map; equivalently, the martingale condition can be stated as
Eµ [(Xi+1 − Xi )χF ] = 0,
for every event F ∈ F, where χF is the indicator function. If the equalities are replaced by
≥ (resp., ≤), then the sequence is a sub- (resp., super-) martingale.

A. Aguirre, G. Barthe, J. Hsu, A. Silva

XX:9

Martingale processes determine a sequence of random variables that may not be independent, but where the expected value of the process at some time step depends only on its
value at the previous time step. Martingales satisfy concentration inequalities.
I Theorem 11 (Azuma-Hoeffding inequality [5]). Let {Xi }i be sequence such that |Xi+1 −Xi | ≤
c for all i ∈ N. If {Xi }i is a sub-martingale, then for every n ∈ N and B ≥ 0, we have
Pr[Xn − X0 ≤ −B] ≤ exp(−B 2 /2nc).
If {Xi }i is a super-martingale, then for every n ∈ N and B ≥ 0, we have
Pr[Xn − X0 ≥ B] ≤ exp(−B 2 /2nc).
If {Xi }i is both a martingale, then combining the above results gives
Pr[|Xn − X0 | ≥ B] ≤ 2 exp(−B 2 /2nc).
Proof of Theorem 7. While the semantics constructed in Section 3 is sufficient to describe
ASP, for showing soundness it is more convenient to work with an instrumented semantics
that tracks the term in the observation stream. We can give a step function of type
st0e : T → D(F 0 (T)), where F 0 (X) = (A × X + X) × T by recording the input term in the
output. For instance:
st0e (u : e0 ) , δ(inl(au , e0 [u0 /u]), u : e0 )
st0e (σ) , δ(inr(e), σ)
and so forth. Using essentially the same construction as in Section 3, we get an instrumented
semantics J−K0 : T → D(OS0 ), where OS0 are infinite streams with constructors out0 :
(A × OS0 ) × T → OS0 and unf 0 : OS0 × T → OS0 , representing output and unfold steps
respectively. Letting the map u : OS0 → OS simply drop the instrumented terms, the map
D(u) ◦ J−K0 : T → D(OS) coincides with the semantics J−K defined in Section 3 by finality.
Now, we define a few stochastic processes. Let {Ti : OS0 → T}i be the sequence of
instrumented terms with T0 = e, {Oi : OS0 → {0, 1}}i be 1 if the ith node is an output
node and 0 if not, {Ui : OS0 → {0, 1}}i = {1 − Oi }i . It is straightforward to show that
Ti is Fi−1 -measurable (and hence Fi -measurable), and Oi , Ui are Fi -measurable—all three
processes are defined by the events in the first i steps.
Now for any stream term t ∈ T, we claim that
Est0e (t) [(inl(−, t0 ), −) → 1 + #(t0 ) else (inr(t0 ), −) → #(t0 ) − γ] = #(t).
This follows by induction on terms using the definition of st0e . We can lift the equality to the
semantics, giving
EJT0 K0 [Oi+1 − γUi+1 + #(Ti+2 ) | Fi ] = #(Ti+1 )
noting that Ti+1 is Fi -measurable and recalling that T0 = e is the initial term. We now
define another stochastic process via
Xi ,

i
X
j=0

Oj − γ

i
X

Uj + #(Ti+1 ).

j=0

Note that Xi is Fi -measurable. As we will show, this process tends towards zero, the second
term decreases, and the third term remains bounded. Hence, the first term—the cumulative

ICALP 2018

XX:10

Almost Sure Productivity

number of outputs—must tend towards infinity. Evidently each Xi is bounded and we are
working with probability measures, so each Xi is integrable. We can directly check that
{Xi }i is a martingale:


i
i
X
X
Oj + Oi+1 − γ
Uj − γUi+1 + #(Ti+2 ) | Fi 
EJT0 K0 [Xi+1 | Fi ] = EJT0 K0 
j=0

j=0



i
i
X
X
= EJT0 K0 
Oj − γ
Uj + #(Ti+1 ) | Fi 
j=0

=

i
X
j=0

Oj − γ

j=0

i
X

Uj + #(Ti+1 ) = Xi .

j=0

We now claim that #(Ti ) ≤ c0 where c0 is one more than the number of constructors in the
original term T0 . This follows by observing that (i) the step function increases the measure
by at most the number of constructors or 1 (if the step function unfolds a primitive term)
every unfolding step, and (ii) the step function only unfolds if a term reduces to a term with
non-positive measure. Similarly,
i
X

Uj ≥ bi/c0 c

j=0

since each unfolding step leads to at most c0 output (non-unfolding) steps.
Since Oi and Ui are both in {0, 1}, this implies that |Xi+1 − Xi | is bounded by some
constant c = c0 + 2, depending only on the initial term. We can now apply the AzumaHoeffding inequality (Theorem 11). For every n ∈ N and B ≥ 0, we have
Pr [Xn − X0 ≥ −B] ≥ 1 − exp(−B 2 /2nc).

JT0 K0

Taking B = n2/3 , we have
Pr [Xn ≥ X0 − n2/3 ] ≥ 1 − exp(1/2n1/3 c).

JT0 K0

We also know that the total number of outputs is at least
n
X
j=0

Oj = Xn + γ

n
X

Uj − #(Tn+1 ) ≥ Xn + γbn/c0 c.

j=0

So if γ > 0, the stream has zero probability of producing at most M outputs for any finite
M . This is because for Xn is at least −n2/3 with probability arbitrarily close to 1 (for large
enough n), and γbn/c0 c grows linearly in n for γ positive. Hence, the term is ASP.
J
The proof for trees is similar, showing that on any path through the observation tree
there are infinitely many output steps with probability 1.
Proof of Theorem 8. We again work with an instrumented semantics based on the step
function st0e : T → D(F 0 (T)), where F 0 (X) = (A × X × X + X) × T by recording the input
term in the output. For instance:
st0e (mk(u, e1 , e2 )) , δ(inl(au , e1 [ul /u], e2 [ur /u]), mk(u, e1 , e2 ))
st0e (τ ) , δ(inr(e), τ )

A. Aguirre, G. Barthe, J. Hsu, A. Silva

XX:11

and so forth. Using essentially the same construction as in Section 3, we get an instrumented
semantics J−K0 : T → D(OT0 ), where OT0 are infinite trees with constructors out0 : (A ×
OT0 × OT0 ) × T → OT0 and unf 0 : OT0 × T → OT0 , representing output and unfold steps
respectively. Letting the map u : OT0 → OT simply drop the instrumented terms, the map
D(u) ◦ J−K0 : T → D(OT) coincides with the semantics J−K defined in Section 3 by finality.
Let w ∈ {L, R}ω be any infinite word, describing whether to follow the left or right child
of a tree. Each word determines a path through an observation tree: on unfold nodes we
simply follow the child, while on output nodes we follow the child indicated by w. We aim
to show that if γ > 0, then there are infinitely many output nodes along this path with
probability 1. If this holds for all w, then the tree term must be ASP.
To model the path, we define a sequence {Pi : OT0 → A × T × T + T}i inductively. P0
is simply the root of the output tree OT0 . Given P0 , . . . , Pi , we define Pi+1 to be a child of
Pi as follows. If Pi is an unfold node it only has one child, so we take Pi+1 to be this child.
Otherwise we take Pi+1 to be the child of Pi indicated by wj+1 , where j is the number of
output nodes in P0 , . . . , Pi . The process {Pi }i is adapted to the filtration on OT0 . (Note
that all indices start at 0.)
Now, we can define similar processes as in the stream case with respect to the path.
Let {Ti : OS0 → T}i be the sequence of instrumented terms along the path with T0 = e,
{Oi : OS0 → {0, 1}}i be 1 if Pi is an output node and 0 if not, {Ui : OS0 → {0, 1}}i = {1−Oi }i .
It is straightforward to show that Ti is Fi−1 -measurable (and hence Fi -measurable), and
Oi , Ui are Fi -measurable—all three processes are defined by the events in the first i steps.
Now for any tree term t ∈ T, we have
Est0e (t) [(inl(−, t0 ), −) → 1 + #(t0 ) else (inr(t0 ), −) → #(t0 ) − γ] ≥ #(t)
by induction on terms using the definition of st0e . The inequality arises from applying a
destructor to a constructor—we may end up with a child term that has larger measure than
the parent term, since the measure of a constructor takes the smaller measure of its children.
We can lift the inequality to the semantics, giving
EJT0 K0 [Oi+1 − γUi+1 + #(Ti+2 ) | Fi ] ≥ #(Ti+1 )
noting that Ti+1 is Fi -measurable and letting T0 = e be the initial term. We can now our
invariant process
Xi ,

i
X

Oj − γ

j=0

i
X

Uj + #(Ti+1 )

j=0

which is a sub-martingale:
EJT0 K0 [Xi+1



i
i
X
X
| Fi ] = EJT0 K0 
Oj + Oi+1 − γ
Uj − γUi+1 + #(Ti+2 ) | Fi 
j=0

j=0



i
i
X
X
≥ EJT0 K0 
Oj − γ
Uj + #(Ti+1 ) | Fi 
j=0

=

i
X
j=0

Oj − γ

j=0

i
X

Uj + #(Ti+1 ) = Xi .

j=0

The remainder of the proof is now quite similar to the stream case. #(Ti ) ≤ c0 where c0 is
one more than the number of constructors in the original term T0 . This follows by observing

ICALP 2018

XX:12

Almost Sure Productivity

that (i) the step function increases the measure by at most the number of constructors or 1
(if the step function unfolds a primitive term) every unfolding step, and (ii) the step function
only unfolds if a term reduces to a term with non-positive measure. Similarly,
i
X

Uj ≥ bi/c0 c

j=0

since each unfolding step leads to at most c0 output (non-unfolding) steps.
Since Oi and Ui are both in {0, 1}, this implies that |Xi+1 − Xi | is bounded by some
constant c = c0 + 2, depending only on the initial term. We can now apply the AzumaHoeffding inequality (Theorem 11). For every n ∈ N and B ≥ 0, we have
Pr [Xn − X0 ≥ −B] ≥ 1 − exp(−B 2 /2nc).

JT0 K0

Taking B = n2/3 , we have
Pr [Xn ≥ X0 − n2/3 ] ≥ 1 − exp(1/2n1/3 c).

JT0 K0

We also know that the total number of outputs along the path w is at least
n
X

Oj = Xn + γ

j=0

n
X

Uj − #(Tn+1 ) ≥ Xn + γbn/c0 c.

j=0

So if γ > 0, the stream has zero probability of producing at most M outputs along w for
any finite M . This is because for Xn is at least −n2/3 with probability arbitrarily close to 1
(for large enough n), and γbn/c0 c is growing linearly in n for γ positive. Since the tree term
produces at least M outputs along path w with probability 1 for every M and every w, it is
ASP.
J

5.3

Examples

We consider a few examples of our analysis. Let the alphabet A = N.
I Example 12. Consider the stream definition σ = (nats : σ) ⊕p tail(σ), where the primitive
term nats represents the stream of natural numbers 0, 1, . . . . Each element in nats is
produced with probability p and dropped with probability 1 − p. The # measure of the
stream term is p · 1 + (1 − p) · (−1) = 2p − 1. By Theorem 7, the stream is ASP when p > 1/2.
The measure does not give useful information when # is not positive.
I Example 13. Consider the stream definition σ = (nats : σ) ⊕1/2 tail(σ); the # measure of
the term is 0. The number of outputs can be modeled by a simple random walk on a line,
where the maximum position is the number of outputs produced by the stream. Since a
simple random walk has probability 1 of reaching every n ∈ N [30], the stream term is ASP.
In contrast, the term #(σ) = 0 but the stream definition σ = σ is clearly non-productive.
We can give similar examples for tree terms.
I Example 14. Let ones be a primitive tree term that always produces the output 1.
Consider the tree definitions τ = ei , where
e1 , left(τ ) ⊕1/4 mk(ones, τ, τ )
e2 , left(τ ) ⊕1/4 mk(ones, τ, left(τ )) .
We apply Theorem 8 to deduce ASP. We have #(e1 ) = (1/4) · (−1) + (3/4) · (+1) = 1/2, so
the first term is ASP. For the second term, #(e2 ) = (1/4) · (−1) + (3/4) · 0 = −1/4, so our
analysis does not give any information.

A. Aguirre, G. Barthe, J. Hsu, A. Silva

6

XX:13

Probabilistic Model-Checking for ASP

The syntactic analysis for ASP is simple, but it is not complete—no information is given if
#(e) ≤ 0. In this section we give a more sophisticated, complete analysis by first modeling
the operational semantics of a term by a Probabilistic Pushdown Automaton (pPDA), then
deciding ASP by reduction to model-checking.

6.1

Probabilistic Pushdown Automata and pCTL∗

A pPDA is a tuple A = (S, Γ, T ) where S is a finite set of states and Γ is a finite stack
alphabet. The transition function T : S × (Γ ∪ {⊥}) × S × Γ∗ → [0, 1] in addition to jumping
between states, looks on each step at the symbol on top of the stack (which might be empty,
denoted ⊥), consumes it, and pushes a (possibly empty, denoted ε) string of symbols onto
the stack. A configuration of A is an element of C = S × Γ∗ , and represents the state of the
pPDA and the contents of its stack (with the top on the left) at some point of its execution.
Given a configuration, the transition function T specifies a distribution over configurations
in the next step. Given an initial state s and an initial stack γ ∈ Γ∗ , T induces a distribution
Paths(s, γ) over the infinite sequence of configurations starting in (s, γ).
Probabilistic Computation Tree Logic (pCTL∗ ) [19] is a branching-time temporal logic
that describes states of a probabilistic transition system, which in a pPDA actually correspond
to its configurations. Propositions in pCTL∗ are defined by the syntax
Φ, Ψ ::= > | Q | Φ ∧ Ψ | ¬Φ | P(φ) ./ p

φ, ψ ::= Φ | ¬φ | X φ | φUψ | ♦φ | φ

where Φ, Ψ are state formulas, which describe the paths starting on a given state, and φ, ψ
are path formulas, which describe a particular path, Q is a set of atomic propositions, ./
ranges over predicates {=, ≤, . . . } and p ∈ [0, 1]. The qualitative fragment of pCTL∗ is the
set of formulas where p is restricted to {0, 1}.
Given a pPDA A, we define the semantics of a pCTL∗ formula as follows:
π |= Φ ⇔ π[0] |= Φ

(s, γ) |= >
(s, γ) |= q ⇔ (s, γ) ∈ JqK (q ∈ Q)

(s, γ) |= Φ ∧ Ψ ⇔ (s, γ) |= Φ ∧ (s, γ) |= Ψ
Pr

π |= X φ ⇔ π1 |= φ
π |= φUψ ⇔ ∃i.πi |= ψ ∧ ∀j < i.πj |= φ

(s, γ) |= ¬Φ ⇔ (s, γ) 6|= Φ
(s, γ) |= P(φ) ./ p ⇔

π |= ¬φ ⇔ π 6|= φ

[π |= φ] ./ p

π∼Paths(s,γ)

π |= ♦φ ⇔ ∃i.πi |= φ
π |= φ ⇔ ∀i.πi |= φ

where atomic propositions q are interpreted as JqK ⊆ C. As expected, state formulas are
interpreted in pPDA configurations (s, γ) ∈ C, while path formulas are interpreted in traces
of configurations π ∈ C ω ; π[i] is the ith element in the path π, and πi is the suffix of π
from π[i]. Path formulas describe measurable events in the σ-algebra of cones of C ω , so the
semantics is indeed well-defined [19].
Given a pPDA A, a configuration (s, γ) ∈ C and a pCTL∗ formula Φ, the model-checking
problem is to decide whether (s, γ) |= Φ. The following is known.
I Theorem 15 (Brázdil, Brozek and Forejt [7]). The model-checking problem for pPDAs is
decidable for the qualitative fragment of pCTL∗ .1
1

Formally, this is proven for atomic propositions that are sets of configurations whose stack can be
recognized by a finite automaton. Since our propositions will be configurations with an empty stack,
this is enough for us.

ICALP 2018

XX:14

Almost Sure Productivity

Almost sure productivity states that an event—producing an output—occurs infinitely
often with probability 1. Such properties belong to the qualititative fragment of pCTL∗ .
I Lemma 16. Let (s, γ) ∈ C be an initial configuration and B ⊆ C be a set of configurations.
Then Prπ∈Paths(s,γ) [π visits B infinitely often] = 1 iff (s, γ) |= P( ♦ B) = 1.
Proof. See [6], Lemma 10.46.

J

We will encode language terms as pPDAs and cast almost sure productivity as a qualitative
pCTL∗ property stating that configurations representing output steps are reached infinitely
often with probability 1. Theorem 15 then gives a decision procedure for ASP.

6.2

Modeling streams with pPDAs

The idea behind our encoding from terms to pPDAs is simple to describe. The states of the
pPDA will represent subterms of the original term, and transitions will model steps. In the
original step relation, the only way a subterm can step to a non-subterm is by accumulating
destructors. We use a single-letter stack alphabet to track the number of destructors so
that a term like tailk (e) can be modeled by the state corresponding to e. More formally,
given a stream term e we define a pPDA Ae = (Se , {tl}, Te ), where Se is the set of syntactic
subterms of e and Te is the following transition function:
Te ((σ, a), (e, a)) = 1

Te ((u : e0 , ⊥), (e0 , ε)) = 1

Te ((e1 ⊕p e2 , a), (e1 , a)) = p

Te ((u : e0 , tl), (e0 , ε)) = 1

Te ((e1 ⊕p e2 , a), (e2 , a)) = 1 − p

Te ((tail(e0 ), a), (e0 , tl · a) = 1

where · concatenates strings, and we implicitly treat a as alphabet symbol or a singleton
string. All non-specified transitions have zero probability. We define the set of outputting
configurations as O , {s ∈ C | ∃u, e0 . s = (u : e0 , ⊥)}, that is, configurations where the current
term is a constructor and there are no destructors left to apply. Our main result states that
this set is visited infinitely often with probability 1 if and only if e is ASP. In fact, we prove
something stronger:
I Theorem 17. Let e be a stream term and let Ae be the corresponding pPDA. Then,
Pr [t has infinitely many output nodes] =
t∼JeK

Pr
π∼Paths(e,ε)

[π |= ♦ O].

In particular, e is ASP if and only if (e, ε) |= P( ♦ O) = 1.
Proof. The first part of the proof consists on simplifying the automaton Ae into a new
automaton with a transition function T 0 that is synchronized to the step function for streams
considered in Section 5, while preserving the validity of π |= ♦ O for every path π. The
simplified transition function needs to skip over all states of the form tail(e0 ) or e1 ⊕ e2 until
it reaches a state of the form u : e0 or σ. We proceed in two steps.
1. For every state of the form tailk+1 (e) such that e does not have a tl on top, we add a new
transition from tailk+1 (e) to e so that T 0 ((tailk+1 (e), a), (e, tlk+1 · a)) = 1 and we remove
the transition from tailk+1 (e) to tailk (e). Then we remove unreachable states.
2. States of the form e1 ⊕p e2 are removed, and for every transition from some e to e1 ⊕p e2
such that T ((e, a), (e1 ⊕p e2 , γ)) = q > 0, we add new transitions from e to e1 and e2 so
that T 0 ((e, a), (e1 , γ)) = pq and T 0 ((e, a), (e2 , γ)) = (1 − p)q.

A. Aguirre, G. Barthe, J. Hsu, A. Silva

XX:15

Notice that this step can be removed if we construct a reduced pPDA from the beginning,
the choice of the given construction is motivated by clarity.
Now, the transition function induces a map T : C → D(A × C + C) from configurations to
output distributions over configurations and outputs from one step of the pPDA:
T (σ, γ) , δ(inr(e, γ))
T (e1 ⊕p e2 , γ) , p · T (e1 , γ) + (1 − p) · T (e2 , γ)
T (u : e0 , ε) , δ(inl(u, (e0 , ε)))
T (u : e0 , tl · γ) , T (e0 , γ)
T (tail(e0 ), γ) , T (e0 , tl · γ).
Hence, (C, T ) and (T, st) are coalgebras of the same functor. We can now build a map
f : T → C from terms to configurations:
f (σ) , (σ, ε)
k

f (tail (σ)) , (σ, tlk )
f (e1 ⊕p e2 ) , (e1 ⊕p e2 , ε)
k

f (tail (e1 ⊕p e2 )) , (e1 ⊕p e2 , tlk )
f (û : e0 ) , (û : e0 , ε)
f (tailk (û : e0 )) , (û : e0 , tlk ).
We assume that every primitive term has been replaced by the same constant stream û,
which changes expressivity but not productivity. For every term e, we have
T (f (e)) = case(st(e), inl(a, e1 ) 7→ inl(a, f (e1 )), inr(e2 ) 7→ inr(f (e2 )))
Therefore, f is a coalgebra homomorphism. By finality, this means that for all e ∈ T,
JeK = Paths(f (e)), and so we conclude
Pr [t has infinitely many output nodes] =
t∼JeK

Pr
π∼Paths(f (e))

[π |= ♦ O].
J

By Theorem 15, ASP is decidable for stream terms. In fact, it is also possible to decide
whether a stream term is almost surely not productive, i.e., the probability of producing
infinitely many outputs is zero. Notice that since model-checking pCTL∗ for pPDAs is
2-EXPTIME-hard [7], the syntactic criterion performs far better than the pPDA reduction
whenever it can be applied.

6.3

Extending to trees

Now, we extend our approach to trees. The main difficulty is that since the pPDA can only
simulate one path in the coinductive structure. The problem can be seen in the constructors.
For streams, we can encode the term u : e by proceeding to the tail e. For trees, however,
how can we encode mk(a, e1 , e2 )? The pPDA cannot simulate both e1 and e2 . Since the
failure of ASP may occur down either path, we cannot directly translate the ASP property
on trees to pCTL∗ —ASP is a property of all paths. Instead, on constructors our pPDA
encoding will choose a path at random to simulate. As we will show, if the probability of

ICALP 2018

XX:16

Almost Sure Productivity

choosing a path that outputs infinitely often is 1, then every path will output infinitely often.
Notice that in general, properties that happen with probability 1 do not necessarily happen
for every path, but the structure of our problem allows us to make this generalization.
More formally, the stack alphabet will now be {rt, lt}, and on constructors we transition
to each child with probability 1/2:
Te ((τ, a), (e, a)) = 1
Te ((e1 ⊕p e2 , a), (e1 , a)) = p
Te ((e1 ⊕p e2 , a), (e2 , a)) = 1 − p

Te ((mk(u, el , er ), lt), (el , ε)) = 1
Te ((mk(u, el , er ), rt), (er , ε)) = 1
Te ((left(e0 ), a), (e0 , lt · a)) = 1

Te ((mk(u, el , er ), ⊥), (el , ε)) = 1/2

Te ((right(e0 ), a), (e0 , rt · a)) = 1

Te ((mk(u, el , er ), ⊥), (er , ε)) = 1/2

We define O , {s ∈ C | ∃u, el , er . s = (mk(u, el , er ), ε)} to be the set of outputting configurations. We can characterize ASP with the following theorem:
I Theorem 18. Let e be a tree term and Ae be the corresponding probabilistic PDA. Then
Prπ∼Paths(e,⊥) [π |= ♦ O] = 1 if and only if for every w ∈ {L, R}ω ,
Pr [t has infinitely many output nodes along w] = 1.
t∼JeK

In particular, e is ASP if and only if (e, ε) |= P( ♦ O) = 1.
Proof. The main result we need to prove is that given a distribution µ over OT and the
distribution µ0 over OS induced by µ,
Pr [π |= ♦O] = 1 ⇐⇒ ∀w ∈ {L, R}ω . Pr [π has infinitely many output nodes along w] = 1.

π∼µ0

t∼µ

After this, all that remains is to check that the distribution over the runs of Ae starting on
(e, ε) is exactly µ0 , which is done using similar techniques as in the proof of 17.
We start by showing how to compute this induced distribution. Let F : X 7→ A × X + X
and G : X 7→ A × X × X + X be the functors that generate OS and OT respectively. We
ρ
define a natural transformation G ⇒ DF , which will allow us to transform G-coalgebras into
DF -coalgebras, and in particular OT into D(OS). We assign to every object X a morphism
ρX : GX → DF X as follows:
ρX : A × X × X + X → D(A × X + X)
ρX (inr(x)) = δ(inr(x))
ρX (inl(a, x, y)) = 1/2 · δ(inl(a, x)) + 1/2 · δ(inl(a, y))
This gives us a map f from OT to D(OS) as the unique coalgebra homomorphism closing
the following commutative diagram (in the Kleisli category):
OT

f
◦

◦ρOT ◦ hout,unfi−1

F (OT)

Ff
◦

OS

◦hhead,taili

F (OS)

A. Aguirre, G. Barthe, J. Hsu, A. Silva

XX:17

We can see that, by uniqueness:
f : OT → D(OS)
f unf(x) = D(unf(•))(f (x))
f out(a, x, y) = 1/2 · D(a : •)(f (x)) + 1/2 · D(a : •)(f (y)).
ρ̄

Since D is a monad, we can extend ρ to a natural transformation DG ⇒ DF assigning to
every X a morphism ρ̄X = mF X ◦ DρX , where m is the product of the D monad. Given
a final DG-coalgebra (D(OT), h), we have a DF -algebra (D(OT), ρD(OT) ◦ h) so there is a
unique DF -homomorphism fˆ to the final DF -coalgebra (D(OS), g). This allows us to give
semantics in D(OS) to a tree term:
fˆ
◦

OT
◦h

G(OT)

J−KOS
◦

◦
J−KOT

T

T

◦st

◦ρ̄T ◦ st

◦

G(T)

◦ρ̄(OT)

ρ̄T
◦

OS
◦g

◦

F (T)

F (OS)

F fˆ
◦

F (OT)
Notice that, by uniqueness:
fˆ(M )(E) = (mOS ◦ (Df ))(M )(E) =

Z

Z

t∈OT


χE (π)df (t) dM

π∈OS

where χE is the characteristic function of E ⊆ OS. Now, let
S = {π | π |= ♦ O}
Pπ = {t | tπ ∈ S}
where tπ for π ∈ {L, R}ω is the path in t corresponding to the choices π:
unf(x)L:w = unf(xL:w )
unf(x)R:w = unf(xL:w )
out(a, x, y)L:w = a : xw
out(a, x, y)R:w = a : yw
Then
Z
Pr [π |= ♦ O] =

π∼µ

χS (π)dµ
π∈OS

and
Z
χPπ (t)dµ.

Pr [tπ has infinitely many output nodes] =

t∼µ

t∈OT

The rest of the proof proceeds in three steps. In the following, let U be the distribution
on {L, R}ω assigning probability (1/2)k to every cone generated by a prefix of length k.
First we need the following lemma stating that the distribution induced by f on OS is the
same as the distribution induced by taking paths sampled from U . Intuitively, we are just
pre-sampling the randomness in f from U :

ICALP 2018

XX:18

Almost Sure Productivity

I Lemma 19. Let t ∈ OT. Then
Z
Z
χPw (t)dU =
χS (π)df (t).
w∈{L,R}ω

π∈OS

Proof of Lemma 19. We show that for every measurable B ⊆ OS,
Z
Z
χB (tw )dU =
χB (π)df (t).
w∈{L,R}ω

π∈OS

For any distribution N ∈ D({L, R}ω ), there is an induced distribution by t and N on D(OS):
g : OT → D({L, R}ω ) → D(OS)
g unf(x) N = D(unf(•))(g x N )
R
g out(n, x, y) N = Pr [w[0] = L] · D(n : •)(g x (N |L
tail )) + Pr [w[0] = R] · D(n : •)(g y (N |tail ))
w∼N

w∼N

where N |X
tail is the distribution on the tails of N conditioned to the head being X. (if it
is empty, we just make that side of the sum 0) What we are doing is taking from the first
position of a w sampled from N the randomness for deciding which branch of the tree to
take. In particular, it is easy to see that g t U = f (t). Therefore,
Z
Z
Z
χB (tw )dU =
χB (π)d(g t U ) =
χB (π)df (t).
w∈{L,R}ω

π∈OS

π∈OS


Then following lemma shows that a tree produces paths with infinitely many outputs along
every w in {L, R}ω with probability 1 if and only if it produces paths with infinitely many
outputs along a w sampled from {L, R}ω with probability 1. In other words, it provides a
connection between the universal quantification in the definition of ASP and the probabilistic
nature of pCTL∗ .
I Lemma 20. Let M ∈ D(OT).
Then, the following are equivalent:
R
ω
1. For
R every w
R ∈ {L, R} , OT χPw dM = 1.
2. w∈{L,R}ω OT χPw dM dU = 1.
Proof of Lemma 20. (1 ⇒
R 2) is immediate. To prove (2 ⇒ 1), we suppose that there is
a w ∈ {L, R}ω such thatR OT χPw dM < 1, and we show that
R this must
R also be true for a
ω
W ⊆ {L, R} such that v∈{L,R}ω χW dU > 0, and therefore v∈{L,R}ω OT χPv dM dU < 1.
To do this, we consider the set {wn }n∈N of prefixes of w of length n, and the cones {Cn }n∈N
generated by them. For each of those prefixes wi , we can compute the set of observation
trees Ti such that every t ∈ Ti has i output nodes along wi . This set is measurable (the
union of cones of all finite trees of height i satisfying the conditions), T1 ⊇ T2 ⊇ T3 ⊇ . . . ,
and therefore:
Z
Z
Z
1≥
dM ≥
dM ≥
dM . . .
T1

T2

T3

R
But
since Pw = ∩n Tn , the limit of this sequence is exactly OT χPw dM < 1. Therefore
R
dM < 1 for some k, and so
Tk
Z
Z
Z
Z
Z
Z
χPv dM dU =
χPv dM dU +
χPv dM dU =
v∈Ck

OT

v∈Ck

Z

Tk

v∈Ck

Z

Tkc

Z
χPv dM dU + 0 <

=
v∈Ck

Tk

dU.
v∈Ck

A. Aguirre, G. Barthe, J. Hsu, A. Silva

Hence, we conclude
Z
Z
Z
χPv dM dU =
v∈{L,R}ω

OT

v∈Ck

Z

Z
χPv dM dU +

OT

Z
<

XX:19

χPv dM dU
OT

Z
dU +

v∈Ck

v∈Ckc

Z

dU = 1.
v∈Ckc


Finally we show that given M ∈ D(OT), fˆ(M ) produces paths with infinitely many
outputs with probability 1 if and only if D(OT) is ASP.
I Lemma 21. Let M ∈ D(OT). Then,
Z Z
Z
ω
χS df (t)dM = 1 ⇐⇒ ∀w ∈ {L, R} .
OT

OS

χPw dM = 1.

OT

This is immediate by Lemma 20, Fubini’s theorem and Lemma 19.
J

7

Possible Generalizations and Extensions

Our definition of ASP and our verification approaches suggest several natural directions for
future investigation. We believe that some extensions can be handled without too much
trouble; however, other generalizations may require new ideas.
Handling Richer Languages The most concrete direction is to consider richer languages for
coinductive probabilistic programming. Starting from our core language, one might consider
allowing more operations on coinductive terms, mutually recursive definitions, or conditional
tests of some kind. It should also be possible to develop languages for more complex
coinductive types associated with general polynomial functors (see, e.g., Kozen [27]). Note
that adding more operations, e.g. point-wise + of streams would increase the expressivity
of the language but have additional challenges from the perspective of the semantics – we
would have to add extra structure to the base category and re-check that the finality proof
still works.
Developing new languages for coinductive probabilistic programming—perhaps an imperative language or a higher-order language—would also be interesting. From the semantics
side, our development in Section 3 should support any language equipped with a small-step
semantics producing output values, allowing ASP to be defined for many kinds of languages.
The verification side appears more challenging; our techniques are specialized to our core
language. Natural extensions, like a pointwise addition operation, already seem to pose
challenges for the analyses. As of now, we know of no general method to reasoning about
ASP. This stands in sharp contrast to almost sure termination, which can be established by
where flexible criteria like decreasing probabilistic variants [20]. Considering counterparts of
these methods for ASP is an interesting avenue of research.
Exploring Other Definitions Our definition of ASP is natural, but other definitions are
possible. For trees (and possibly more complex coinductive structures), we could instead
require that there exists a path producing infinitely many outputs, rather than requiring
that all paths produce infinitely many outputs. This weaker notion of ASP can be defined in
our semantics, but it is currently unclear how to verify this kind of ASP.

ICALP 2018

XX:20

Almost Sure Productivity

Our notion of ASP also describes just the probability of generating infinitely many outputs,
and does not impose any requirement on the generation rate. Quantitative strengthenings of
ASP—say, requiring bounds on the expected number of steps between outputs—could give
more useful information.
Understanding Dependence on Step Relation Our coalgebraic semantics supporting our
verification methods are based on a small-step semantics for programs. A natural question is
whether this dependence is necessary, or if one could verify ASP with a less step-dependent
semantics. Again drawing an analogy, it appears that fixing a reduction strategy is important
in order to give a well-defined notion of almost sure termination for probabilistic higher-order
languages (see, e.g., [29]). The situation for almost sure productivity is less clear.

8

Related Work

Our work draws inspiration from two previously independent lines of research: probabilistic
termination and productivity of coalgebraic definitions.
Probabilistic Termination There are a broad range of techniques for proving termination
of probabilistic programs. Many of the most powerful criteria use advanced tools from
probability theory [31], especially martingale theory [9, 18, 10, 11, 12]. Other works adopt
more pragmatic approaches, generally with the goal of achieving automation. Arons, Pnueli
and Zuck [4] reduce almost sure termination of a program P to termination of a nondeterministic program Q, using a planner that must be produced by the verifier. Subsequent
work by Esparza, Gaiser and Kiefer [17] give a CEGAR-like approach for building patterns—
which play a role similar to planners—and proving that their approach is complete for a
natural class of programs.
Productivity of Corecursive Definitions There has been a significant amount of work on
verifying productivity of corecursive definitions, without probabilistic choice. Endrullis and
collaborators [16] give a procedure for deciding productivity of an expressive class of stream
definitions. In a companion work [15], they study the strength of data oblivious criteria, i.e.,
criteria that do not depend on values. More recently, Komendantskaya and collaborators [24]
define the notion of observational productivity and give a semi-decision procedure for logic
programs.

9

Conclusion

We introduce almost sure productivity, a counterpart to almost sure termination for probabilistic coinductive programs. In addition, we propose two methods for proving ASP for
a core language for streams and infinite trees. Our results demonstrate that verification of
ASP is feasible and can even be decidable for simple languages. Our work can be seen as
an initial exploration into productivity and probabilistic coalgebraic definitions, with many
avenues for extensions to more complex languages and generalizations to other datatypes.
References
1

Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors,
ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL),

A. Aguirre, G. Barthe, J. Hsu, A. Silva

2

3

4

5
6
7

8

9

10

11

12

13

XX:21

Rome, Italy, pages 27–38, 2013. URL: http://doi.acm.org/10.1145/2429069.2429075,
doi:10.1145/2429069.2429075.
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. Lexicographic ranking
supermartingales: an efficient approach to termination of probabilistic programs. Proceedings of the ACM on Programming Languages, 2(POPL):34:1–34:32, 2018. URL:
http://doi.acm.org/10.1145/3158122, doi:10.1145/3158122.
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak
Garg. Relational reasoning for Markov chains in a probabilistic guarded lambda calculus.
In European Symposium on Programming (ESOP), Thessaloniki, Greece, Lecture Notes in
Computer Science. Springer-Verlag, 2018.
Tamarah Arons, Amir Pnueli, and Lenore D. Zuck. Parameterized verification by probabilistic abstraction. In Andrew D. Gordon, editor, Foundations of Software Science and
Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of
the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw,
Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science,
pages 87–102. Springer-Verlag, 2003. URL: https://doi.org/10.1007/3-540-36576-1_6,
doi:10.1007/3-540-36576-1_6.
Kazuoki Azuma. Weighted sums of certain dependent random variables. Tohoku Mathematical Journal, 19(3):357–367, 1967.
Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
Tomás Brázdil, Václav Brozek, and Vojtech Forejt. Branching-time model-checking of probabilistic pushdown automata. Electronic Notes in Theoretical Computer Science, 239:73–83,
2009. URL: https://doi.org/10.1016/j.entcs.2009.05.031, doi:10.1016/j.entcs.
2009.05.031.
Venanzio Capretta and Jonathan Fowler. The continuity of monadic stream functions. In
IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, pages 1–12,
2017. URL: https://doi.org/10.1109/LICS.2017.8005119, doi:10.1109/LICS.2017.
8005119.
Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with
martingales. In International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia, pages 511–526, 2013. URL: https://www.cs.colorado.edu/~srirams/
papers/cav2013-martingales.pdf.
Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through Positivstellensatz’s. In International Conference on
Computer Aided Verification (CAV), Toronto, Ontario, volume 9779 of Lecture Notes in
Computer Science, pages 3–22. Springer-Verlag, 2016. URL: https://doi.org/10.1007/
978-3-319-41528-4_1, doi:10.1007/978-3-319-41528-4_1.
Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Saint Petersburg, Florida, pages 327–342, 2016. URL: https:
//doi.acm.org/10.1145/2837614.2837639, doi:10.1145/2837614.2837639.
Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić. Stochastic invariants for probabilistic termination. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pages 145–160, 2017. URL: https://doi.acm.
org/10.1145/3009837.3009873, doi:10.1145/3009837.3009873.
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. The guarded
lambda-calculus: Programming and reasoning with guarded recursion for coinductive types.
Logical Methods in Computer Science, 12(3), 2016. URL: https://doi.org/10.2168/
LMCS-12(3:7)2016, doi:10.2168/LMCS-12(3:7)2016.

ICALP 2018

XX:22

Almost Sure Productivity

14
15

16

17

18

19

20

21

22

23

24

25

Rick Durrett. Probability: Theory and Examples. Cambridge University Press, 2010.
Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks. Data-oblivious stream productivity. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR),
Doha, Qatar, volume 5330 of Lecture Notes in Computer Science, pages 79–96. SpringerVerlag, 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_6, doi:10.1007/
978-3-540-89439-1_6.
Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem
Klop. Productivity of stream definitions. Theoretical Computer Science, 411(4-5):765–782,
2010. URL: https://doi.org/10.1016/j.tcs.2009.10.014, doi:10.1016/j.tcs.2009.
10.014.
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic
programs using patterns. In P. Madhusudan and Sanjit A. Seshia, editors, International
Conference on Computer Aided Verification (CAV), Berkeley, California, volume 7358 of
Lecture Notes in Computer Science, pages 123–138. Springer-Verlag, 2012. URL: https:
//doi.org/10.1007/978-3-642-31424-7_14, doi:10.1007/978-3-642-31424-7_14.
Luis María Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In Sriram K. Rajamani and David Walker, editors, ACM
SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pages 489–501, 2015. URL: http://doi.acm.org/10.1145/2676726.2677001,
doi:10.1145/2676726.2677001.
Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal
Asp. Comput., 6(5):512–535, 1994. URL: https://doi.org/10.1007/BF01211866, doi:
10.1007/BF01211866.
Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent program. ACM Transactions on Programming Languages and Systems, 5(3):356–380, 1983.
URL: http://doi.acm.org/10.1145/2166.357214, doi:10.1145/2166.357214.
John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Hans-Juergen Boehm and Guy L. Steele Jr., editors, ACM
SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 410–423, 1996. URL: http://doi.acm.org/10.1145/
237721.240882, doi:10.1145/237721.240882.
Benjamin Lucien Kaminski and Joost-Pieter Katoen. On the hardness of almost-sure
termination. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Symposium on Mathematical Foundations of Computer Science (MFCS), Milan,
Italy, volume 9234 of Lecture Notes in Computer Science, pages 307–318. SpringerVerlag, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_24, doi:10.1007/
978-3-662-48057-1_24.
Henning Kerstan and Barbara König. Coalgebraic trace semantics for continuous probabilistic transition systems. Logical Methods in Computer Science, 9(4), 2013. URL:
https://doi.org/10.2168/LMCS-9(4:16)2013, doi:10.2168/LMCS-9(4:16)2013.
Ekaterina Komendantskaya, Patricia Johann, and Martin Schmidt. A productivity checker
for logic programming. In Manuel V. Hermenegildo and Pedro López-García, editors, International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR),
Edinburgh, Scotland, volume 10184 of Lecture Notes in Computer Science, pages 168–
186. Springer-Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-63139-4_10,
doi:10.1007/978-3-319-63139-4_10.
Dexter Kozen. Semantics of probabilistic programs. Journal of Computer and System
Sciences, 22(3):328–350, 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2,
doi:10.1016/0022-0000(81)90036-2.

A. Aguirre, G. Barthe, J. Hsu, A. Silva

26

27

28

29

30

31

32

XX:23

Dexter Kozen. A probabilistic PDL. In David S. Johnson, Ronald Fagin, Michael L.
Fredman, David Harel, Richard M. Karp, Nancy A. Lynch, Christos H. Papadimitriou,
Ronald L. Rivest, Walter L. Ruzzo, and Joel I. Seiferas, editors, ACM SIGACT Symposium
on Theory of Computing (STOC), Boston, Massachusetts, pages 291–297, 1983. URL:
http://doi.acm.org/10.1145/800061.808758, doi:10.1145/800061.808758.
Dexter Kozen. Realization of coinductive types. Electronic Notes in Theoretical Computer
Science, 276:237–246, 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.024,
doi:10.1016/j.entcs.2011.09.024.
Antonín Kucera, Javier Esparza, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2(1), 2006. URL: https://doi.
org/10.2168/LMCS-2(1:2)2006, doi:10.2168/LMCS-2(1:2)2006.
Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized
typing. In Hongseok Yang, editor, European Symposium on Programming (ESOP), Uppsala,
Sweden, volume 10201 of Lecture Notes in Computer Science, pages 393–419. SpringerVerlag, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_15, doi:10.1007/
978-3-662-54434-1_15.
David A. Levin, Yuval Peres, and Elizabeth L. Wilmer. Markov Chains and Mixing
Times. American Mathematical Society, 2009. URL: https://pages.uoregon.edu/
dlevin/MARKOV/markovmixing.pdf.
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen.
A new proof rule for almost-sure termination. Proceedings of the ACM on Programming
Languages, 2(POPL):33:1–33:28, 2018. URL: http://doi.acm.org/10.1145/3158121,
doi:10.1145/3158121.
Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers.
ACM Transactions on Programming Languages and Systems, 18(3):325–353, 1996. URL:
http://doi.acm.org/10.1145/229542.229547, doi:10.1145/229542.229547.

ICALP 2018

