#  Abstract Hidden Markov Models:
a monadic account of quantitative information flow

Annabelle McIver  Dept. Computing
Macquarie University.
Sydney, Australia<EMAIL_ADDRESS>,  Carroll Morgan  School of
Comp. Sci. and Eng.
Univ. New South Wales, and Data61.
Sydney, Australia<EMAIL_ADDRESS>and  Tahiry Rabehaja  Dept.
Computing
Macquarie University.
Sydney, Australia<EMAIL_ADDRESS>
###### Abstract.

Hidden Markov Models, HMM’s, are mathematical models of Markov processes with
state that is hidden, but from which information can leak. They are typically
represented as 3-way joint-probability distributions.

We use HMM’s as denotations of probabilistic hidden-state sequential programs:
for that, we recast them as “abstract” HMM’s, computations in the Giry monad
${\mathbb{D}}$, and we equip them with a partial order of increasing security.
However to encode the monadic type _with hiding_ over some state ${\cal X}$ we
use ${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$
rather than the conventional ${\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}{\cal
X}$ that suffices for Markov models whose state is not hidden. We illustrate
the ${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$
construction with a small Haskell prototype.

We then present _uncertainty measures_ as a generalisation of the extant
diversity of probabilistic entropies, with characteristic analytic properties
for them, and show how the new entropies interact with the order of increasing
security. Furthermore, we give a “backwards” uncertainty-_transformer_
semantics for HMM’s that is dual to the “forwards” abstract HMM’s — it is an
analogue of the duality between forwards, relational semantics and backwards,
predicate-transformer semantics for imperative programs with demonic choice.

Finally, we argue that, from this new denotational-semantic viewpoint, one can
see that the Dalenius desideratum for statistical databases is actually an
issue in compositionality. We propose a means for taking it into account.

###### Key words and phrases:

Abstract Hidden Markov Models, Giry Monad, Quantitative Information Flow.

##  1\. Introduction

###  1.1. Setting and overview

We can represent probabilistic sequential programs with hidden state as Hidden
Markov Models, i.e. HMM’s 111We use apostrophe uniformly between acronyms and
suffixes, even when they are not possessive. formulated as probabilistic
mechanisms that take prior, input probability distributions and give posterior
distributions over (leaked) observations and final state. Here, however, we
recast HMM’s as computations over the Giry monad, making them more suitable
for denotational semantics. Indeed the monadic view of simple Markov processes
in particular is well established [1, 2], using ${\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}{\cal X}$ where type-constructor
${\mathbb{D}}$ makes distributions on its base type ${\cal X}$; the Kleisli
extension is then of type ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}{\cal X}$, representing the action of
multiplying an initial-state-distribution vector by a Markov matrix. But that
simplicity cannot account for hidden state and information flow.

We treat hidden state by beginning with ${\mathbb{D}}{\cal X}$ (not ${\cal
X}$): the computation type we obtain is then “one level up”, of type
${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$, the
Kleisli extension is ${\mathbb{D}}^{2}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$; and we call the double-
distribution type ${\mathbb{D}}^{2}{\cal X}$ _hyper-distributions_ , or
“hypers” for short.

Although the Giry monad is formulated in terms of general measures [2], we
will need only discrete distributions for matrix-based HMM’s. Nevertheless, we
give our constructions and results in more general terms, anticipating e.g.
infinite sequences of HMM’s, nondeterminism, and iterations for which proper
measures will be necessary [3].

In earlier work, we have used the hypers ${\mathbb{D}}^{2}{\cal X}$, equipped
with a partial order of increasing security, to establish compositionality
results [4], to explore the effect of including demonic nondeterminism [5] and
to give an abstract treatment of probabilistic channels [6, 7]. A second
earlier theme has been the generalisation of entropies (such as Shannon) to a
more abstract setting where only their essential properties are preserved [4,
8, 5, 7]. Here we use monads to bring all those separate strands together and
to go further.

One major further step is to show that there is a dual, backwards view for
abstract HMM’s, based on “uncertainty” _transformers_ that transform post-
uncertainty measures into pre- uncertainty measures where, in turn,
_uncertainty measures_ generalise probabilistic entropies.

We and others have argued that specific entropies (e.g. Shannon) have
limitations in security work generally [9, 4]. Therefore we focus here on
their essential properties: continuity and concavity. That view is supported
by powerful theorems that such a generalisation supports, and a methodological
criterion that uncertainty measures capture contexts in a way that individual
styles of entropy cannot.

A second further step is to extend our recent treatment [7] of the _Dalenius
Desideratum_ , the “collateral” leakage of information due to unknown
correlations with third-party data, from merely channels (a “read only”
scenario [10, 11], such as access to a statistical database) to programs that
might alter the database (thus “read/write” as well). The Dalenius perspective
here is the fact that care must be taken wrt. compositionality in a context
containing extra variables even when a program fragment does not explicitly
refer to them[4].

_To remain accessible to a broader security community_ , we do not begin from
Giry: rather we first work in elementary terms. In §7 the monadic structures
will be seen to have informed our earlier definitions and theorems.

###  1.2. Principal contributions and aims: summary

Our principal contributions are these, in which the new constructions and
results are given in bold:

— We note that (finite) classical HMM’s are a model for straight-line
sequential probabilistic programs with hidden state — We formulate _abstract
HMM’s_ over a state as a monadic model for HMM’s over that same state, and
give their characteristic properties.

— We formulate _uncertainty measures_ as a generalisation of diverse entropies
(top centre), and give their characteristic properties. 222They were studied,
but less extensively, as “disorders”, in [5].

— We note that uncertainty measures have a complete representation based on
real-valued functions of state and adversarial strategy.

— We give a dual, uncertainty-transformer semantics of HMM’s and prove the
duality.

— We show how all of the above is an instance of the general Giry monad as a
computation, of which (finite) HMM’s use a discrete portion.

— We explain how the “Dalenius effect” is manifested as a compositional issue
in this framework, and how it can be treated.

In other sections we review abstract channels (§2.2), hyper-distributions
(§2.3) and the security order (§6) on hypers.

We believe that Thm. 33, in particular its assumptions and proof, is a
significant new result.

Our principal aims are these:

— (More abstract) To construct forward- and dual backward semantic spaces for
probabilistic sequential computations over hidden state, using monadic
computations and partial (refinement) orders in this new context, and we
formulate and prove the general properties that make them suitable for
embedding finite (for the moment) HMM’s.

— (More concrete) To provide the basis for a source-level reasoning method,
analogous to Hoare logic or weakest preconditions, for quantitative non-
interference in sequential programs. For this, the dual, transformer semantics
for HMM’s seems to be a necessary first step, together with a link between the
social aspects of security and the mathematical behaviour of a program (§11).

The conclusion §14 discusses the benefits of doing this.

###  1.3. General notations — see also §A

Application of function $f$ to argument $x$ is written $f.x$ to reduce
parentheses. It associates to the left.

Although a matrix $M$ with rows, columns indexed by $R,C$ is a function
$R{\times}C\mathbin{\rightarrow}{\mathbb{R}}$, we avoid constant reference to
the reals ${\mathbb{R}}$ by writing just $R{\mathbin{\rightarrowtriangle}}C$
for that type; similarly we write the type of a vector over $X$ as
$\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{X}}$.
We write $M_{r,c}$ for the element of matrix $M$ indexed by row $r$ and column
$c$; then the $r$-th row of $M$ is $M_{r,-}$; and the $c$-th column is
$M_{-,c}$, of types
$\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{Y}},\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{X}}$
resp. For row- or column vector
$v{{:}\,}{\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{I}}}$
we write $v_{i}$ for its $i$-th element. Thus e.g. we have
${(M_{-,c})}_{r}{=}M_{r,c}$.

When multiplying vectors and matrices we assume without comment that the
vector has been oriented properly, i.e. as a row or column as required. Thus
$v$ acts as a row in $v{\mathbin{\cdot}}M$ but as a column in
$M{\mathbin{\cdot}}v$. Thus for
$v{{:}\,}\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{X}}$
and $M{{:}\,}X{\mathbin{\rightarrowtriangle}}Y$ the matrix product
$v{\mathbin{\cdot}}M$ is in
$\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{Y}}$,
where here we are using dot $(\cdot)$ for matrix multiplication.
Multiplication of scalars will usually be juxtaposition, but occasionally
$\times$ when we are avoiding ambiguity.

We write for example $x{{:}\,}X$, i.e. with a colon, when we are introducing a
fresh variable $x$ into the discussion at that point; with $x{\in}X$ we are
instead stating a property of some $x$ and $X$ that have been already
introduced at some earlier point. 333For example we could write “Because we
have already established that $s{\in}{\mathbb{P}}X$, we know that for any
$x{{:}\,}s$ we have $x{\in}X$.” Both $s,X$ are defined in the surrounding
text, but $x$ here is a local (i.e. bound) variable just used temporarily.
That means in the former case that one need not search backwards to see what
$x$ is being referred to (and in the latter case, one might).

Other specific notations are explained at first use, and (as noted above) a
full glossary in occurrence order is given in §A.

##  2\. Abstract channels and hyper-distributions

We now review abstract channels as a conceptual stepping-stone to hyper-
distributions — recall they are “hypers” for short. (Channels are the special
case of HMM’s where the state is not updated.)

###  2.1. Channels and distributions as matrices and vectors

A _channel_ is a (stochastic) matrix of non-negative reals with 1-summing
rows; we use upper-case Roman letters like $C$ for them. The rows are labelled
with elements from some set ${\cal X}$; and the columns from some set ${\cal
Y}$. Thus a channel typically has type ${\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$; here, both ${\cal X}$ and ${\cal
Y}$ will be finite.

A distribution in ${\mathbb{D}}{\cal X}$ can be presented as a 1-summing
vector in
$\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{{\cal
X}}}$, usually lower-case Greek: generally $\delta$ for “distribution”, but
especially $\pi$ for prior and sometimes $\rho$ for posterior.

######  Definition 1.

Weight Let $M$ or $v$ be a matrix or vector resp. Then
$\textrm{$\footnotesize\Sigma$}M$ or $\textrm{$\footnotesize\Sigma$}v$ is its
_weight_ , the sum $\textrm{$\footnotesize\Sigma$}_{x,y}M_{x,y}$ or
$\textrm{$\footnotesize\Sigma$}_{x}v_{x}$ taken over all its indices. $\Box$

Thus e.g. we have
$\textrm{$\footnotesize\Sigma$}M_{x,-}=\textrm{$\footnotesize\Sigma$}_{y}M_{x,y}$
and that $M$ is stochastic (i.e. represents a channel) just when
$\textrm{$\footnotesize\Sigma$}M_{x,-}$ is 1 for all $x$.

Each row $C_{x,-}$ of a channel $C$ is a conditional probability distribution
over ${\cal Y}$ given that particular $x{{:}\,}{\cal X}$. That is, the $y$-th
element $C_{x,y}$ of $C_{x,-}$ is the probability that $C$ takes input $x$ to
output $y$.

###  2.2. Informal channel semantics: _abstract_ channels

A (1-summing) prior $\pi$ and (stochastic) channel $C$ together determine a
joint distribution as follows.

######  Definition 2.

Channel applied to prior Given a prior
$\pi{{:}\,}{\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{{\cal
X}}}}$ and channel $C{{:}\,}{\cal X}{\mathbin{\rightarrowtriangle}}{\cal Y}$
we write $\pi{\rhd}C$ for the joint-distribution matrix of type ${\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ resulting from _applying_ the
channel to the prior, defined $(\pi{\rhd}C)_{x,y}{:=}\,\pi_{x}C_{x,y}$. (Here
juxtaposition is ordinary multiplication of reals.) $\Box$

Note that matrix $\pi{\rhd}C$ is not stochastic: rather because $C$ itself is
stochastic we have
$\textrm{$\footnotesize\Sigma$}(\textrm{$\footnotesize\Sigma$}(\pi{\rhd}C)_{x,-})=\textrm{$\footnotesize\Sigma$}\pi_{x}=1$.

A non-zero vector is normalised as follows.

######  Definition 3.

Normalisation Let
$\delta{{:}\,}{\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{{\cal
X}}}}$ be such that $0{\neq}\textrm{$\footnotesize\Sigma$}\delta$. Then the
_normalisation_ $\lfloor\delta\rfloor$ of $\delta$ is given by
$\lfloor\delta\rfloor_{x}{:=}\,\delta_{x}/\textrm{$\footnotesize\Sigma$}\delta$
for each $x{{:}\,}{\cal X}$. $\Box$

Now for some
$\pi{{:}\,}\stackrel{{\scriptstyle\raisebox{-1.5pt}[0.0pt][0.0pt]{$\rightarrowtriangle$}}}{{{\cal
X}}}$ and channel $C{{:}\,}{\cal X}{\mathbin{\rightarrowtriangle}}{\cal Y}$
define joint distribution $J{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ by $J{=}\pi{\rhd}C$. The (marginal)
probability of each output $y{{:}\,}{\cal Y}$ is
$\textrm{$\footnotesize\Sigma$}J_{-,y}$ and, associated with each $J$, there
is a posterior distribution $\lfloor J_{-,y}\rfloor$ on ${\cal X}$.

Abstracting from the $y$-values, but retaining the link between the marginal
probabilities and the posterior distributions, gives an informal description
of our intended “abstract channel” semantics [6]. We make this precise in
§2.4.

###  2.3. Hypers abstract from joint distributions

The joint-distribution matrix $J{=}\pi{\rhd}C$ contains “too much” information
if we do not need the actual value of $y$ that led to a particular posterior.
Abstracting from those output values leads us to a representation of the
possible posteriors on their own, retaining however the probability with which
they occur (in fact the marginal probability of the value $y$ that produced
each one). The advantage we take from that is that HMM’s acquire a monadic
structure, acting as Kleisli maps, and furthermore can express other
probabilistic notions in a way more suited to calculation: for example,
conditional entropies become expected values (of the entropies) over the
distribution of posteriors.

More intuitive reasons for the abstraction include that it is appropriate in
security to consider the information leakage of a channel $C$ wrt. a prior
$\pi$ to concern only what an adversary can discover about $\pi$, and not the
actual observations that led to that discovery: whether a spy’s vocabulary is
“da/nyet” or “yes/no”, or indeed whether “yes” means “it’s zero” or “it’s
one”, does not affect the information-theoretic threat that spy represents,
provided of course that the spy and her controller have agreed on the
vocabulary beforehand.

We can abstract from the observations in $\pi{\rhd}C$ as follows. If column
$y$ of $J=\pi{\rhd}C$ is all zero, then that $y$ will never occur (for any
prior); thus we can omit that column.

And if two columns $y_{1,2}$ of $J$ are proportional to each other, i.e. are
_similar_ (as for triangles), then we can add them together, since for a given
prior the same posterior will be inferred for $y_{1}$ as for $y_{2}$ and the
overall probability of inferring that posterior will be the sum of the
marginal probabilities for $y_{1,2}$. 444For brevity we write $y_{1,2}$ rather
than $y_{1},y_{2}$.

Finally, a 1-1 renaming of the $y$-values has no effect on the posteriors and
their respective probabilities; so we can remove those names as long as we
retain the distinction between separate (non-zero, non-similar) columns.

Abstracting from all that arguably inessential information (about $y$) leaves
only a distribution of posteriors on ${\cal X}$ and, for us, this is the
semantic view. Writing in general ${\mathbb{D}}{\cal X}$ for 1-summing
functions of type ${\cal X}{\mathbin{\rightarrow}}{\mathbb{R}}^{\geq}$, a
discrete distribution over ${\cal X}$ has type ${\mathbb{D}}{\cal X}$ and so a
discrete distribution of such distributions has type
${\mathbb{D}}({\mathbb{D}}{\cal X})$ that is ${\mathbb{D}}^{2}{\cal X}$. Those
latter are our hypers, and they are our abstraction of joint distributions
${\cal X}{\mathbin{\rightarrowtriangle}}{\cal Y}$.

The values of type ${\mathbb{D}}{\cal X}$ are called the _inners_ of a hyper,
and the _outer_ distribution of a hyper is its distribution over those inners:
that is, a hyper on ${\cal X}$ is a (single) outer distribution over (possibly
many) inners, and each inner is a (single) distribution over ${\cal X}$
itself.

As an example, recall the famous puzzle of _Bertrand’s Boxes_. Three identical
boxes contain two balls each: one has two white balls; one has two black
balls; and the remaining box has one of each. It is not known which box is
which; and one of them is chosen randomly. A ball is drawn at random from it,
and it is white. What is the probability that the other ball in that box is
also white? We reason as follows.

The state space is ${\cal X}{=}\\{0,1,2\\}$, referring to the number of white
balls in each box. The prior distribution in ${\mathbb{D}}{\cal X}$ is
uniform, which we can write
$(\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}})$. The HMM is a
channel that takes input $x$ to the distribution
$(\textit{white}\mapsto\nicefrac{{x}}{{2}},\textit{black}\mapsto
1{-}\nicefrac{{x}}{{2}})$. The joint distribution $p$ say, of type
${\mathbb{D}}({\cal X}{\times}\\{\textit{white},\textit{black}\\})$, would be
such that
$p(1,\textit{white})=\nicefrac{{1}}{{3}}{\times}\nicefrac{{1}}{{2}}=\nicefrac{{1}}{{6}}$,
the probability that Box 1 was chosen and that the ball taken from it was
white. The overall probability that a white ball is taken (from whichever box)
is the white-marginal
$0{+}\nicefrac{{1}}{{6}}{+}\nicefrac{{1}}{{3}}=\nicefrac{{1}}{{2}}$ (which is
obvious from symmetry anyway), and the posterior distribution on ${\cal X}$ is
in that case $(0,\nicefrac{{1}}{{3}},\nicefrac{{2}}{{3}})$ — which nicely
solves the puzzle. The posterior probability that $x{=}2$ is
$\nicefrac{{2}}{{3}}$ given that a white is taken and, by the way, a white is
taken with overall probability $\nicefrac{{1}}{{2}}$ (the marginal). And for
that reasoning of course the value of the observation, the colour of the drawn
ball, is used.

But now suppose instead you wanted to know only the decrease in Shannon
entropy resulting from that experiment. Beforehand the entropy is
$H(\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}})=\log_{2}3=1.58$
(approximately). Afterwards, it will be the _conditional_ Shannon entropy of
the distribution of posteriors, calculated by taking the expected value of
$H()$ over the distribution of posteriors: and that is approximately

$\nicefrac{{1}}{{2}}{\times}H(0,\nicefrac{{1}}{{3}},\nicefrac{{2}}{{3}})+\nicefrac{{1}}{{2}}{\times}H(\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}},0)\hskip
10.00002pt=\hskip
10.00002pt\nicefrac{{1}}{{2}}{\times}0.92+\nicefrac{{1}}{{2}}{\times}0.92\hskip
10.00002pt=\hskip 10.00002pt0.92\quad,$ (1)

so that $1.58{-}0.92=\nicefrac{{2}}{{3}}$ (exactly) of a bit has been leaked.
And we did not need colours for that: the calculation is done entirely with
the hyper-distribution, that is with the distribution

$\textrm{the
{outer}}\left\\{~{}\begin{array}[]{rcl}\nicefrac{{1}}{{2}}&\mapsto&(0,\nicefrac{{1}}{{3}},\nicefrac{{2}}{{3}})\\\
\nicefrac{{1}}{{2}}&\mapsto&(\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}},0)\end{array}~{}\right\\}\textrm{the
{inners}}$

_of distributions_ , i.e. of posteriors: a hyper-distribution. The
$\nicefrac{{1}}{{2}}$’s are the marginals, and the $({\cdots})$ are the
posteriors associated with each. We call the channel-output marginal the
_outer_ , and the posteriors the _inners_.

Seeing this example as a security leak, we might imagine that the adversary is
trying to guess the colour of the other ball in the box: in that case she
would look at the colour she took and then guess that same colour. To describe
that we use a different entropy $V_{1}$, called _Bayes Vulnerability_ , which
is the probability the secret can be guessed in one try by an optimal
adversary. Obviously she will guess the $x$-value with the largest probability
in the posterior (the inner), and her conditional probability of guessing
correctly is

$\nicefrac{{1}}{{2}}{\times}V_{1}(0,\nicefrac{{1}}{{3}},\nicefrac{{2}}{{3}})+\nicefrac{{1}}{{2}}{\times}V_{1}(\nicefrac{{2}}{{3}},\nicefrac{{1}}{{3}},0)\hskip
10.00002pt=\hskip
10.00002pt\nicefrac{{1}}{{2}}{\times}\nicefrac{{2}}{{3}}+\nicefrac{{1}}{{2}}{\times}\nicefrac{{2}}{{3}}\hskip
10.00002pt=\hskip 10.00002pt\nicefrac{{2}}{{3}}\quad.$

That’s no surprise — but what is worth noting is that we used the _same_
hyper-distribution for the $V_{1}$ calculation just above as for the $H$
calculation at (1). That is the utility of the abstraction: that the hyper
contains enough information to handle many entropies one might use to measure
leakage.

###  2.4. The semantic function from joints to hypers

In this section we define precisely the denotation $[\\![J]\\!]$ in
${\mathbb{D}}^{2}{\cal X}$ of a joint-distribution matrix $J{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$.

######  Definition 4.

Sub-distribution, sup-hyper A discrete sub-distribution over a set ${\cal X}$
is a function of type ${\cal X}{\mathbin{\rightarrow}}[0,1]$ that sums to _no
more than 1_ ; we write that type as $\underline{{\mathbb{D}}}{\cal X}$.
(Recall that a _proper_ distribution in ${\mathbb{D}}{\cal X}$ sums to exactly
1, and thus ${\mathbb{D}}{\cal X}\subseteq\underline{{\mathbb{D}}}{\cal X}$.)

Similarly a discrete sub-_hyper_ over a set ${\cal X}$ is a sub-distribution
over the (proper, inner) distributions ${\mathbb{D}}{\cal X}$, thus of type
$\underline{{\mathbb{D}}}({\mathbb{D}}{\cal X})$; only the outer of a sub-
hyper can sum to less than 1. We write that type as
$\underline{{\mathbb{D}}^{2}}{\cal X}$. (Note that the inners of a sub-hyper
are proper distributions.) $\Box$

######  Definition 5.

One- and two-point distributions For $z,z^{\prime}{{:}\,}{\cal Z}$ in general
we write $[z]$ for the _point distribution_ on $z$, viz. assigning probability
1 to $z$ and 0 to all other elements of ${\cal Z}$. 555Function $[\cdot]$ is
the unit $\eta$ of the ${\mathbb{D}}$-monad: see §7.  We write
$z{\mathbin{{}_{p}\kern-0.50003pt\oplus}}z^{\prime}$ for the two-point
distribution that assigns $p$ to $z$ and $1{-}p$ to $z^{\prime}$ and 0 to
everything else in ${\cal Z}$. $\Box$

Thus $z\,{\mathbin{{}_{1}\kern-0.50003pt\oplus}}\,z^{\prime}=[z]$ and
$z\,{\mathbin{{}_{0}\kern-0.50003pt\oplus}}\,z^{\prime}=[z^{\prime}]$.

######  Definition 6.

Point sub-hyper For sub-distribution
$\delta{{:}\,}\underline{{\mathbb{D}}}{\cal X}$ the _point sub-hyper_
$\underline{[\delta]}$ in $\underline{{\mathbb{D}}^{2}}{\cal X}$ has weight
$\textrm{$\footnotesize\Sigma$}\delta$ concentrated on the single (inner)
distribution $\lfloor\delta\rfloor$, provided of course that
$\textrm{$\footnotesize\Sigma$}\delta{\neq}0$. If
$\textrm{$\footnotesize\Sigma$}\delta{=}0$ then $\underline{[\delta]}$ is the
(unique) weight-zero sub-hyper.

That is, the argument $\delta$ is normalised to make the inner, and its weight
becomes the (one-point) sub-outer on that inner. $\Box$

Note that when $\textrm{$\footnotesize\Sigma$}\delta=1$ we have
$\underline{[\delta]}=[\delta]$.

We now define the semantic function itself:

######  Definition 7.

Joint-distribution denotes hyper Let $J{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ satisfy
$1{=}\textrm{$\footnotesize\Sigma$}J$ so that it describes a discrete (proper)
joint distribution in ${\mathbb{D}}({\cal X}{\times}{\cal Y})$. Then its
abstraction [[J]] to a hyper in ${\mathbb{D}}^{2}{\cal X}$ is given by

$[\\![J]\\!]\hskip 10.00002pt=\hskip 10.00002pt\sum_{y{\in}{\cal
Y}}\underline{[J_{-,y}]}\quad,$

with summation $\textrm{$\footnotesize\Sigma$}_{y{\in}{\cal Y}}$ therefore
being an addition of sub-hypers, i.e. sub-distributions on ${\mathbb{D}}{\cal
X}$. Each column $J_{-,y}$ is regarded as a sub-distribution in
$\underline{{\mathbb{D}}}{\cal X}$, and then $\underline{[-]}$ converts it to
a sub-point hyper. $\Box$

Note that in Def. 7 any all-zero columns in $J$ are automatically ignored,
since they become zero-weight sub-hypers in the sum and drop out
automatically. If however all columns of $J$ are zero, then its denotation
$[\\![J]\\!]$ becomes automatically the weight-zero sub-point hyper.

###  2.5. Abstract channels — review

In earlier work [6] we described an “abstract channel” as a function from
prior distributions to hypers. We restate that here in our current
denotational style:

######  Definition 8.

Denotation of channel Let $C{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ be a channel matrix. Its
denotation, of type ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$, is called an _abstract
channel_ and is defined for $\pi{{:}\,}{\mathbb{D}}{\cal X}$ by

$[\\![C]\\!].\pi{:=}\,[\\![\pi{\rhd}C]\\!]~{},$

where the $[\\![\cdot]\\!]$ on the left is the denotational function for
channels, being defined here; and on the right it is the denotational function
on joint distributions that we have already from Def. 7. (We use $[\\![-]\\!]$
uniformly for denotation functions, relying on context instead of e.g. using
subscripts like $[\\![-]\\!]_{\rm chan}$ on the left and $[\\![-]\\!]_{\rm
joint}$ on the right.) $\Box$

In fact the prior $\pi$ can be recovered from $\pi{\rhd}C$, as this definition
shows:

######  Definition 9.

Support of a distribution Given discrete distribution
$\delta{{:}\,}{\mathbb{D}}{\cal Z}$, we write $\lceil\delta\rceil$ for the
_support_ of $\delta$, the set of elements $z{{:}\,}{\cal Z}$ for which
$\delta.z$, the probability assigned by $\delta$ to $z$, is not zero.
Obviously $\delta{\in}{\mathbb{D}}{\cal Z}$ implies
$\lceil\delta\rceil{\subseteq}{\cal Z}$; if in fact
$\lceil\delta\rceil{=}{\cal Z}$ then we say that $\delta$ is _full support_.
$\Box$

######  Definition 10.

Average of a hyper For hyper $\Delta{{:}\,}{\mathbb{D}}^{2}{\cal X}$ define
its average ${\sf avg}.\Delta$ in ${\mathbb{D}}{\cal X}$ by

${\sf avg}.\Delta.x\hskip 10.00002pt{:=}\,\hskip
10.00002pt\sum_{\delta{{:}\,}\lceil\Delta\rceil}(\Delta.\delta)(\delta.x)~{}\textrm{\quad\quad
for all}~{}x{{:}\,}{\cal X},\quad$

where we use upper-case Greek for hypers. $\Box$

We then have ${\sf avg}.([\\![C]\\!].\pi)=\pi$, because

$({\sf avg}.([\\![C]\\!].\pi))_{x}~{}~{}=~{}~{}({\sf
avg}.[\\![\pi{\rhd}C]\\!])_{x}~{}~{}=~{}~{}\textrm{$\footnotesize\Sigma$}(\pi{\rhd}C)_{x,-}~{}~{}=~{}~{}\pi_{x}\quad.$

In fact ${\sf avg}.[\\![J]\\!]$ for any $J$ in ${\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ is $J$’s ${\cal X}$ marginal in
${\mathbb{D}}{\cal X}$.

##  3\. Classical- vs. abstract HMM’s

###  3.1. Classical HMM’s, and single HMM-steps as matrices

Classically a Hidden Markov Model comprises a set ${\cal X}$ of states, a set
${\cal Y}$ of observations and two stochastic matrices $C,M$ that give resp.
the _emission_ probabilities $C_{x,y}$ that $x$ will emit observation $y$ and
the _transition_ probabilities $M_{x,x^{\prime}}$ that $x$ will change to
$x^{\prime}$ [12]. Usually, the homogeneous case, computation evolves in
(probabilistic) steps each determined by the same $C,M$, with each output
state $x^{\prime}$ becoming the following input $x$ and with the emissions $y$
accumulating. In our case however, heterogeneous, we can vary the matrices
from step to step, each standing for various (different) program fragments.

We show two computations in Fig. 1. If $\pi$ is the distribution of incoming
$x$, the distribution $\pi^{\prime\prime}$ of intermediate $x^{\prime\prime}$
is $\pi{\mathbin{\cdot}}M^{1}$. The distribution of observations $y^{1}$ is
$\pi{\mathbin{\cdot}}C^{1}$. The second step’s input $x^{\prime\prime}$ is the
output of the first step.

A classical HMM hides all of three of $x,x^{\prime\prime},x^{\prime}$, but
still the observations $y^{1,2}$ tell us something about each of them provided
we know $\pi,M^{1,2},C^{1,2}$. (This is analogous to knowing the source code
of a program, but not being able to observe its variables as it executes.)

Each step $H^{1,2}$ takes an input- to an output state in ${\cal X}$; the
observations $y^{1,2}{{:}\,}{\cal Y}$ are accumulated. In each step $H^{1,2}$
the output state is determined by a markov $M^{1,2}$ on the input to that
step, and the observation is determined independently by a channel $C^{1,2}$
on the same input, i.e.  _before_ application of the markov. Figure 1. Two
successive steps $H^{1}$ and $H^{2}$ of a heterogeneous HMM.

From now on we call the emission part of an HMM the _channel_ and the
transition part the _markov_ (lower case).

######  Definition 11.

Single HMM-step Given channel $C{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ and markov $M{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal X}$, define the HMM-matrix $(C{;}M)$ of
type ${\cal X}{\mathbin{\rightarrowtriangle}}{\cal Y}{\times}{\cal X}$ by

$(C{;}M)_{x,y,x^{\prime}}\hskip 10.00002pt{:=}\,\hskip 10.00002ptC_{x,y}\times
M_{x,x^{\prime}}~{}.$

This (row-1-summing) matrix $(C{;}M)$ produces a joint distribution of type
${\mathbb{D}}({\cal X}{\times}{\cal Y}{\times}{\cal X})$, as top-left in Fig.
6, once applied to a prior (Def. 2). $\Box$

Note that in $(C{;}M)$ the probabilistic choices in $C$ (of $y$) and $M$ (of
$x^{\prime}$) are made independently; although indeed $(C{;}M)$ has the
property that for each $x{{:}\,}{\cal X}$ the (remaining) joint distribution
$(C{;}M)_{x,-,-}$ is independent in $y,x^{\prime}$, this property is not
preserved once steps are composed (§4).

###  3.2. Abstract HMM’s represent classical HMM’s

For abstract channels (§2.5) we focussed on the hyper of posteriors on the
_input_ ; for HMM’s we focus on the hyper of posteriors on the _output_ ,
because HMM’s are computations and so it is over their outputs we wish to
reason. (The _prior_ on the output would be our calculation from the input
prior and the markov of what the output distribution would be, but _before_
running the program and making observations in the type ${\cal Y}$.)

######  Definition 12.

Matrix HMM denotes abstract HMM Let $H{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}{\times}{\cal X}$ be an HMM presented
as a matrix (stochastic in $y,x^{\prime}$). Its denotation, of type
${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$, is
called an _abstract HMM_ and is defined $[\\![H]\\!].\pi{:=}\,[\\![J]\\!]$,
where $\pi{{:}\,}{\mathbb{D}}{\cal X}$ and the joint-distribution matrix
$J{{:}\,}{\cal X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ is given by
$J_{x^{\prime},y}{:=}\,\,\textrm{$\footnotesize\Sigma$}_{x}\pi_{x}H_{x,y,x^{\prime}}$.
$\Box$

In §12 we discuss the (Dalenius) implications of having abstracted from the
HMM’s input (with the $\textrm{$\footnotesize\Sigma$}_{x}$ just above) — it is
not always appropriate.

###  3.3. Special cases of HMM-steps: pure markovs

Markovs are the special case of HMM where the channel-part effectively outputs
nothing. If an HMM-step $(C{;}M)$ has for its channel $C$ an all-one column
vector nc, where nc stands for “null channel”. Then ${\cal Y}$ is a singleton
and $J$ becomes a column vector: i.e.
$J_{x^{\prime}}=\textrm{$\footnotesize\Sigma$}_{x}\pi_{x}M_{x,x^{\prime}}$, so
that in fact $J$ is the usual matrix product $\pi{\mathbin{\cdot}}M$.

Taking ${\sf nc}$ as the default channel gives $[\\![{:}M]\\!].\pi=[\\![{\sf
nc}{:}M]\\!].\pi=[\pi{\mathbin{\cdot}}M]$, the point hyper on
$\pi{\mathbin{\cdot}}M$. This more general framework simply “wraps” a $[-]$
around the final distributions; but it’s that wrapping that enables treating
markovs and channels within the same type. A general $H$ is a markov just when
$\textrm{$\footnotesize\Sigma$}_{x^{\prime}}H_{x,y,x^{\prime}}$ is ${\sf nc}$.

// xs is initialised uniformly at random.
---
xs:= xs ${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.45003pt\oplus}}$ -xs
// What does an attacker guess for xs finally?
The secret two-bit bit-string xs is set initially from $\\{00,01,10,11\\}$
with equal probability $\nicefrac{{1}}{{4}}$ for each; the following
assignment either leaves xs unchanged (probability $\nicefrac{{1}}{{2}}$) or
bit-wise inverts both components. Figure 2. Pure-markov HMM program

Consider the program of Fig. 2 whose single variable is a two-bit string xs.
We model it with ${\cal X}{=}\\{00,01,10,11\\}$; prior
$\pi{{:}\,}{\mathbb{D}}{\cal X}$ is uniform, and its markov $M$ is as just
below:

<EMAIL_ADDRESS>15.00002pt&\mbox{{\mbox{\small$00$}}}&{\mbox{\small$01$}}&{\mbox{\small$10$}}&{\mbox{\small$11$}}\\\\[3.00003pt]
{\mbox{\small$00{:}$}}\hfil\hskip
15.00002pt&\makebox[0.0pt]{\raisebox{-18.00005pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{28.00006pt}\right.\hskip
10.00002pt$}}\nicefrac{{1}}{{2}}&0&0&\nicefrac{{1}}{{2}}\makebox[0.0pt]{\raisebox{-18.00005pt}[0.0pt][0.0pt]{$\hskip
11.00008pt\left.\rule{0.0pt}{28.00006pt}\right)$}}\\\
{\mbox{\small$01{:}$}}\hfil\hskip
15.00002pt&0&\nicefrac{{1}}{{2}}&\nicefrac{{1}}{{2}}&0\\\
{\mbox{\small$10{:}$}}\hfil\hskip
15.00002pt&0&\nicefrac{{1}}{{2}}&\nicefrac{{1}}{{2}}&0\\\
{\mbox{\small$11{:}$}}\hfil\hskip
15.00002pt&\nicefrac{{1}}{{2}}&0&0&\nicefrac{{1}}{{2}}\end{array}$

The output distribution is of course
$\pi^{\prime}{=}\pi{\mathbin{\cdot}}M{=}\pi$, and so the attacker’s guess of
the final state is optimally any of the four values in ${\cal X}$: they are
equally good.

This system viewed as an abstract HMM would give output _hyper_
$\Delta^{\prime}=[\\![{:}M]\\!].\pi=[\pi]$, in fact the _point_ hyper on $\pi$
indicating that the attacker is certain (point-probability 1) that the
posterior distribution $\pi^{\prime}$ on the final value of xs is equal to the
prior $\pi$ in this case, i.e. it is still uniform.

###  3.4. Special cases of HMM-steps: pure channels

Channels are the special case where the input- and the output state are the
same. If $(C{;}M)$ has markov $M$ as the identity id, then it is a “pure
channel” with output the same as its input. In that case Def. 12 gives
$J_{x^{\prime},y}=\sum_{x}\pi_{x}C_{x,y}{\sf
id}_{x,x^{\prime}}=(\pi{\rhd}C)_{x^{\prime},y}$, and so $[\\![C{:}{\sf
id}]\\!]$ from Def. 12 is just $[\\![C]\\!]$ from Def. 8.

With ${\sf id}$ as the default markov, we have $[\\![C{:}]\\!]=[\\![C]\\!]$.

// xs is initialised uniformly at random.
---
leak xs[0]${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.45003pt\oplus}}$ xs[1]
The value of either bit 0 or bit 1 of xs is revealed; the attacker learns that
value, but does not know which bit it came from. What should he guess for xs
after execution in this case? Figure 3. Pure-channel HMM program.

Now consider Fig. 3 where some of xs is leaked, but xs itself is not changed.
Thus our state ${\cal X}$ and prior $\pi$ are as before, the observation space
is ${\cal Y}{=}\\{0,1\\}$ and the channel $C$ representing this program is
here at left:

<EMAIL_ADDRESS>16.99998pt&{\mbox{\small$0$}}&{\mbox{\small$1$}}\\\
{\mbox{\small$00{:}$}}\hfil\hskip
16.99998pt&\makebox[0.0pt]{\raisebox{-18.00005pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{28.00006pt}\right.\hskip
10.00002pt$}}1&0\makebox[0.0pt]{\raisebox{-18.00005pt}[0.0pt][0.0pt]{$\hskip
11.00008pt\left.\rule{0.0pt}{28.00006pt}\right)$}}\\\
{\mbox{\small$01{:}$}}\hfil\hskip
16.99998pt&\nicefrac{{1}}{{2}}&\nicefrac{{1}}{{2}}\\\
{\mbox{\small$10{:}$}}\hfil\hskip
16.99998pt&\nicefrac{{1}}{{2}}&\nicefrac{{1}}{{2}}\\\
{\mbox{\small$11{:}$}}\hfil\hskip 16.99998pt&0&1\end{array}\hskip
<EMAIL_ADDRESS>16.99998pt&{\mbox{\small$0$}}&{\mbox{\small$1$}}\\\
{\mbox{\small$00{:}$}}\hfil\hskip
16.99998pt&\makebox[0.0pt]{\raisebox{-18.00005pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{28.00006pt}\right.\hskip
10.00002pt$}}\nicefrac{{1}}{{4}}&0\makebox[0.0pt]{\raisebox{-18.00005pt}[0.0pt][0.0pt]{$\hskip
11.00008pt\left.\rule{0.0pt}{28.00006pt}\right)$}}\\\
{\mbox{\small$01{:}$}}\hfil\hskip
16.99998pt&\nicefrac{{1}}{{8}}&\nicefrac{{1}}{{8}}\\\
{\mbox{\small$10{:}$}}\hfil\hskip
16.99998pt&\nicefrac{{1}}{{8}}&\nicefrac{{1}}{{8}}\\\
{\mbox{\small$11{:}$}}\hfil\hskip 16.99998pt&0&\nicefrac{{1}}{{4}}\end{array}$

The joint distribution in $x^{\prime},y$ is $J{=}\pi{\rhd}C$. The construction
of Def. 7 gives us a hyper $\Delta^{\prime}$ as

$\begin{array}[]{r@{\hspace{3em}}l@{\,}l}\textrm{inner distributions}\hskip
30.00005pt&\lx@intercol\textrm{outer distribution}\hfil\lx@intercol\\\
(\nicefrac{{1}}{{2}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},0)\hskip
30.00005pt&@&\nicefrac{{1}}{{2}}\\\
(0,\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{2}})\hskip
30.00005pt&@&\nicefrac{{1}}{{2}}~{},\end{array}$ (2)

where in general we write $z_{1}@p_{1},~{}z_{2}@p_{2},\cdots$ for the discrete
distribution that assigns probability $p_{1}$ to $z_{1}$ etc. In (2) the
values $z_{1},z_{2}$ are themselves (inner, posterior) distributions. This
hyper shows that with probability $\nicefrac{{1}}{{2}}$ an optimal attacker
will guess `00` (because she saw a `0` leaked, and deduces _a posteriori_ that
`00` now has the highest probability, twice either of the others); and with
probability $\nicefrac{{1}}{{2}}$ the attacker will guess `11` (because she
saw a `1`).

##  4\. Beyond steps: HMM programming and sequential composition

###  4.1. Classical HMM composition: matrices

Let $H^{1},H^{2}{{:}\,}{\cal X}{\mathbin{\rightarrowtriangle}}{\cal
Y}{\times}{\cal X}$ be two HMM’s. Their sequential composition $H=H^{1};H^{2}$
describes the distribution on $x$, and $y_{1,2}$ together, and $x^{\prime}$ as

$(H^{1};H^{2})_{x,(y_{1},y_{2}),x^{\prime}}\hskip 10.00002pt{:=}\,\hskip
10.00002pt\sum_{x^{\prime\prime}}H^{1}_{x,y_{1},x^{\prime\prime}}H^{2}_{x^{\prime\prime},y_{2},x^{\prime}}~{}.$
(3)

Note how the set of observables is now ${\cal Y}{\times}{\cal Y}$, compounding
the observations ${\cal Y}$ from each component. (This is why infinite
composition of HMM’s cannot easily be represented as a finite matrix.)

Remarkably, the action of HMM-composition on pure-markovs HMM’s is effectively
their matrix multiplication, yet its action on pure channels is effectively
their “parallel composition”: thus a single general definition of composition
specialises automatically to the two principal sub-cases, as we now show.
First, we give the details for classical HMM’s; then Thm. 15 shows that the
same holds for abstract HMM’s.

####  4.1.1. Composition of pure markovs

The usual composition of Markov matrices $M^{1,2}{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal X}$ is via matrix multiplication
$M^{1}{\mathbin{\cdot}}M^{2}$, and the result is of the same type ${\cal
X}{\mathbin{\rightarrowtriangle}}{\cal X}$. If we do it at the HMM-level, we
find

|
$\begin{array}[t]{@{}llll}({;}M^{1}){;}({;}M^{2})~{}_{x,(y_{1},y_{2}),x^{\prime}}\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}\sum_{x^{\prime\prime}}({;}M^{1})_{x,y_{1},x^{\prime\prime}}({;}M_{2})_{x^{\prime\prime},y_{2},x^{\prime}}\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}{\sf nc}_{x,(y_{1},y_{2})}\sum_{x^{\prime\prime}}M^{1}_{x,x^{\prime\prime}}M^{2}_{x^{\prime\prime},x^{\prime}}\end{array}$ “Recall from §3.3 that channel ${\sf nc}$ reveals nothing.”
$=$ |  $\begin{array}[t]{@{}llll}({;}~{}M^{1}{\mathbin{\cdot}}M^{2})\quad_{x,(y_{1},y_{2}),x^{\prime}}~{},\end{array}$

so that indeed $({;}M^{1}){;}({;}M^{2})=({;}~{}M^{1}{\mathbin{\cdot}}M^{2})$.

####  4.1.2. Composition of pure channels

Parallel composition of channels, which we write $C^{1}{\parallel}C^{2}$,
models applying _both_ channels to the same input and observing both outputs.
Thus

$C^{1}{\parallel}C^{2}\quad_{x,(y_{1},y_{2})}\hskip 10.00002pt=\hskip
10.00002ptC^{1}_{x,y_{1}}\times C^{2}_{x,y_{2}}~{}.$

This is different from channel _cascading_ , which applies the second channel
$C^{2}$ to the observations of the first channel $C^{1}$ via matrix
multiplication. A striking distinction is that the cascade of $C^{1}$ into
$C^{2}$ releases no more information that $C^{1}$ alone (the Data-Processing
Inequality [13]), whereas $C^{1}{\parallel}C^{2}$ releases no _less_
information that either of $C^{1,2}$ alone. In this latter case we find

|
$\begin{array}[t]{@{}llll}(C^{1}{;}){;}(C^{2}{;})~{}_{x,(y_{1},y_{2}),x^{\prime}}\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}\sum_{x^{\prime\prime}}(C^{1}{;})_{x,y_{1},x^{\prime\prime}}(C^{2}{;})_{x^{\prime\prime},y_{2},x^{\prime}}\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}\sum_{x^{\prime\prime}}C^{1}_{x,y_{1}}{\sf id}_{x,x^{\prime\prime}}C^{2}_{x^{\prime\prime},y_{2}}{\sf id}_{x^{\prime\prime},x^{\prime}}\end{array}$ “Recall from §3.4 markov ${\sf id}$ is the identity.”
$=$ |  $\begin{array}[t]{@{}llll}C^{1}_{x,y_{1}}C^{2}_{x,y_{2}}{\sf id}_{x,x^{\prime}}\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(C^{1}{\parallel}C^{2})_{x,(y_{1},y_{2})}{\sf id}_{x,x^{\prime}}\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(C^{1}{\parallel}C^{2}~{}{;})~{}_{x,(y_{1},y_{2}),x^{\prime}}~{},\end{array}$

so that indeed again
$(C^{1}{;}){;}(C^{2}{;})=(C^{1}{\parallel}C^{2}~{}{;}~{})$.

####  4.1.3. Pure channel followed by pure markov

Finally, note that a general HMM-step (§3.1) is a pure channel followed by a
pure markov. Let ${\sf nc}_{x,y_{2}}$ be $(\textrm{$1$ if $y_{2}{=}\hat{y}$
else $0$})$ for some fixed $\hat{y}$ in ${\cal Y}$, and calculate

|
$\begin{array}[t]{@{}llll}(C{;}){;}({;}M)\quad_{x,(y_{1},y_{2}),x^{\prime}}\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}\sum_{x^{\prime\prime}}(C{;})_{x,y_{1},x^{\prime\prime}}({;}M)_{x^{\prime\prime},y_{2},x^{\prime}}\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}\sum_{x^{\prime\prime}}C_{x,y_{1}}{\sf id}_{x,x^{\prime\prime}}{\sf nc}_{x^{\prime\prime},y_{2}}M_{x^{\prime\prime},x^{\prime}}\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}C_{x,y_{1}}M_{x,x^{\prime}}{\sf nc}_{x,y_{2}}\end{array}$ “${\sf id}_{x^{\prime\prime},x^{\prime}}$, 1-point rule”
$=$ |  $\begin{array}[t]{@{}llll}\textrm{$C_{x,y_{1}}M_{x,x^{\prime}}$ if $y_{2}{=}\hat{y}$ else $0$}\end{array}$ “above”
$=$ |  $\begin{array}[t]{@{}llll}(C{;}M)_{x,(y_{1},y_{2}),x^{\prime}}~{},\end{array}$

so that $(C{;}){\,;\,}({;}M)=(C{;}M)$.

The reason that $(C{;}){;}({;}M)$ and $({;}M){;}(C{;})$ differ in general is
that in the (mathematical) definition of an HMM-step (e.g. Fig. 1) the
emissions are determined by the input, initial state (rather than the output,
final state). Had that original definition been the other way around, then
we’d have had $({;}M){;}(C{;})$ as an HMM-step.

####  4.1.4. Pure markov followed by pure channel

This cannot, in general, be reduced to a single HMM-step. In $({;}M);(C{;})$
let both $C,M$ be the identity. Then the observations and final state will be
perfectly correlated, something that is not possible for single HMM-step
$(C^{\prime}{;}M^{\prime})$.

###  4.2. Abstract HMM’s: Kleisli composition

Now we consider $h_{1};h_{2}$ where $h_{1,2}$ are abstract HMM’s. (We use
upper-case for matrices and lower-case for denotations.) Because the
components’ types ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$ do not match directly, i.e.
the co-domain ${\mathbb{D}}^{2}{\cal X}$ from the left is not the domain
${\mathbb{D}}{\cal X}$ required on the right, we use Kleisli composition for
that. 777This is the usual composition in a Kleisli category. See §7.

######  Definition 13.

Push-forward of a function Given sets ${\cal Z},{\cal Z}^{\prime}$ and
function $f{{:}\,}{\cal Z}{\mathbin{\rightarrow}}{{\cal Z}^{\prime}}$, we
write ${\mathbb{D}}f$ for the _push-forward_ of $f$, a “lifted” function of
type ${\mathbb{D}}{\cal Z}{\mathbin{\rightarrow}}{\mathbb{D}}{\cal
Z}^{\prime}$ [14]. For $z^{\prime}{{:}\,}{\cal Z}^{\prime}$ and
$\delta{{:}\,}{\mathbb{D}}{\cal Z}$ we have 888Lifting, as in ${\mathbb{D}}f$,
binds tightest: the conventional notation for
${\mathbb{D}}f.\delta.z^{\prime}$ would be
$({\mathbb{D}}f)(\delta)(z^{\prime})$, so that
$({\mathbb{D}}f)(\delta){\in}{\mathbb{D}}{\cal Z}^{\prime}$.

${\mathbb{D}}f.\delta.z^{\prime}\hskip 10.00002pt{:=}\,\hskip
10.00002pt\sum_{\begin{subarray}{c}z{{:}\,}{\cal Z}\\\
f.z=z^{\prime}\end{subarray}}\delta.z~{}.\quad\vspace{-1em}$

$\Box$

######  Definition 14.

Kleisli composition of abstract HMM’s
Given two abstract HMM’s $h_{1,2}{{:}\,}{\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$, their Kleisli composition
is defined

$(h_{1};h_{2}).\pi\hskip 10.00002pt{:=}\,\hskip 10.00002pt{\sf
avg}.({\mathbb{D}}h_{2}.(h_{1}.\pi))$

for $\pi{{:}\,}{\mathbb{D}}{\cal X}$, where ${\mathbb{D}}h_{2}$ is as above
the push-forward of $h_{2}$. Using functional composition, equivalently
$h_{1};h_{2}{:=}\,{\sf
avg}\mathbin{\circ}{\mathbb{D}}h_{2}\mathbin{\circ}h_{1}$. $\Box$

That is, the lifting inherent in Kleisli-composition applies the right-hand
abstract HMM $h_{2}$ to each inner (i.e. posterior) produced by the left-hand
$h_{1}$ from prior $\pi$, preserving the way in which they are all combined
together by the outer distribution. Then the intermediate result, of type
${\mathbb{D}}^{3}{\cal X}$, is averaged to bring it back to the required type
${\mathbb{D}}^{2}{\cal X}$.

###  4.3. Proof that composition is faithfully denoted

It is important (though unsurprising) for our interpretation that composition
of HMM’s as matrices (3) is correctly mapped by $[\\![\cdot]\\!]$ to their
Kleisli composition as abstract HMM’s (Def. 14). That is, we expect

######  Theorem 15.

Composition faithfully denoted Let $H^{1,2}{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}{\times}{\cal X}$ be HMM’s as
matrices. Then we have

$[\\![H^{1};H^{2}]\\!]\hskip 10.00002pt=\hskip
10.00002pt[\\![H^{1}]\\!];[\\![H^{2}]\\!]~{},$

where (3) is used on the left and Def. 14 on the right.

Proof. We reason as follows for any $\pi$.

|  $\begin{array}[t]{@{}llll}([\\![H^{1}]\\!];[\\![H^{2}]\\!]).\pi\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}{\sf avg}.({\mathbb{D}}[\\![H^{2}]\\!].([\\![H^{1}]\\!].\pi))\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}{\sf avg}.({\mathbb{D}}[\\![H^{2}]\\!].[\\![[\\![\pi]\\!]{H^{1}}]\\!])\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}{\sf avg}.({\mathbb{D}}[\\![H^{2}]\\!].(\sum_{y^{1}}\underline{[([\\![\pi]\\!]{H^{1}})_{y^{1},-}]}))\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{y^{1}}[\\![H^{2}]\\!].([\\![\pi]\\!]{H^{1}})_{y^{1},-})\end{array}$ “${\mathbb{D}}f$ distributes $f$ through inners.”
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{y^{1}}[\\![[\\![([\\![\pi]\\!]{H^{1}})_{y^{1},-}\,]\\!]{\,H^{2}}]\\!])\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{y^{1}}(\sum_{y^{2}}\underline{[([\\![([\\![\pi]\\!]{H^{1}})_{y^{1},-}\,]\\!]{\,H^{2}})_{y^{2},-}]}))\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{y^{1},y^{2}}\underline{[([\\![\pi]\\!]{(H^{1};H^{2})})_{(y^{1},y^{2}),-}]})\end{array}$ “Lem. 16”
$=$ |  $\begin{array}[t]{@{}llll}[\\![H^{1};H^{2}]\\!].\pi~{},\end{array}$

as required. $\Box$

######  Lemma 16.

Double application of HMM matrix We have

$([\\![\pi]\\!]{(H^{1};H^{2})})_{(y^{1},y^{2}),-}\hskip 10.00002pt=\hskip
10.00002pt([\\![([\\![\pi]\\!]{H^{1}})_{y^{1},-}]\\!]{H^{2}})_{y^{2},-}$

from this calculation for any $x^{\prime}$ that

|
$\begin{array}[t]{@{}llll}([\\![\pi]\\!]{(H^{1};H^{2})})_{(y^{1},y^{2}),{x^{\prime}}}\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{x}\pi_{x}\,(H^{1};H^{2})_{x,(y^{1},y^{2}),{x^{\prime}}})\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{x}\pi_{x}\,(\sum_{x^{\prime\prime}}H^{1}_{x,y^{1},x^{\prime\prime}}H^{2}_{x^{\prime\prime},y^{2},x^{\prime}}))\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{x,x^{\prime\prime}}\pi_{x}\,H^{1}_{x,y^{1},x^{\prime\prime}}H^{2}_{x^{\prime\prime},y^{2},x^{\prime}})\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{x^{\prime\prime}}(\sum_{x}\pi_{x}\,H^{1}_{x,y^{1},x^{\prime\prime}})H^{2}_{x^{\prime\prime},y^{2},x^{\prime}})\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}(\sum_{x^{\prime\prime}}([\\![\pi]\\!]{H^{1}})_{y^{1},x^{\prime\prime}}H^{2}_{x^{\prime\prime},y^{2},x^{\prime}})\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}([\\![([\\![\pi]\\!]{H^{1}})_{y^{1},-}]\\!]{H^{2}})_{y^{2},x^{\prime}}~{},\end{array}$

as required. $\Box$

// xs is set uniformly at random.
---
leak xs[0] ${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.45003pt\oplus}}$ xs[1] ;
xs:= xs ${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.45003pt\oplus}}$ -xs
The value of either bit 0 or bit 1 of xs is revealed; the attacker learns that
value, but does not know which bit it is. Then xs is either unchanged or
inverted, but the attacker does not know which. What’s his best guess now for
the final value of xs? Figure 4. HMM program as sequential composition.

###  4.4. Channel/markov together: two examples of composition

For an example of sequential composition we return to xs and consider Fig. 4
where the state is both leaked _and_ (possibly) changed. The final hyper
$\Delta^{\prime}$ in this case is obtained by applying the markov $M$ to the
_inners_ generated by $C$ in §3.3 while retaining their outers: that gives

$\begin{array}[t]{r@{~}r@{\hspace{1em}}l@{}l@{\,}l}(~{}&\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{2}}+\nicefrac{{1}}{{2}}{\times}0,\hskip
10.00002pt\\\
~{}&\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}}+\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}},\hskip
10.00002pt\\\
~{}&\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}}+\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}},\hskip
10.00002pt\\\
~{}&\nicefrac{{1}}{{2}}{\times}0+\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{2}}\hskip
<EMAIL_ADDRESS>\end{array}\hskip
10.00002pt\begin{array}[t]{{r@{~}r@{\hspace{1em}}l@{}l@{\,}l}}(~{}&\nicefrac{{1}}{{2}}{\times}0+\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{2}},\hskip
10.00002pt\\\
~{}&\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}}+\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}},\hskip
10.00002pt\\\
~{}&\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}}+\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{4}},\hskip
10.00002pt\\\
~{}&\nicefrac{{1}}{{2}}{\times}\nicefrac{{1}}{{2}}+\nicefrac{{1}}{{2}}{\times}0\hskip
10.00002pt&)&@&\nicefrac{{1}}{{2}}\end{array}$

which is simplified first to this

$\begin{array}[]{r@{\hspace{1.2em}}l@{\,}l}(\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}})\hskip
11.99998pt&@&\nicefrac{{1}}{{2}}\\\
(\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}})\hskip
11.99998pt&@&\nicefrac{{1}}{{2}}\end{array}$

and then, since the two inners are the same, as a hyper-distribution is
collapsed to just the singleton hyper $[\pi]$, where we are using an explicit
$(\times)$ for multiplication of specific numbers.

Thus the program of Fig. 4 reveals nothing about the final value of xs when
the initial distribution was uniform. Informally we would explain this by
noting that the information about xs released by the leak becomes “stale”,
irrelevant once we do not know whether xs has subsequently been inverted or
not. (See §12 however for a discussion of why the initial value of xs might in
some cases still be important.)

It would be wrong however to conclude, from $\Delta^{\prime}{=}[\pi]$ in this
specific case, that the program is secure for xs in general — for when the
initial distribution is _not_ uniform, the final value of xs  _can_ be less
secure than the initial. This illustrates the danger in assuming something is
uniformly distributed simply because we know nothing about it. (See §4.4.)

We now reconsider Fig. 4 but with a non-uniform prior, showing that indeed the
conclusion that the program was (wrt. the final state) “leak free” is
unjustified. In Fig. 5 the initial hyper is “skewed”, i.e. it is not uniform
over the whole type XS of xs, but rather is concentrated on only three of its
values:

// xs is set uniformly from {01,10,11}.
---
leak xs[0] ${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.45003pt\oplus}}$ xs[1] ;
xs:= xs ${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.45003pt\oplus}}$ -xs
This system is as in Fig. 4 except that the prior initial distribution
differs: at least one bit of xs is known to be 1. Figure 5. Simple-channel
program excluding xs=00 initially.

$\begin{array}[]{r@{\hspace{3em}}l@{\,}l}(0,\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}})\hskip
30.00005pt&@&1~{},\end{array}$ (4)

so that with certainty ($@1$) it is known that the initial distribution is
$(0,\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}},\nicefrac{{1}}{{3}})$. Via the
first statement leak xs[0]
${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.50003pt\oplus}}$ xs[1] an attacker
will with probability $\nicefrac{{1}}{{3}}$ (resp. $\nicefrac{{2}}{{3}}$)
observe `0` (resp. `1`) and revise his belief of xs’s distribution as in the
first (resp. second) row here:

$\begin{array}[]{r@{\hspace{3em}}l@{\,}l}(0,\nicefrac{{1}}{{2}},\nicefrac{{1}}{{2}},0)\hskip
30.00005pt&@&\nicefrac{{1}}{{3}}\\\
(0,\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{2}})\hskip
30.00005pt&@&\nicefrac{{2}}{{3}}\end{array}$

And after the second statement xs:= xs
${\mathbin{{}_{\nicefrac{{1}}{{2}}}\kern-0.50003pt\oplus}}$ -xs the hyper for
the _current_ (and final) distribution of xs will have become

$\begin{array}[]{r@{\hspace{3em}}l@{\,}l}(0,\nicefrac{{1}}{{2}},\nicefrac{{1}}{{2}},0)\hskip
30.00005pt&@&\nicefrac{{1}}{{3}}\\\
(\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}},\nicefrac{{1}}{{4}})\hskip
30.00005pt&@&\nicefrac{{2}}{{3}}~{},\end{array}$ (5)

where in the $\nicefrac{{1}}{{3}}$-case he is better off finally than
initially (since he knows xs cannot be 00 or 11), but in the other case he is
worse off (since xs=00 has become possible). Thus if the attacker’s choice is
either to guess xs’s initial value or to run the program and guess xs’s final
value, he can use these hypers to help make up his mind depending on his own
criteria for the utility of his planned theft, that is the social context in
which he is operating. Compare for example a thief’s two alternatives for
stealing a credit card: she might _“Steal it now, since the wallet is just
sitting there.”_ or she might _“Steal it after the card is used at an ATM
where she can see some digit of the PIN.”_ But in the second case there is a
risk her victim will notice her, and choose a new PIN.

For example, the Shannon entropy of xs is initially $\lg(3){\sim}1.6$, but
finally, it is conditionally
$\nicefrac{{1}}{{3}}{\times}1+\nicefrac{{2}}{{3}}{\times}2=\nicefrac{{2}}{{3}}{>}1.6$:
if the attacker is using Shannon entropy to make his decision, he should act
sooner rather than later.

On the other hand, the one-guess probability (Rényi min-entropy) of xs is
initially $\nicefrac{{1}}{{3}}$; and finally it is the same, at
$\nicefrac{{1}}{{3}}{\times}\nicefrac{{1}}{{2}}+\nicefrac{{2}}{{3}}{\times}\nicefrac{{1}}{{4}}=\nicefrac{{1}}{{3}}$.
If the attacker is using this criterion, it does not matter when he acts.

In either case, the hypers (4) and (5) contain all the information necessary
for his decision: the bit-values printed are themselves not important _for his
decision_ , which is why we can quotient our semantics by abstracting from
them. (He does, however, need those values when he _makes_ his attack if
indeed he decides “later”.)

These calculations are confirmed in the next section.

##  5\. Overview of Haskell-monadic prototype

A Haskell prototype of our hyper-based monadic model has been constructed for
discrete, finite HMM’s, and it has been applied to our examples of Figs. 2–5
[15]. We give a brief summary here.

A discrete probability distribution on a set ${\cal X}$ is modelled as a
monadic type `Dist x` that is effectively a list `[(x,Rational)]` of elements
from ${\cal X}$ and their associated probabilities. The type of (discrete)
hypers ${\mathbb{D}}^{2}{\cal X}$ is then `Dist(Dist x)`.

A Markov “matrix” on ${\cal X}$ is of type `x->Dist x`, in fact encoding the
matrix as a function from row-indices to distributions ${\mathbb{D}}{\cal X}$;
a channel matrix is of type `x->Dist y` for any type ${\cal Y}$ of
observations whatever.

The mini- programming language has two elementary statements: to use a markov
`mm` we have an `update mm` that updates the state according to `mm`. Note
that `mm` is a _Markov matrix_ , but `update mm` is a _markov HMM_ that is
constructed from `mm`, i.e. implements it.

To use a channel `cm` we have a `reveal cm` that emits (e.g. prints) the
channel’s output wrt. the hidden state at that point: the state is not changed
and, in particular, the output is not assigned to anything. It is merely
observed. Both of these statements are of type `Dist x->Dist(Dist x)`,
modelling our ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$. In fact they are in
${\mathbb{H}}{\cal X}$, as Lemmas 21,23 show.

Sequential composition $({;})$ of programs is the Kleisli composition `>=>`
provided by Haskell’s conventions for monads, in this case the monad `Dist`.
Using that, and relying on §4.3 and §4.1.3, we can define an elementary HMM-
step (§3.1) as

> | hmmStep cm mm
> ---|---
> = |  reveal cm >=> update mm .

Thus `hmmStep` does not have to be primitive.

Our example space ${\cal X}$ is `(Bool,Bool)`, representing the bit-pair xs,
and our two example (input) priors are

> uniform | = | [ | ((False,False),1%4),
> ---|---|---|---
> |  |  | ((False,True),1%4),
> |  |  | ((True,False),1%4),
> |  |  | ((True,True),1%4)
> |  | ] |
> and from §B |  |  |
> skewed | = | [ | ((False,False),0),
> |  |  | ((False,True),1%3),
> |  |  | ((True,False),1%3),
> |  |  | ((True,True),1%3)
> |  | ] |

Our example observation space ${\cal Y}$ is `Bool`.

With suitable definitions typed as above for channel `oneBit` that outputs one
of `xs`’s two bits, uniformly at random, and `invert` that either inverts `xs`
or does not, again uniformly at random, the four programs are then

> fig2 | = |  | update invert
> ---|---|---|---
> fig3 | = |  | reveal oneBit
> fig4 | = |  | \-- Uniform prior.
> |  |  | reveal oneBit
> |  | >=> | update invert
> fig5 | = |  | \-- Skewed prior.
> |  |  | reveal oneBit
> |  | >=> | update invert

The programs are run using the function

> | runOn prior prog
> ---|---
> = | pretty (prog prior)

where `pretty` is an output-formatting function that prints hypers in a
readable way.

The results of running the programs are as follows, where the third column
gives the outer probabilities of the resulting hyper, and the first two
columns give the corresponding inner distributions. We print `True`,`False` as
`1`,`0` respectively: (The prototype prints probabilities as fractions; but
here they are printed as reals, for neatness.)

> runOn uniform fig2 =  00 0.25 1.0 point hyper 01 0.25 10 0.25 11 0.25

> runOn uniform fig3 =  01 0.25 0.5 Half the time… 10 0.25 11 0.5 11 is most
> likely, and 00 0.5 0.5 the other half it’s 00. 01 0.25 10 0.25

> runOn uniform fig4 =  00 0.25 1.0 01 0.25 10 0.25 11 0.25

> runOn skewed fig5 =  00 0.25 0.67 01 0.25 10 0.25 11 0.25 01 0.5 0.33 10 0.5

The prototype contains also a `repeat` feature: for example `repeat 10 (reveal
oneBit)` is a program that reveals a random bit of `xs` 10 times
independently. (Such an iteration of parallel compositions is sometimes called
“repeated independent runs.”) With the uniform prior we would expect that the
resulting hyper would have three inners: one of them, occurring with
probability approximately $\nicefrac{{1}}{{2}}$, would correspond to the case
where the input bits of xs differed, in which case with overall probability
$\nicefrac{{1023}}{{1024}}$ there would be two different revelations among the
10 instances — thus showing that indeed the bits differed. But we would still
have no (more) information about whether the input was `01` or `10`.

The remaining $\nicefrac{{1}}{{1024}}$ would be split between two cases: bit
`xs[0]` was revealed every time, or `xs[1]` was; and those outcomes would
contribute to the other two inners.

Those other two inners would have probability approximately
$\nicefrac{{1}}{{4}}$ each, corresponding to input `00` or `11` where the two
bits are the same. The program confirms this, giving

> runOn uniform
> (repeat 10 (reveal oneBit)) =
>  01 1/1026 513/2048 outer is about $\nicefrac{{1}}{{4}}$ 10 1/1026 11
> 512/513 inner is “almost certainly 11” 01 1/2 511/1024 about
> $\nicefrac{{1}}{{2}}$ 10 1/2 00 512/513 513/2048 about $\nicefrac{{1}}{{4}}$
> 10 1/1026 11 1/1026

(where this time we preserve the fractions). The small perturbations away from
$\nicefrac{{1}}{{4}}$ etc. reflect the small chance, mentioned above, that
even when the inputs differ the random `oneBit` reveals the same bit 10 times
in a row.

Finally, if we run the same program but with the final probabilistic inversion
included, we get

> runOn uniform
> (repeat 10 (reveal oneBit)
> >=> update invert) =
>  00 256/513 513/1024 two inners merged 01 1/1026 10 1/1026 11 256/513 about
> $\nicefrac{{1}}{{2}}$ 01 1/2 511/1024 about $\nicefrac{{1}}{{2}}$ 10 1/2

in which the two “bits equal” inners from just above have merged: although the
probabilistic inversion preserves the information concerning whether the bits
are equal, it conceals in the equals case whether they were both `00` or both
`11`.

##  6\. The structure of hyper-space

Our hyper-space ${\mathbb{D}}^{2}{\cal X}$ has been synthesised by abstraction
from the classical “matrix style” description of HMM’s. We now recall that
there is a partial order $(\ref{)}$ of refinement on hypers, where for two
hypers $\Delta_{S,I}{{:}\,}{\mathbb{D}}^{2}{\cal X}$ we say that $\Delta_{S}$
(a specification) is “refined by” $\Delta_{I}$ (implementation) when, in a
sense we make precise below, the implementation $\Delta_{I}$ releases no more
information than the specification $\Delta_{S}$ does [4, 5, 8, 3]. That order
lifts pointwise to ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$, i.e. that
$h_{S}{\ref{}}h_{I}$ just when $h_{S}.\pi\ref{h}_{I}.\pi$ for all
$\pi{{:}\,}{\mathbb{D}}{\cal X}$, thus giving a new _refinement_ order for
(abstract) HMM’s. We write $\Delta_{S}{\ref{}}\Delta_{I}$, and call it
“uncertainty refinement” if we need to distinguish it from other kinds of
refinement. Its ultimate antecedent is the lattice of information [16] — but
it generalises those seminal ideas significantly.

######  Definition 17.

Uncertainty refinement [5, 3] Let $\Delta_{S,I}{{:}\,}{\mathbb{D}}^{2}{\cal
X}$ be two hypers on ${\cal X}$. We say that $\Delta_{S}$ is refined by
$\Delta_{I}$ just when there is a distribution
$\underline{\Delta}{{:}\,}{\mathbb{D}}^{3}{\cal X}$, that is a distribution of
_hypers_ , such that

$\Delta_{S}~{}=~{}{\sf avg}.\underline{\Delta}\hskip
10.00002pt\textrm{and}\hskip 10.00002pt({\mathbb{D}}{\sf
avg}).\underline{\Delta}~{}=~{}\Delta_{I}~{}.\vspace{-1em}$

$\Box$

Recall that ${\mathbb{D}}{\sf avg}$ is the push-forward of ${\sf avg}$ (Defs.
13,10).

The advantage of the abstract formulation in Def. 17 is that it is defined on
hypers directly, and can be generalised to proper measures, thus extending
discrete distributions [5]. But in the case (as here) where we remain
discrete, there is an equivalent matrix-style characterisation:

######  Lemma 18.

Refinement of joint-distributions [4, 8] Let $J_{S}{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}_{S}$ and $J_{I}{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}_{I}$ be joint-distribution matrices
such that $[\\![J_{S,I}]\\!]{=}\Delta_{S,I}$ resp. 101010Recall that the
${\cal X}$ here in type ${\cal X}{\mathbin{\rightarrowtriangle}}{\cal Y}_{S}$
is the final-, not the initial state. Then

$\Delta_{S}\ref{\Delta}_{I}\hskip 10.00002pt\textrm{iff}\hskip
10.00002ptJ_{S}\mathbin{\cdot}R=J_{I}$ (6)

for some stochastic _refinement matrix_ $R{{:}\,}{\cal
Y}_{S}{\mathbin{\rightarrowtriangle}}{\cal Y}_{I}$. Note that the state-spaces
of $\Delta_{S,I}$ are the same, but their observation spaces ${\cal Y}_{S,I}$
can differ.

Proof. Illustrated in §C; sketch proof in §D. $\Box$

With Lem. 18 the reflexivity and transitivity of relation $(\ref{)}$ is clear
from elementary matrix properties. For anti-symmetry we refer to [6, Thm 6],
whose supporting Lemma 1 there is adapted to suit our purposes here:

######  Definition 19.

Expected value For distribution $\delta{{:}\,}{\mathbb{D}}{\cal Z}$ and
function $f{{:}\,}{\cal Z}{\mathbin{\rightarrow}}V$ for vector space $V$, the
expected value of $f$ on $\delta$ is ${\cal
E}_{\delta}\,f{:=}\,\sum_{z{{:}\,}{\cal Z}}~{}\delta_{z}{\times}f.z$, where
$\sum$ and $(\times)$ are taken in the vector space. 111111More generally it
is $\int f\,\textrm{d}\delta$ and requires measurability of $f$. One reason we
do not use the standard notation $E(X)$ for the expected value of random
variable $X$ is that the distribution over which $X$ is taken is implicit. In
the calculations our HMM-semantics entails, we often need to make it explicit.
$\Box$

We will be using ${\cal E}\,$ principally over hypers, i.e. the case ${\cal
Z}={\mathbb{D}}{\cal X}$ in the definition.

######  Lemma 20.

(Strict) monotonicity Given are two hypers
$\Delta_{S,I}{{:}\,}{\mathbb{D}}^{2}{\cal X}$ and a strictly concave function
$f{{:}\,}{\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{R}}^{\geq}$.

If $\Delta_{S}{\mathrel{\sqsubset}}\Delta_{I}$ then ${\cal
E}_{\Delta_{S}}\,f<{\cal E}_{\Delta_{I}}\,f$. And if $f$ is (non-strictly)
concave, then $\Delta_{S}{\ref{}}\Delta_{I}$ implies ${\cal
E}_{\Delta_{S}}\,f\leq{\cal E}_{\Delta_{I}}\,f$.

Proof. Proved for abstract channels in [6, Lem 1]; the proof for hypers is
essentially identical. $\Box$

We now have antisymmetry, because
$\Delta_{S}{\ref{}}\Delta_{I}{\ref{}}\Delta_{S}$ and
$\Delta_{S}{\neq}\Delta_{I}$ implies
$\Delta_{S}{\mathrel{\sqsubset}}\Delta_{I}{\mathrel{\sqsubset}}\Delta_{S}$
whence we have from Lem. 20 the contradiction ${\cal E}_{\Delta_{S}}\,f<{\cal
E}_{\Delta_{I}}\,f<{\cal E}_{\Delta_{S}}\,f$ for any strictly concave
$f{{:}\,}{\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{R}}^{\geq}$ of
our choice (for example Shannon entropy).

Hyper-space ${\mathbb{D}}^{2}{\cal X}$ also admits a metric, the Kantorovich
metric [17] based on the Manhattan metric on ${\mathbb{D}}{\cal X}$ (§7). It
is used for continuity properties (as we will see in §8.1), and is chosen
because of its hierarchical properties, i.e. that the Kantorovich metric on
say ${\cal X}$ induces a metric on ${\mathbb{D}}{\cal X}$ and
${\mathbb{D}}^{2}{\cal X}$ etc. [17].

##  7\. Monads: Giry, Kleisli and Kantorovich

With ${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$ we
have given a discrete model of abstract HMM’s, suitable for interpreting
probabilistic sequential programs with hidden state, together with concrete
programming examples (Figs. 2–4). We now provide a brief overview about how
our setup embeds into structures based on a Giry monad.

The Giry monad over the category of Polish spaces and continuous functions
comprises an endofunctor $\Pi$ and two natural transformations $\eta$ (unit)
and $\mu$ (multiply) [2]; following [1] we take that as a basis for the
denotation of computations. More precisely, we restrict ourselves to the
category Comp of compact metric spaces and continuous functions. We have been
using ${\mathbb{D}}$ as a specialisation of $\Pi$ to this case. The object
${\mathbb{D}}\mathcal{S}$ is the set of Borel probability measures over the
compact metric space $\mathcal{S}$ which is indeed a compact metric space [18,
Thm 6.4]. To form a monad on Comp, we have provided the unit-function
$[\cdot]$ specialising $\eta$ that makes a point measure, and multiply-
function ${\sf avg}$ specialising $\mu$ that takes the average of a
distribution (of distributions). Typically we have $[\cdot]_{{\mathbb{D}}{\cal
X}}{\in}{\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$
and ${\sf avg}_{\cal X}{\in}{\mathbb{D}}^{2}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}{\cal X}$ where the subscripts are left
implicit when they are clear from the context.

From Giry’s construction, the arrows $[\cdot]_{\mathcal{S}}$ and ${\sf
avg}_{\mathcal{S}}$ are continuous with respect to the weak topology on
${\mathbb{D}}\mathcal{S}$ but, in this paper, we are dealing with compact
metric spaces. Fortunately, for compact metric spaces, the Kantorovich
distance metrizes the weak topology [19]. This implies that the triple
$({\mathbb{D}},[\cdot],{\sf avg})$ is indeed a monad on the category Comp.

Monadic constructions based on the Kantorovich metric are not new. In [17],
Van Breugel construct monads on the category Comp* of compact metric spaces
and 1-Lipschitz functions. His functor $\cal B$ coincides with our
${\mathbb{D}}$ on objects and he shows that $\cal Bf$, $[\cdot]_{\mathcal{S}}$
and ${\sf avg}_{\mathcal{S}}$ are 1-Lipschitz; whenever $f$ is 1-Lipschitz and
$\mathcal{S}$ is a compact metric space. Thus $(\cal B,[\cdot],{\sf avg})$ is
a monad on the category Comp* 121212Note that Van Breugel’s construction is
more general than this since he also considers complete metric spaces and
tight probability measures over them.. In that work, the metric is crucial
since the notion of 1-Lipschitzness is not a topological property. In fact,
Van Breugel shows that the Kantorovich metric is _the right_ metric to
construct probabilistic monads out of metric spaces. Such a construction does
not necessarily work with other metrics that metrizes the weak topology (e.g.
Prohorov metric which is equivalent to the Kantorovich metric from compact
spaces). However, arrows in the category Comp* are insufficient to denote
probabilistic programs with hidden states because $[\\![C]\\!]$ is not
necessarily 1-Lipschitz for some channel matrix $C$. This drives our choice of
the Giry monad $({\mathbb{D}},[\cdot],{\sf avg})$ on the category Comp of
compact metric spaces and continuous functions.

Our construction of the Kantorovich metric begins with a finite set ${\cal X}$
endowed with the discrete metric $d_{1}$ (i.e.
$d_{1}(x,x^{\prime}){:=}\,0\textrm{ if }x{=}x^{\prime}\textrm{ else }1$). This
is trivially a compact metric space. The space ${\mathbb{D}}{\cal X}$ of
discrete distributions on ${\cal X}$ is endowed with the Kantorovich metric
based on $d_{1}$ which coincides with the total variation metric on
${\mathbb{D}}{\cal X}$. At this level, the Kantorovich metric reduces to
$d_{K}(\delta^{1},\delta^{2})=\frac{1}{2}\sum_{x}|\delta^{1}_{x}{-}\delta^{2}_{x}|$.
At the next level, our hyper-space ${\mathbb{D}}^{2}{\cal X}$ has the Borel
algebra generated by ${\mathbb{D}}$ from ${\mathbb{D}}{\cal X}$, which is in
turn determined by the Kantorovich metric derived from $d_{K}$ which we will
also denote by $d_{K}$. These metrics are distinguished in terms of the
arguments they are applied on, i.e. $d_{K}(\delta^{1},\delta^{2})$ is the
Kantorovich metric on ${\mathbb{D}}{\cal X}$ while
$d_{K}(\Delta^{1},\Delta^{2})$ is the Kantorovich metric on
${\mathbb{D}}^{2}{\cal X}$.

##  8\. Characteristics of ${\mathbb{H}}{\cal X}$, the abstract HMM’s

###  8.1. Continuity and super-linearity

The semantic function $[\\![\cdot]\\!]$ (Def. 12) takes HMM matrices in ${\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}{\times}{\cal X}$ to functions in
${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$; but not
all of those functions are denotations $[\\![H]\\!]$ of some $H$. We now
describe two important characteristics satisfied by $[\\![H]\\!]$ as $H$
ranges over HMM’s: they are continuity and super-linearity. We will define
abstract HMM’s ${\mathbb{H}}{\cal X}$ to be just the functions satisfying
those conditions.

Sometimes called “healthiness conditions”, these are essentially technical
results giving general properties that are to hold for the denotation of any
program. They are used for the proof of other, more specific properties of
programs. Here we use them to define a subset ${\mathbb{H}}{\cal X}$ of
${\mathbb{D}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$, and we
prove that $[\\![H]\\!]{\in}{\mathbb{H}}{\cal X}$ for all classical HMM’s $H$.

Our first condition concerns continuity wrt. the Kantorovich metrics on
${\mathbb{D}}{\cal X}$ and ${\mathbb{D}}^{2}{\cal X}$.

######  Lemma 21.

Denotations of HMM’s are continuous For all $H{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}{\times}{\cal X}$ we have that
$[\\![H]\\!]$ is a continuous function in ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$ wrt. the Kantorovich
metrics.

Proof. We recall from Def. 12 that $[\\![H]\\!].\pi=[\\![\pi{\rhd}J]\\!]$
where $J_{x^{\prime},y}=\sum_{x}H_{x,y,x^{\prime}}$. We consider this as the
composition of the two functions $\pi{\mapsto}(\pi{\rhd}J)$ and
$[\\![\cdot]\\!]$, with the metric on the intermediate space ${\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ (of matrices) being the Kantorovich
metric $d_{K}$ on ${\mathbb{D}}({\cal X}{\times}{\cal Y})$ which is
$d_{K}(J^{1},J^{2})=\frac{1}{2}\sum_{(x,y)}|J^{1}_{x,y}-J^{2}_{x,y}|$.
Furthermore, since $\pi{\mapsto}(\pi{\rhd}J)$ comprises only elementary
arithmetic operations, and $d_{K}$ is topologically equivalent to the
Euclidean distance, the continuity is clear. Thus we concentrate on the
continuity of $[\\![\cdot]\\!]$ at an arbitrary joint distribution
$J{{:}\,}{\mathbb{D}}({\cal X}{\times}{\cal Y})$.

Let $\varepsilon{>}0$. We denote $[\\![J]\\!]=\Delta$ and let
$J^{\prime}{{:}\,}{\mathbb{D}}({\cal X}{\times}{\cal Y})$ with
$[\\![J^{\prime}]\\!]=\Delta^{\prime}$. Since $J$ and $J^{\prime}$ are
matrices, we can write $\Delta=\sum_{y}a_{y}[\delta^{y}]$ and
$\Delta^{\prime}=\sum_{y}a_{y}^{\prime}[\delta^{\prime y}]$ with
$\delta^{y},\delta^{\prime y}{{:}\,}{\mathbb{D}}{\cal X}$. These are sums over
the full set ${\cal Y}$ so if $a_{y}=0$ (resp. $a^{\prime}_{y}=0$) then we
define $\delta^{y}{:=}\,\delta^{\prime y}$ (resp. $\delta^{\prime
y}{:=}\,\delta^{y}$). Let us define
$\Delta^{\prime\prime}=\sum_{y}a_{y}[\delta^{\prime y}]$ which combines the
coefficients of $\Delta$ with the inners of $\Delta^{\prime}$. The triangular
inequality tells us that

$d_{K}(\Delta,\Delta^{\prime})\leq
d_{K}(\Delta,\Delta^{\prime\prime})+d_{K}(\Delta^{\prime\prime},\Delta^{\prime})~{}.$

On the one hand,

|
$\begin{array}[t]{@{}llll}d_{K}(\Delta^{\prime\prime},\Delta^{\prime})\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}\frac{1}{2}\sum_{y}\left|a_{y}-a^{\prime}_{y}\right|\end{array}$ “$\Delta^{\prime\prime}$ and $\Delta^{\prime}$ have finite supports”
$=$ |  $\begin{array}[t]{@{}llll}\frac{1}{2}\sum_{y}\left|\sum_{x}J_{x,y}-\sum_{x}J_{x,y}^{\prime}\right|\end{array}$ “Defn. $a_{y}$ and $a_{y}^{\prime}$”
$\leq$ |  $\begin{array}[t]{@{}llll}\frac{1}{2}\sum_{y,x}\left|J_{x,y}-J_{x,y}^{\prime}\right|\end{array}$ “$\left|\sum_{x}f.x\right|\leq\sum_{x}\left|f.x\right|$”
$=$ |  $\begin{array}[t]{@{}llll}d_{K}(J,J^{\prime})\end{array}$ “Defn. $d_{K}(J,J^{\prime})$”

On the other hand, for every $y$, the function which maps $J$ to $\delta_{y}$
is continuous at $J$ since it is a composition of a $y$-projection and
normalisation. Therefore, there exists $\alpha_{y}{>}0$ such that for every
$J^{\prime}{{:}\,}{\mathbb{D}}({\cal X}{\times}{\cal Y})$ with
$d_{K}(J,J^{\prime}){<}\alpha_{y}$, we have $d_{K}(\delta^{y},\delta^{\prime
y}){<}\frac{\varepsilon}{2}$. But we have

|  $\begin{array}[t]{@{}llll}d_{K}(\Delta,\Delta^{\prime\prime})\end{array}$
---|---
$\leq$ |  $\begin{array}[t]{@{}llll}\sum_{y}a_{y}d_{K}(\delta^{y},\delta^{\prime y})\end{array}$ “Kantorovich-Rubeinstein Theorem [19, Pg. 8]”
$\leq$ |  $\begin{array}[t]{@{}llll}\max_{y}d_{K}(\delta^{y},\delta^{\prime y})\end{array}$ “$\sum_{y}a_{y}=1$ and $a_{y}{\geq}0$ for all $y$”

Therefore, we choose $\beta=\min(\min_{y}\alpha_{y},\frac{\varepsilon}{2})$
and for every $J^{\prime}$ such that $d_{K}(J,J^{\prime})<\beta$, we have

$d_{K}(\Delta,\Delta^{\prime}){<}\frac{\varepsilon}{2}+\frac{\varepsilon}{2}=\varepsilon~{}.$

Hence, $[\\![\cdot]\\!]$ is continuous at $J$. $\Box$

Our second condition concerns linear combinations.

######  Definition 22.

Weighted sum For $\delta_{1,2}{{:}\,}{\mathbb{D}}{\cal X}$ we write
$\delta_{1}{\mathbin{{}_{p}\kern-0.50003pt+}}\delta_{2}$ for the weighted sum
of the two distributions, so that
$(\delta{\mathbin{{}_{p}\kern-0.50003pt+}}\delta^{\prime})_{x}=p\delta_{x}+(1{-}p)\delta^{\prime}_{x}$.
Note that $\delta{\mathbin{{}_{p}\kern-0.50003pt+}}\delta^{\prime}$ defined
here and the $\delta{\mathbin{{}_{p}\kern-0.50003pt\oplus}}\delta^{\prime}$ of
Def. 10 differ: the former is a single distribution made from $p$-merging
$\delta,\delta^{\prime}$; the latter is a hyper whose support is just the two
elements $\delta,\delta^{\prime}$. $\Box$

######  Lemma 23.

Denotations of HMM’s are super-linear For all $H{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}{\times}{\cal X}$ we have

$[\\![H]\\!].\pi_{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}[\\![H]\\!].\pi_{2}\hskip
10.00002pt\ref{}{1em}[\\![H]\\!].(\pi_{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}\pi_{2})~{},$
(7)

where $(\ref{)}$ is refinement as defined in Def. 17. 131313Super-linearity
can also be seen as a form of monotonicity. See §E.1.

Proof. Take any reduced $J^{1,2}{:}\,{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$, and argue first that for any
$0{\leq}p{\leq}1$ we have

$[\\![J^{1}]\\!]~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}[\\![J^{2}]\\!]\hskip
10.00002pt\ref{}{1em}[\\![J^{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}J^{2}]\\!]~{},$
(8)

since the horizontal concatenation $J$ of the two (scaled) matrices
$p{\times}J^{1}$ and $(1{-}p){\times}J^{2}$ satisfies
$[\\![J]\\!]=[\\![J^{1}]\\!]{\mathbin{{}_{p}\kern-0.50003pt+}}[\\![J^{2}]\\!]$,
and $J$ itself is refined to
$J_{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}J_{2}$ (in the sense of Lem. 18)
by the refinement matrix

$R\hskip 10.00002pt{:=}\,\hskip
10.00002pt\left(\begin{array}[]{ccc}1&0&\cdots\makebox[0.0pt][l]{\hskip
15.00002pt$\longleftarrow$\small\ corresp.\ to first col.\ of $J^{1}$}\\\
0&1&\cdots\makebox[0.0pt][l]{\hskip 15.00002pt$\longleftarrow$\small\
corresp.\ to snd.\ col.\ of $J^{1}$}\\\ \vdots&\vdots&\vdots\\\
1&0&\cdots\makebox[0.0pt][l]{\hskip 15.00002pt$\longleftarrow$\small\
corresp.\ to first col.\ of $J^{2}$}\\\ 0&1&\cdots\makebox[0.0pt][l]{\hskip
15.00002pt$\longleftarrow$\small\ corresp.\ to snd.\ col.\ of $J^{2}$}\\\
\vdots&\vdots&\vdots\end{array}\right)~{},\hskip 100.00015pt$

that simply sums corresponding columns. Now we observe that

|
$\begin{array}[t]{@{}llll}[\\![H]\\!](\pi_{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}\pi_{2})\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}[\\![(\pi_{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}\pi_{2}){\rhd}H)]\\!]\end{array}$
$=$ |  $\begin{array}[t]{@{}llll}[\\![\pi_{1}{\rhd}H~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}\pi_{2}{\rhd}H]\\!]\end{array}$
$\mathrel{\sqsupseteq}$ |  $\begin{array}[t]{@{}llll}[\\![\pi_{1}{\rhd}H]\\!]~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}[\\![\pi_{2}{\rhd}H]\\!]\end{array}$ “(8) just above”
$=$ |  $\begin{array}[t]{@{}llll}[\\![H]\\!].\pi_{1}~{}{\mathbin{{}_{p}\kern-0.50003pt+}}~{}[\\![H]\\!].\pi_{2}~{},\end{array}$

as required. $\Box$

Motivated by those two lemmas, we now define

######  Definition 24.

The space ${\mathbb{H}}{\cal X}$ of abstract HMM’s We write ${\mathbb{H}}{\cal
X}$ for those $h$ in ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$ satisfying Lemmas 21,23,
i.e. that are Kantorovich-continuous and super-linear. $\Box$

Thus our two lemmas above establish that $[\\![H]\\!]{\in}{\mathbb{H}}{\cal
X}$ for any classical HMM $H$.

Since we will therefore be restricting our denotations to ${\mathbb{H}}{\cal
X}$, a subset of the arrows in the category Comp, we expect ${\mathbb{H}}{\cal
X}$ to be closed under composition.

######  Lemma 25.

Abstract HMM’s closed under composition For any two
$h_{1,2}{{:}\,}{\mathbb{H}}{\cal X}$ we have $h_{1};h_{2}\in{\mathbb{H}}{\cal
X}$ as well, where $({;})$ is as in Def. 14.

Proof. Although a direct proof is possible, the result is much easier once we
have introduced “uncertainty” transformers (§9), because it is then a
consequence of Thm. 33 and in particular its Cor. 34, which depends crucially
on the dual view we develop in §9. $\Box$

It is shown in §E.2 that composition in ${\mathbb{H}}{\cal X}$ is monotonic
with respect to the refinement order $(\ref{)}$. This completes our
construction of our forward, abstract semantics for HMM’s. We now propose a
dual view.

##  9\. A dual view: uncertainty measures, and their transformers

###  9.1. Uncertainty measures, and their relation to refinement

“Uncertainty measures” generalise the diversity of entropy measures (including
e.g. Shannon), the functions from distributions to reals that measure
increasing disorder.

######  Definition 26.

Uncertainty measure An _uncertainty measure_ over ${\cal X}$ is a Kantorovich-
continuous- and concave function in ${\mathbb{D}}{\cal
X}\mathbin{\rightarrow}{\mathbb{R}}^{\geq}$, i.e. one taking distributions (on
${\cal X}$ in this case) to non-negative reals. It is intended that a
distribution’s greater uncertainty indicates more resilience (less
vulnerability) to the distribution’s being exploited by an adversary.
141414Smith’s “vulnerability measure” based on Bayes Risk [9] is an
uncertainty measure except that it goes in the opposite direction.

We write ${\mathbb{U}}{\cal X}$ for the uncertainty measures over ${\cal X}$,
and call them “UM’s” in the text for brevity. $\Box$

A typical example of a UM applied to a hyper is as follows. Given prior
$\pi{{:}\,}{\mathbb{D}}{\cal X}$ and channel $C{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$, the resulting hyper is
$\Delta{{:=}\,}[\\![\pi{\rhd}C]\\!]$ and the “conditional $u$ uncertainty” of
that (compare conditional Shannon entropy) would be ${\cal E}_{\Delta}\,u$. We
write ${\cal E}_{\Delta}\,u$ because it makes explicit that the conditional
uncertainty is an expected value and, as such, we can calculate with it. (More
conventional notations such as $H(y|x)$ –in the Shannon case– make those
calculations more difficult.) This could be compared to the uncertainty
$u.\pi$ of the prior, to give a “$u$-leakage” of the channel on that prior.

There is a compelling connection between UM’s (Def. 26) and refinement (Def.
17, Lem. 18): we have

######  Lemma 27.

Soundness and completeness of uncertainty measures [6] For any hypers
$\Delta_{1,2}{{:}\,}{\mathbb{D}}^{2}{\cal X}$ we have

$\Delta_{1}\ref{\Delta}_{2}\hskip 10.00002pt\textrm{iff}\hskip 10.00002pt{\cal
E}_{\Delta_{1}}\,\\!u\leq{\cal E}_{\Delta_{2}}\,\\!u~{}\textrm{\quad for all
$u{{:}\,}{\mathbb{U}}{\cal X}$.}\vspace{-1em}$

$\Box$

We regard “only if” as _soundness_ in the sense that if we have a witness to
the refinement relation $\Delta_{1}{\ref{}}\Delta_{2}$, i.e. either
$\underline{\Delta}$ (Def. 17) or $R$ (Lem. 18), then no UM can show
$\Delta_{2}$ to be less uncertain than $\Delta_{1}$. It is related to the
_Data-Processing Inequality_ , as explained in [6].

We regard “if” as _completeness_ in the sense that if refinement fails, that
is if $\Delta_{1}{\mathrel{\not\sqsubseteq}}\Delta_{2}$, then there is a UM
demonstrating the failure [4, 5, 8, 6].

In §E.5 is background on the proof of Lem. 27, whose completeness part was
originally called “Coriaceous” because it was hard to prove [8].

###  9.2. Abstract HMM’s to UM-transformers

In §3 we introduced a “forward” denotational view of HMM’s that takes initial
distributions to final hypers. Here we take the dual view, where an HMM takes
a “post-uncertainty” to a “pre-uncertainty”.

######  Definition 28.

Uncertainty-measure transformers Take $h{{:}\,}{\mathbb{H}}{\cal X}$ and
$u{{:}\,}{\mathbb{U}}{\cal X}$. Define the _uncertainty transformer_
$\textrm{wp}.h$ of type ${\mathbb{U}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{U}}{\cal X}$ so that for any
$u{{:}\,}{\mathbb{U}}{\cal X}$ and $\pi{{:}\,}{\mathbb{D}}{\cal X}$ we have

$\textrm{wp}.h.u.\pi\hskip 10.00002pt{:=}\,\hskip 10.00002pt{\cal
E}_{h.\pi}\,u~{},$

where on the right we are taking the expected value of $u$ on the hyper
$h.\pi$. (Because $u$ is continuous, it is measurable.) $\Box$

By analogy with weakest preconditions for ordinary sequential programming
[20], a UM-transformer $\textrm{wp}.h$ takes a UM to be applied _after_ $h$
and produces a UM that equivalently can be applied _before_ $h$. (Compare also
[21, 22, 23] for probabilistic/demonic sequential programs.) The idea (and
utility) is in goal-directed reasoning: if one knows the program, and knows
also the uncertainty that it must achieve, with the uncertainty transformer
one determines the minimum uncdertainty that is necessary _before_ the program
begins its execution.

In Lem. 29 we show well definedness of Def. 28, that is that $\textrm{wp}.h.u$
is indeed in ${\mathbb{U}}{\cal X}$.

######  Lemma 29.

Well-definedness of Def. 28 If $h{{:}\,}{\mathbb{H}}{\cal X}$ is an abstract
HMM and $u{{:}\,}{\mathbb{U}}{\cal X}$ is a UM, then $\textrm{wp}.h.u$ is in
${\mathbb{U}}{\cal X}$.

Proof. See §F. $\Box$

###  9.3. Characteristic properties of $\textrm{wp}.h$

For $h{{:}\,}{\mathbb{H}}{\cal X}$ the UM-transformer $\textrm{wp}.h$ has a
number of characteristic properties.

######  Lemma 30.

$\textrm{wp}.h$ is linear and total For every $h{{:}\,}{\mathbb{H}}{\cal X}$
and $t=\textrm{wp}.h$ we have that $t$ is:

  1. (1)

_linear_ so that for $a_{1,2}{{:}\,}{\mathbb{R}}^{\geq}$ and
$u_{1,2}{{:}\,}{\mathbb{U}}{\cal X}$ we have

$t.(a_{1}u_{1}+a_{2}u_{2})\hskip 10.00002pt=\hskip
10.00002pta_{1}t.u_{1}+a_{2}t.u_{2}~{};$

  2. (2)

_monotonic_ , so that $t.u_{1}.\delta\geq t.u_{2}.\delta$ for every
$u_{1}{\geq}u_{2}$ with $u_{1,2}{{:}\,}{\mathbb{U}}{\cal X}$ and
$\delta{{:}\,}{\mathbb{D}}{\cal X}$, where we lift $(\geq)$ pointwise; and

  3. (3)

_total_ , so that $t.\mathbf{1}{=}\mathbf{1}$ where $\mathbf{1}.\delta{:=}\,1$
for all $\delta{{:}\,}{\mathbb{D}}{\cal X}$.

Proof. These properties are immediate from Def. 28. $\Box$

A further property of UM-transformers is that they are 1-Lipshitz in a certain
sense:

######  Lemma 31.

$\textrm{wp}.h$ is 1-Lipschitz Take $h{{:}\,}{\mathbb{H}}{\cal X}$ and define
$t{{:=}\,}\textrm{wp}.h$. Let $|{\cdot}|$ be absolute value. Then $t$ is
$1$-Lipschitz in the sense that

$\sup_{\delta{{:}\,}{\mathbb{D}}{\cal
X}}\left|t.{u_{1}}.\delta-t.{u_{2}}.\delta\right|\hskip 10.00002pt\leq\hskip
10.00002pt\sup_{\delta{{:}\,}{\mathbb{D}}{\cal
X}}\left|{u_{1}}.\delta-{u_{2}}.\delta\right|~{}.$

Proof. Consider arbitrary $u_{1,2}{{:}\,}{\mathbb{U}}{\cal X}$. We reason

|  $\begin{array}[t]{@{}llll}\sup_{\delta{{:}\,}{\mathbb{D}}{\cal
X}}\left|\textrm{wp}.h.u_{1}.\delta-\textrm{wp}.h.u_{2}.\delta\right|\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}\sup_{\delta{{:}\,}{\mathbb{D}}{\cal X}}\left|{\cal E}_{h.\delta}\,u_{1}-{\cal E}_{h.\delta}\,u_{2}\right|\end{array}$
$\leq$ |  $\begin{array}[t]{@{}llll}\sup_{\delta{{:}\,}{\mathbb{D}}{\cal X}}~{}{\cal E}_{h.\delta}\,|u_{1}{-}u_{2}|\end{array}$ “property of $|\cdot|$”
$\leq$ |  $\begin{array}[t]{@{}llll}\sup_{\delta{{:}\,}{\mathbb{D}}{\cal X}}\quad{\cal E}_{h.\delta}\,(\sup_{\delta^{\prime}{{:}\,}{\mathbb{D}}{\cal X}}\left|u_{1}.{\delta^{\prime}}-u_{2}.{\delta^{\prime}}\right|)\end{array}$ “${\cal E}\,$ monotonic”
$=$ |  $\begin{array}[t]{@{}llll}\sup_{\delta{{:}\,}{\mathbb{D}}{\cal X}}\left|u_{1}.{\delta}-u_{2}.{\delta}\right|~{}.\end{array}$ “${\cal E}_{h.\delta}\,\mathbf{1}=1$ and rename $\delta^{\prime}$ to $\delta$”

$\Box$

Motivated by those lemmas, we define uncertainty transformers to be exactly
the functions in ${\mathbb{U}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{U}}{\cal
X}$ that satisfy the properties listed.

######  Definition 32.

The uncertainty transformers ${\mathbb{T}}{\cal X}$ The uncertainty
transformers ${\mathbb{T}}{\cal X}$ are the functions in ${\mathbb{U}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{U}}{\cal X}$ that satisfy Lems. 30,31.
$\Box$

We note that transformers ${\mathbb{T}}{\cal X}$ are closed under composition.
In §E.3 we show that refinement for ${\mathbb{T}}{\cal X}$ is pointwise
$(\leq)$.

###  9.4. UM-transformers back to abstract HMM’s

The function $\textrm{wp}.(\cdot)$ has been shown to be of type
${\mathbb{H}}{\cal X}{\mathbin{\rightarrow}}{\mathbb{T}}{\cal X}$. Here we
show that this correspondence is exact, i.e. that for every
$t{{:}\,}{\mathbb{T}}{\cal X}$ there is an $h{{:}\,}{\mathbb{H}}{\cal X}$ such
that $t{=}\textrm{wp}.h$ and, moreover, that the $h$ is unique.

The following theorem thus establishes the exact correspondence between
${\mathbb{H}}{\cal X}$ and ${\mathbb{T}}{\cal X}$, giving an analogue for
hidden-state probabilistic programs to the well-known correspondence between
demonic relations and conjunctive predicate transformers [20] that the former
correspond exactly to those functions from predicates to predicates that
distribution conjunction. (A further example, generalising that, is the
correspondence between demonic/probabilistic programs and super-linear
expectation transformers [22, 24].)

######  Theorem 33.

Characterisation of transformers For any $t{{:}\,}{\mathbb{T}}{\cal X}$ there
is a unique $h{{:}\,}{\mathbb{H}}{\cal X}$ such that $t{=}\textrm{wp}.h$.

Proof. Let $t{{:}\,}{\mathbb{T}}$. The construction of $h$ starts by showing
that the transformer $t$ can be extended into a linear function over the space
${\mathbb{C}}{\cal X}$ of continuous functions from ${\mathbb{D}}{\cal X}$ to
itself. This extension is executed in two phases. Firstly, we show that the
set ${\mathbb{U}}{\cal X}$ of continuous, concave and non-negative function
over ${\mathbb{D}}{\cal X}$ generates a sub-vector space of ${\mathbb{C}}{\cal
X}$. Thus, the first stage is an algebraic extension of $t$ to that generated
sub-space. This extension is necessarily unique by linearity (Lem. 30). The
second stage is a topological extension where ${\mathbb{C}}{\cal X}$ is
endowed with the norm uniform making it a Banach space. In fact, we show that
the sub-vector space generated by ${\mathbb{U}}{\cal X}$ is a dense sub-
algebra of ${\mathbb{C}}{\cal X}$ using the Stone-Weierstrass Theorem [25,
Thm. 5]. Thus the second stage of the extension is also unique by continuity.
Full technical details of these extensions are given in §G.

We now have a unique continuous linear function $\hat{t}$ from
${\mathbb{C}}{\cal X}$ to itself which coincides with $t$ on
${\mathbb{U}}{\cal X}$. We shall construct an $h$ such that $\textrm{wp}.h=t$.

Fix $\delta{{:}\,}{\mathbb{D}}{\cal X}$. The function

$f\hskip 10.00002pt\mapsto\hskip 10.00002pt\tilde{t}.f.\delta$

maps each continuous function $f{{:}\,}{\mathbb{C}}{\cal X}$ to
$\tilde{t}.f.\delta$ is a positive linear functional on ${\mathbb{C}}{\cal
X}$; moreover $\tilde{t}.\mathbf{1}.\delta=t.\mathbf{1}.\delta=1$, thus
$\mathbf{1}\mapsto 1$. Therefore, the Riesz Representation Theorem for linear
functionals [18, Ch. 2 Thm. 5.8] implies that there exists a unique Borel
probability measure $\Delta_{\delta}$ on ${\mathbb{D}}{\cal X}$ such that
$\tilde{t}.f.\delta={\cal E}_{\Delta_{\delta}}\,f$, for every
$f{{:}\,}{\mathbb{C}}{\cal X}$.

Define $h.\delta{:=}\,\Delta_{\delta}$ for each
$\delta{{:}\,}{\mathbb{D}}{\cal X}$. We now check that $h$ has the required
properties demanded by Lemmas 21,23.

Continuity: For the continuity assumption in Lem. 21, we let $\delta_{n}$ be a
sequence of distributions in ${\mathbb{D}}{\cal X}$ converging to
$\delta{{:}\,}{\mathbb{D}}{\cal X}$ with respect to the Kantorovich metric on
${\mathbb{D}}{\cal X}$. It suffices to show that the limit of
$d_{K}(h.\delta_{n},h.\delta)$ is $0$, as $n$ goes to infinity. Since
${\mathbb{D}}{\cal X}$ is compact, the Kantorivich metric metrizes the weak
topology and it suffices to show that $h.\delta_{n}$ converges weakly to the
Borel measure $h.\delta$. Let $f{{:}\,}{\mathbb{C}}{\cal X}$, we have

${\cal E}_{h.\delta_{n}}\,f=\tilde{t}.f.\delta_{n}$

Since $\tilde{t}.f$ is also continuous, the sequence $\tilde{t}.f.\delta_{n}$
converges to $\tilde{t}.f.\delta$ and thus, $h.\delta_{n}$ coverges weakly to
$h.\delta$. 151515This proof crucially depends on the compactness of
${\mathbb{D}}{\cal X}$. For Polish spaces, we can achieve the same result but
using a more general result by Rao [26, Thm. 3.1].

Super-linear: For the super-linearity assumption in Lem. 23, suppose that
$t{=}\textrm{wp}.h$ is in ${\mathbb{T}}{\cal X}$ and take arbitrary
$\delta_{1,2}{{:}\,}{\mathbb{D}}{\cal X}$. Then we reason

|
$\begin{array}[t]{@{}llll}h.\delta_{1}{\mathbin{{}_{p}\kern-0.50003pt+}}h.\delta_{2}~{}\ref{~}h.(\delta_{1}{\mathbin{{}_{p}\kern-0.50003pt+}}\delta_{2})\end{array}$
---|---
if |  $\begin{array}[t]{@{}llll}{\cal E}_{(h.\delta_{1}{\mathbin{{}_{p}\kern-0.35002pt+}}h.\delta_{2})}\,u~{}\leq~{}{\cal E}_{h.(\delta_{1}{\mathbin{{}_{p}\kern-0.35002pt+}}\delta_{2})}\,u\end{array}$ “for all $u{{:}\,}{\mathbb{U}}{\cal X}$ Lem. 27 Coriaceous”
if |  $\begin{array}[t]{@{}llll}\textrm{wp}.h.u.\delta_{1}{\mathbin{{}_{p}\kern-0.50003pt+}}\textrm{wp}.h.u.\delta_{2}\leq&\textrm{wp}.h.u.(\delta_{1}{\mathbin{{}_{p}\kern-0.50003pt+}}\delta_{2})\end{array}$ “Defn. wp.()”
if |<EMAIL_ADDRESS>X}~{},\end{array}$ “Defn. ${\mathbb{U}}{\cal X}$”

which was our assumption. $\Box$

With these characterisations, we now can prove two technical facts. In the
discrete case (as earlier) they seem self-evident. In the more general
setting, however, the work is mainly in ensuring well definedness (e.g. that
only measurable functions are integrated, etc.) The first establishes the
usual connection between composition, this time between the forward- and
backward semantics; the second confirms that ${\mathbb{H}}{\cal X}$ is closed
under composition (i.e. preserves continuity and super-linearity, as claimed
in Lem. 25).

######  Corollary 34.

Transformer composition For any $h_{1,2}{{:}\,}{\mathbb{H}}{\cal X}$ we have
that also $h_{1};h_{2}{\in}{\mathbb{H}}{\cal X}$, and furthermore that
$\textrm{wp}.(h_{1};h_{2})=\textrm{wp}.h_{1}\mathbin{\circ}\textrm{wp}.h_{2}$.

Proof. Direct calculation shows that
$\textrm{wp}.(h_{1};h_{2})=\textrm{wp}.h_{1}\mathbin{\circ}\textrm{wp}.h_{2}$,
although the working is intricate in the general (Giry) case. Well definedness
of $h_{1};h_{2}$ itself uses the simpler properties of (functional)
composition on the transformer side. See §H. $\Box$

Also, transformer composition respects refinement (§E.4).

##  10\. Gain- and loss functions define uncertainty measures

###  10.1. Gain- and loss functions

Although Def. 26 of uncertainty measures is abstract, they can be made
concrete via “gain functions” [8] or equivalently “loss functions” [4, Eqn.
(5)] that encode an attacker’s (e.g.) economic interest in the secrets and the
cost of obtaining them. We use loss functions here.

######  Definition 35.

Loss function determines uncertainty measure A _loss function_ ${\ell}$ is of
type $I{\mathbin{\rightarrow}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{R}}^{\geq}$ for some index set $I$, with the
intuitive meaning that ${\ell}.i.x$ is the cost to the attacker of using
“attack strategy” $i$ when the hidden value turns out actually to be $x$. Her
expected cost for an attack planned but not yet carried out is then ${\cal
E}_{\delta}\,({\ell}.i)$ if $\delta$ is the distribution in ${\mathbb{D}}{\cal
X}$ she believes to be governing $x$ currently.

From such an ${\ell}$ we define an uncertainty measure

$U_{\ell}.\rho\hskip 10.00002pt{:=}\,\hskip 10.00002pt\inf_{i{{:}\,}I}~{}{\cal
E}_{\rho}\,({\ell}.i)~{}.$ (9)

When $I$ is finite, the $\inf$ can be replaced by $\min$. $\Box$

The $\inf$ represents a rational strategy of minimising cost or risk, and a
typical attacker will act as follows: she chooses the attack strategy (i.e. he
chooses $i$) whose expected cost ${\cal E}_{\rho}\,({\ell}.i)$ to her, where
$\rho$ is the posterior in ${\mathbb{D}}{\cal X}$ she infers from her
observations in ${\cal Y}$, will be the least.

######  Lemma 36.

Well-definedness for Def. 35 For any loss function
${\ell}{{:}\,}I{\mathbin{\rightarrow}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{R}}^{\geq}$ the function $U_{\ell}$ in Def.
35 is continuous and concave.

Proof. We give here the proof for the finite-$I$ case. (The infinite case is
considered in [7, Sec III-B]; it might require further assumptions on $I$.)
Let ${\ell}$ be a loss function and $U_{\ell}$ be the associated uncertainty
measure.

$U_{\ell}$ is concave: Take $\rho_{1,2}{{:}\,}{\mathbb{D}}{\cal X}$ and
$p{{:}\,}[0,1]$. We have

|
$\begin{array}[t]{@{}llll}U_{\ell}.(\rho_{1}{\mathbin{{}_{p}\kern-0.50003pt+}}\rho_{2})\end{array}$
---|---
$=$ |  $\begin{array}[t]{@{}llll}\min_{i{{:}\,}I}\,({\cal E}_{\rho_{1}{\mathbin{{}_{p}\kern-0.35002pt+}}\rho_{2}}\,{\ell}.i)\end{array}$ “definition $U_{\ell}$”
$=$ |  $\begin{array}[t]{@{}llll}\min_{i{{:}\,}I}\,({\cal E}_{\rho_{1}}\,{\ell}.i{\mathbin{{}_{p}\kern-0.50003pt+}}{\cal E}_{\rho_{2}}\,{\ell}.i)\end{array}$ “$\lambda{\delta}\ \\!\mbox{\boldmath$\mathrel{\cdot}$}\ \\!{{\cal E}_{\delta}\,u}$ is linear”
$\geq$ |  $\begin{array}[t]{@{}llll}(\min_{i{{:}\,}I}{\cal E}_{\rho_{1}}\,{\ell}.i)\mathbin{{\mathbin{{}_{p}\kern-0.50003pt+}}}(\min_{i{{:}\,}I}{\cal E}_{\rho_{2}}\,{\ell}.i)\end{array}$ “$(\min f){{\mathbin{{}_{p}\kern-0.45003pt+}}}(\min g)$ $\leq\min(f{\mathbin{{\mathbin{{}_{p}\kern-0.45003pt+}}}}g)$”
$=$ |<EMAIL_ADDRESS>“definition $U_{\ell}$”

$U_{l}$ is continuous: Since $I$ is finite and each function $(\lambda{\rho}\
\\!\mbox{\boldmath$\mathrel{\cdot}$}\ \\!{{\cal
E}_{\rho}\,{\ell}.i})=(\lambda{\rho}\ \\!\mbox{\boldmath$\mathrel{\cdot}$}\
\\!{\sum_{x{{:}\,}{\cal X}}\rho_{x}{\times}{\ell}.i.x})$ is continuous, the
function $U_{\ell}$ is also continuous. $\Box$

Remarkably, loss functions are _complete_ for uncertainty measures: any
uncertainty measure in ${\mathbb{U}}{\cal X}$ can be expressed as $U_{\ell}$
for some loss function ${\ell}$ in $I{\mathbin{\rightarrow}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{R}}^{\geq}$, but possibly requiring $I$ to
be infinite [27]. Roughly speaking, this is because of the way concave
functions can be expressed as the envelope of their tangential hyperplanes:
the coefficients of the hyperplanes’ normals are the loss functions. 161616For
example, Shannon entropy requires infinite $I$, and the encoding is then
related to minimising the Kullback-Leibler divergence.

It is compellingly shown elsewhere how versatile loss (equiv. gain) functions
are [8]. Of particular interest is that Lem. 27 applies, both in the discrete
[4] and the continuous cases [5], even when uncertainties are restricted to
those generated by loss functions: the “distinguishing witness” constructed
for completeness is in fact a loss function [4].

##  11\. A UM-transformer example for §4.4

###  11.1. Profiling an attacker with a loss function

In the context of Fig. 4 we imagine an attacker whose livelihood depends on
her guessing whether $\texttt{xs}\verb+[0]+{=}\texttt{xs}\verb+[1]+$ or not,
finally. If he guesses incorrectly he loses $1; if correctly, he breaks even
(loses $0). This is as much a mathematical- as a _social_ issue: attacks will
be discouraged if they are not worthwhile for the attacker in terms of her own
criteria. (See also §4.4 for this social aspect.)

In this example, following §10, we express the attacker’s criteria as two
strategies “guess same” and “guess different” (thus $I=\\{\textsf{\small
same},\textsf{\small diff}\\}$) and a loss function ${\ell}$ therefore defined

$\begin{array}[]{rcl}{\ell}.\textsf{\small same}.(\verb+00+)&=&0\\\
\makebox[0.0pt][r]{$\dagger$\quad}{\ell}.\textsf{\small
same}.(\verb+01+)&=&1\\\ {\ell}.\textsf{\small same}.(\verb+10+)&=&1\\\
{\ell}.\textsf{\small same}.(\verb+11+)&=&0\\\ \end{array}\hskip
30.00005pt\begin{array}[]{rcl}{\ell}.\textsf{\small diff}.(\verb+00+)&=&1\\\
{\ell}.\textsf{\small
diff}.(\verb+01+)&=&0\makebox[0.0pt][l]{\quad$\ddagger$}\\\
{\ell}.\textsf{\small diff}.(\verb+10+)&=&0\\\ {\ell}.\textsf{\small
diff}.(\verb+11+)&=&1~{},\\\ \end{array}$

based on the informal description just above: for example if
$\texttt{xs}{=}\verb+01+$ but he guesses same, the case indicated by
$\dagger$, then he loses $1; but if he guesses diff, he breaks even
$\ddagger$. Using (9) we define our UM as $u.\delta=U_{\ell}.\delta=$

$\begin{array}[]{crcl}&{\ell}.\textsf{\small
same}.\delta&\min&{\ell}.\textsf{\small diff}.\delta\\\ =&{\cal
E}_{\delta}\,({\ell}.\textsf{\small same})&\min&{\cal
E}_{\delta}\,({\ell}.\textsf{\small diff})\\\
=&(\delta_{00}{+}\delta_{11})&\min&(\delta_{01}{+}\delta_{10})~{}.\end{array}$

###  11.2. Using UM’s and transformers to plan an attack

We can use our transformer semantics to answer $u$-dependent questions about
Fig. 4 over _all_ priors: we use the two we chose earlier in §4.4 as examples.

Writing $[\\![P]\\!]$ for the abstract HMM denoted by the two lines of code in
Fig. 4, we have for any $\pi$ that

$\textrm{wp}.[\\![P]\\!].u.\pi\hskip 10.00002pt=\hskip
10.00002pt\begin{array}[t]{@{}ll}&\pi_{00}~{}\min~{}(\pi_{01}{+}\pi_{10})/2\\\
+&\pi_{11}~{}\min~{}(\pi_{01}{+}\pi_{10})/2~{}.\end{array}$ (10)

(See §I below for how this $\textrm{wp}.(\cdot)$ is calculated.)

Now let $\pi^{\ref{f0544cm}}$ be the prior described by the initial comment in
Fig. 4. The attacker’s (expected) uncertainty wrt. the _final_ hyper
$[\\![P]\\!].\pi^{\ref{f0544cm}}$ is given by $\textrm{wp}.[\\![P]\\!].u$
applied to that _initial_ (uniform) prior $\pi^{\ref{f0544cm}}$, that is
$\textrm{wp}.[\\![P]\\!].u.\pi^{\ref{f0544cm}}=\nicefrac{{1}}{{2}}$ directly
from (10). Since $u.\pi^{\ref{f0544cm}}$ is also $\nicefrac{{1}}{{2}}$, he is
indifferent wrt. whether he should attack before or after $P$ has been allowed
to run.

Now suppose that $\texttt{xs}[0]{=}1$ is known initially, thus with prior
$\pi$ being $(0,0,\nicefrac{{1}}{{2}},\nicefrac{{1}}{{2}})$ so that $u$
applied initially gives $u.\pi{=}\nicefrac{{1}}{{2}}$. But $u$ applied finally
would give
$\textrm{wp}.[\\![P]\\!].u.\pi=(0\min\nicefrac{{1}}{{4}})+(\nicefrac{{1}}{{2}}\min\nicefrac{{1}}{{4}})=\nicefrac{{1}}{{4}}<\nicefrac{{1}}{{2}}$,
so that it is better to attack later even though xs might have been altered by
$P$. This scenario confirms that in fact for some priors, the program in Fig.
4 cannot be regarded as secure.

##  12\. HMM’s and the Dalenius Desideratum

Our abstracting from initial-state correlations allows a semantics for
programs’ _final_ states alone. Sometimes, however, leakage from the _initial_
state is important, even if that state is overwritten by the markov part of
the HMM: what the initial state _was_ might reveal information about what some
other correlated state still _is_ , even if that other state is not mentioned
in the program at all. This general concern was raised wrt. statistical
databases by Dalenius [10] who argued that it is inescapable; Dwork later gave
a proof of this [11]. Here is an (edited) extract from her paper:

> Suppose we have a statistical database that [records] average heights of
> population subgroups, and suppose further that it is infeasible to learn
> this information (perhaps for financial reasons) in any other way (say, by
> conducting a new study). Finally, suppose that one’s true height is
> considered sensitive.
>
> [An adversary having the] auxiliary information “Turing is two inches taller
> than the average Lithuanian woman” [would, with access to the database,
> learn] Turing’s height. In contrast, anyone without access to the database,
> knowing only the auxiliary information, learns much less about Turing’s
> height.

With our constructions here, we are able to see the Dalenius effect in
programming terms. The program that allows access to Dwork’s database of
Lithuanian heights (as above) might itself, in isolation, have been analysed
for security leaks. But if that program is run in a larger programming context
in which there is a (to be kept secret) variable tHeight containing Turing’s
height _and_ there is program code (external to the database-access code) that
establishes a correlation between the two, then running the database-access
program reveals information about tHeight even though that variable is not
mentioned anywhere in the database program.

In more austere terms, we would explain the effect as follows. A “classical”
sequential program does not affect variables to which it does not refer; for
example x:= E does not affect some other variable y in any way. But the
program  leak x  (recalling the notation of Fig. 3) can affect _what we know_
about variable y even though the program  leak x  does not refer to y at all.

Consider for example an input distribution
$(0,0)@\nicefrac{{1}}{{2}},(1,1)@\nicefrac{{1}}{{2}}$ on two variables (x,y).
Its y-marginal distribution is uniform on $\\{0,1\\}$. But the output hyper of
that program, projected onto y, is
$[0]@\nicefrac{{1}}{{2}},[1]@\nicefrac{{1}}{{2}}$, showing that the
distribution on y is now a point, no longer uniform: 171717Since the output is
a hyper, if knowledge of y were unaffected we would have the point hyper on
the uniform distribution, that is
$[0@\nicefrac{{1}}{{2}},1@\nicefrac{{1}}{{2}}]$. with probability
$\nicefrac{{1}}{{2}}$ that point will be $[0]$, and with probability
$\nicefrac{{1}}{{2}}$ that point will be $[1]$. Reviewing the leaks of x tells
us which point distribution on y we have, and we see essentially the Dalenius
effect between “database” x, “query”  leak x  and “third-party data” y.

This effect is exacerbated when we include state updates, as we have done with
our abstract HMM’s here. (Updates were not considered originally by Dalenius
or by Dwork.) For then the program  leak x; x:= 0  and the program  x:= 0
have the same abstract-HMM semantics on state-space (just) x, but different
semantics on state-space x,y. 181818On state-space x, both programs produce
the output hyper $[[0]]$ that denotes “x is certainly 0.” On x,y however, the
first might reveal something about y while the second cannot. The Dalenius
effect has become, in programming terms, a failure of compositionality wrt.
unreferenced global variables.

We show in this section how to deal with that: in brief, we include both the
initial- and the final values of the state in our semantics. The crucial point
is that we do not have to do more than that, in particular that we do not have
to consider “all possible third-party data y of any type”.

We now address the details. Consider a “constant” overwrite-by-x markov
$M^{\sf x}_{x,x^{\prime}}=\textit{1 if $x^{\prime}{=}{\sf x}$ else 0}$ for
some fixed ${\sf x}{{:}\,}{\cal X}$. Then $[\\![C{:}M^{\sf
x}]\\!]=[\\![{:}M^{\sf x}]\\!]$ for any channel $C$, because $C$ has no effect
on our knowedge of the final state. We know already what it is going to be.

We now adjust the semantics so that leakage from the initial state is
accounted for, even if it is subsequently overwritten. Let $C{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal Y}$ be a channel and $M{{:}\,}{\cal
X}{\mathbin{\rightarrowtriangle}}{\cal X}$ a markov, as usual, and let ${\cal
Z}$ be fresh. Write $C_{{\times}\kern-1.39998pt{\cal Z}}$ in $({\cal
X}{\times}{\cal Z}){\mathbin{\rightarrowtriangle}}{\cal Y}$ for the expanded
channel

$(C_{{\times}\kern-1.39998pt{\cal Z}})_{(x,z),y}\hskip 10.00002pt{:=}\,\hskip
10.00002ptC_{x,y}~{},$

i.e. that $C$ ignores $z$. Similarly $M_{{\times}\kern-1.39998pt{\cal
Z}}{{:}\,}({\cal X}{\times}{\cal Z}){\mathbin{\rightarrowtriangle}}({\cal
X}{\times}{\cal Z})$ is given by

$(M_{{\times}\kern-1.39998pt{\cal Z}})_{(x,z),(x^{\prime},z^{\prime})}\hskip
10.00002pt{:=}\,\hskip 10.00002pt\textrm{\quad$M_{x,x^{\prime}}$ if
$z{=}z^{\prime}$ else $0$}~{},$

i.e. so that $M$ does not change $x$. Thus these definitions ensure that for
any $\pi{{:}\,}{\mathbb{D}}({\cal X}{\times}{\cal Z})$ neither
$\pi{\rhd}(C_{{\times}\kern-1.39998pt{\cal Z}})$ nor
$\pi{\rhd}(M_{{\times}\kern-1.39998pt{\cal Z}})$ depends on the ${\cal Z}$
component. Take for example ${\cal Z}{:=}\,\\{z_{0},z_{1}\\}$ consider $C,M$
as below:

$C~{}=~{}\begin{array}[]{ccc}&y_{0}&y_{1}\\\\[4.5pt]
x_{0}{:}&\makebox[0.0pt]{\raisebox{-5.40005pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{13.50002pt}\right.\hskip
9.90007pt$}}1&0\makebox[0.0pt]{\raisebox{-5.40005pt}[0.0pt][0.0pt]{$\hskip
9.90007pt\left.\rule{0.0pt}{13.50002pt}\right)$}}\\\
x_{1}{:}&\nicefrac{{1}}{{4}}&\nicefrac{{3}}{{4}}\end{array}\hskip
27.00005ptM~{}=~{}\begin{array}[]{ccc}&x_{0}&x_{1}\\\\[4.5pt]
x_{0}{:}&\makebox[0.0pt]{\raisebox{-4.5pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{13.50002pt}\right.\hskip
8.09995pt$}}\nicefrac{{1}}{{2}}&\nicefrac{{1}}{{2}}\makebox[0.0pt]{\raisebox{-4.58995pt}[0.0pt][0.0pt]{$\hskip
8.09995pt\left.\rule{0.0pt}{13.50002pt}\right)$}}\\\
x_{1}{:}&\nicefrac{{1}}{{2}}&\nicefrac{{1}}{{2}}\end{array}$
$C_{{\times}\kern-1.25998pt{\cal Z}}\hskip 9.00002pt=\hskip
<EMAIL_ADDRESS>(x_{0},z_{0}){:}&\makebox[0.0pt]{\raisebox{-16.20004pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{25.20006pt}\right.\hskip
9.90007pt$}}1&0\makebox[0.0pt]{\raisebox{-16.20004pt}[0.0pt][0.0pt]{$\hskip
12.59996pt\left.\rule{0.0pt}{25.20006pt}\right)$}}\\\ (x_{0},z_{1}){:}&1&0\\\
(x_{1},z_{0}){:}&\nicefrac{{1}}{{4}}&\nicefrac{{3}}{{4}}\\\
(x_{1},z_{1}){:}&\nicefrac{{1}}{{4}}&\nicefrac{{3}}{{4}}\end{array}$
$M_{{\times}\kern-1.25998pt{\cal Z}}\hskip 9.00002pt=\hskip
9.00002pt\begin{array}[]{ccccc}&x_{0}z_{0}&x_{0}z_{1}&x_{1}z_{0}&x_{1}z_{1}\\\\[4.5pt]
x_{0}z_{0}{:}&\makebox[0.0pt]{\raisebox{-16.20004pt}[0.0pt][0.0pt]{$\left(\rule{0.0pt}{25.20006pt}\right.\hskip
9.90007pt$}}\nicefrac{{1}}{{2}}&0&\nicefrac{{1}}{{2}}&0\makebox[0.0pt]{\raisebox{-16.20004pt}[0.0pt][0.0pt]{$\hskip
14.40007pt\left.\rule{0.0pt}{25.20006pt}\right)$}}\\\
x_{0}z_{1}{:}&0&\nicefrac{{1}}{{2}}&0&\nicefrac{{1}}{{2}}\\\
x_{1}z_{0}{:}&\nicefrac{{1}}{{2}}&0&\nicefrac{{1}}{{2}}&0\\\
x_{1}z_{1}{:}&0&\nicefrac{{1}}{{2}}&0&\nicefrac{{1}}{{2}}\end{array}~{}.$

The definitions above show that in $C_{{\times}\kern-1.39998pt{\cal Z}}$ the
rows of the original $C$ are each repeated $2{=}{\\#{\cal Z}}$ times; and the
subsequent update by $M_{{\times}\kern-1.39998pt{\cal Z}}$ leaves ${\cal Z}$
unchanged. Observe that these definitions now account for information flows
with respect to initial distributions ${\mathbb{D}}({\cal X}{\times}{\cal Z})$
where, crucially, the ${\cal Z}$ component is merely “carried along”. But it
captures the Dalenius effect mentioned, as we now explain.

Consider an initial distribution $\pi{{:}\,}{\mathbb{D}}({\cal X}{\times}{\cal
Z})$ such that $\pi_{x_{i},z_{j}}=1$ if and only if $i{=}j$, i.e. that $z$ is
a copy of $x$’s initial value. We see that, even though ${\cal Z}$ is not
accessed by the program at all, if ever $y_{1}$ is observed then the ${\cal
Z}$ component must certainly be $z_{1}$, and if $y_{0}$ is observed then it is
$4$ times more likely to be $z_{0}$ than $z_{1}$.

Although ${\cal Z}$ is arbitrary, it can be shown that this Dalenius effect on
any ${\cal Z}$ can be determined by the HMM semantics _specifically in the
case where ${\cal X}{=}{\cal Z}$_ as just above. That is, we do not have to
consider “all ${\cal Z}$’s”, which would be impractical. Note the construction
of a fully compositional semantics for programs with hidden states is requires
further extensive conceptual and technical work which we have developed
elsewhere [28].

##  13\. Related work

There is great diversity in approaches to information flow in (probabilistic)
programs, which we have surveyed in our own earlier work [4, 5, 6, 7]. Here we
have concentrated on general techniques for semantic constructions, in
particular those based on monads, duality and refinement.

Refinement of probabilistic programs appeared in [29] where evaluations were
used to construct a powerdomain for probabilistic but possibly non-terminating
computations; this was extended to include demonic choice in the discrete case
in [22, 24], and was significantly generalised in [30]. Our “uncertainty
refinement” that combines information flow with functional properties first
appeared for information flow in straight-line programs in [4], was extended
to general measure spaces [5] and appeared independently for the specific case
of channels [8]. Whereas Jones and Plotkin began with an underlying partial
order over which to construct a probability space, our uncertainty-refinement
order begins “one level up”, using hyper-distributions ${\mathbb{D}}^{2}{\cal
X}$ to encode an “attack model” that accounts for information flow.

Doberkat defines _stochastic relations_ that correspond to forward-semantic
functions of type ${\cal X}{\mathbin{\rightarrow}}{\mathbb{D}}{\cal X}$ for
Markov processes: these are what we generalise by going “one level up”. The
converse of those stochastic relations [31] might improve the presentation of
our Def. 7, where a hyper is extracted from a channel and a prior, i.e. from a
joint distribution.

Dual models for program semantics include [20], then for probabilistic
programs [21, 23] in the purely probabilistic case. Subsequently [22] added
demonic choice. And [30, 32] study dual models for probability and
nondeterminism using a version of Riesz’s representation theorem.

In particular, Goubault-Larrecq’s approach [32] to combining probability and
nondeterminism differs from our earlier work [22]. It uses general denotations
for probabilistic programs in which nondeterminism is introduced at the level
of measures (by weakening the modularity law) rather than as healthy sets of
measures [22, 24, 30]. That leads naturally to a backward semantics of
probabilistic demonic programs because nondeterminism is captured within
integration. There is thus a strong analogy between our UM-transformers and
Goubault-Larrecq’s “previsions” because both are continuous functionals that
act on some set of tests (bounded continuous functions). The main difference
is that our UM-transformers are specifically tailored to capture security
semantics, which is what leads to concavity on our set of uncertainty
measures. Notice moreover that Goubault-Larrecq encounters a difficulty
similar to our composition of HMM’s, that the decomposition $[\\![C{:}M]\\!]$
(resp. collinearity) is not preserved by Giry composition. Indeed, both
difficulties are resolved by working in a larger space, namely, the space of
abstract HMM’s (resp. not-necessarily-collinear continuous previsions).

In [33] a dual model for Markov processes is used to prove properties about
approximations of finite behaviours, and in [34] it is shown how expectation
transformers relate to explicit program models described by Markov processes.

Recently Jacobs and Hasuo have explored a general categorical construction of
a backward transformer semantics from a forward monadic model of probabilistic
computations (discrete, continuous and quantum) [35, 36]. Their construction
uses measurability as the underlying feature of “predicates”, while the
stronger condition of continuity is crucial for our uncertainty measures. It
would be interesting to see whether an instantiation of that categorical
derivation can provide more structure for what we have done.

The concave functions advocated here for analysing information-flow properties
have appeared in [5, 8] and have been identified in [37] as an ingredient in
privacy analysis.

##  14\. Conclusions and prospects

Figure 6. Relationship between the semantic spaces.

Our principal objective was to provide an abstract setting for HMM’s based on
well understood principles of semantic spaces. We did that using Giry’s
general monadic framework applied at the level of ${\mathbb{D}}{\cal X}$
(rather than ${\cal X}$); the resulting structures include a refinement order
which is sensitive to both functional _and_ information-flow properties, and
they lead to a dual, transformer space supported by theorems demonstrating the
duality. Fig. 6 summarises the results:

— Top-left Fig. 6 shows the three-way joint distribution ${\mathbb{D}}({\cal
X}{\times}{\cal Y}{\times}{\cal X})$ produced by an HMM applied to a prior of
type ${\mathbb{D}}{\cal X}$: recall §3.1.

— At bottom-left we formulate _abstract HMM’s_ over a state ${\cal X}$, a type
${\mathbb{H}}{\cal X}$, as a monadic model for HMM’s over ${\cal X}$, and give
their characteristic properties: recall §3.2,6,8.

— At top-right we have _uncertainty measures_ ${\mathbb{U}}{\cal X}$ as a
generalisation of diverse entropies (top centre), and we gave their
characteristic properties: recall §9.1.

— We showed (centre right) that uncertainty measures have a complete
representation as _loss functions_ ; recall §10.

— We gave a dual, uncertainty-transformer semantics ${\mathbb{T}}{\cal X}$ of
${\mathbb{H}}{\cal X}$, stating its characteristic properties (bottom right)
and proved that they enable the duality with ${\mathbb{H}}{\cal X}$ (centre):
recall Thm. 33 in §9.2.

— We showed how all of that is an instance of the general Giry monad as a
computation, of which (finite) HMM’s use a discrete portion (bottom centre):
recall §7.

— We explained how the “Dalenius effect” is manifested as a compositional
issue in this framework, and suggested how it can be treated: recall §12.

— We stated and proved Thm. 33, which we believe is a significant new result,
in particular its assumptions and proof.

More abstractly (recall §1.2), we aimed to profit by joining two ideas: the
established use of HMM’s as descriptions of probabilistic mechanisms having
hidden state, and the established use of monads for modelling computations.
Our novel use of ${\mathbb{D}}{\cal X}$ in the monad, rather than the state
${\cal X}$ itself, is the principal innovation that allowed this; and the
synthesised hyper-distribution space that results leads to other advantages
(the two $\dagger$’s below).

An immediate benefit accrues because, in monad-enabled programming languages,
probabilistic-programming packages can be built very quickly and e.g. [38] is
just one of many examples. Indeed the translation into real programs is almost
elementary because of the powerful and general structures available: the
Haskell prototype independently verifies the examples in Figs. 2–5. (See §5
for an overview.)

More importantly, any monad brings with it both general equational properties
and specific properties applying to the monad in question (such as those in
[2]). These conceptual tools allow reasoning about the structures modelled
(HMM’s in this case) in ways that would be obscured by their more direct
operational representation (e.g. as matrices).

$\dagger$ The other advantages of hypers are several: one is that they
abstract from differences between entropies in a way that allows all of the
entropies to be used uniformly. For example, a hyper contains all the
information necessary to calculate the information leakage of a particular
program fragment (typically, in the security literature, a pure channel §3.4),
as shown in [6], and furthermore the Kantorovich-metric structure of
${\mathbb{D}}{\cal X}$ we used earlier for channels [7] now carries over to
HMM’s.

$\dagger$ Another advantage of hypers is that their partial-order enables
semantics for “looping HMM’s” in the standard way (least fixed-point) for
computer science, rather than a direct ad-hoc definition based on matrices.
Indeed a typical use of HMM’s is to run a single HMM-step (§3.1) repeatedly
and then to make statistical deductions about its hidden features:
sophisticated mathematical tools are available for this special case [12]. Via
abstract HMM’s we can however, in principle, handle complex, heterogeneous
systems beyond (what amounts to, in the special case just above) a single loop
containing just a single statement.

Our more concrete aim (again §1.2) was to allow source-level reasoning about
probabilistic programs with hidden state. Historically _at the source level_
this works best with backwards reasoning based on predicates (or similar) that
can be embedded between program statements rather than forwards reasoning
which, here, would be calculations using ${\mathbb{D}}{\cal
X}{\mathbin{\rightarrow}}{\mathbb{D}}^{2}{\cal X}$ directly.

Here our “predicates” are UM’s, which in this paper however are mathematical
objects unsuitable for embedding directly in program texts (see §I, last
paragraph) As remarked in §10.1, however, any UM can be expressed as $U_{l}$
for some loss-function $l$ which function –crucially– is indeed an expression
based on program variables [27]. The added complexity introduced by the hidden
state is that the program-logic based on that observation must represent the
index-set ($I$) of the loss function; that would most likely be done by adding
a special-purpose quantifier (since the loss-function index must be a bound
variable within the assertion, not appearing in the program proper).

Exploiting this opportunity for a source-level quantitative logic of
probabilistic hidden state is planned for future work.

Acknowledgements We’re grateful for advice from Franck van Breugel, James
Worrell, Tom Schrijvers and other members of IFIP WG 2.1, and for inspiration
and insight from the INRIA Princess team. We acknowledge support from the
Australian Research Council’s grant DP120101413 and the INRIA équipe associée
Princess; and Morgan acknowledges the support of Data61.

## References

  * [1] E. Moggi, “Computational lambda-calculus and monads,” in _Proc. 4th IEEE Symp. LiCS_ , 1989, pp. 14–23.
  * [2] M. Giry, “A categorical approach to probability theory,” in _Categorical Aspects of Topology and Analysis_ , ser. Lecture Notes in Mathematics. Springer, 1981, vol. 915, pp. 68–85.
  * [3] A. McIver, L. Meinicke, and C. Morgan, “Hidden-Markov program algebra with iteration,” _Mathematical Structures in Computer Science_ , 2014.
  * [4] ——, “Compositional closure for Bayes risk in probabilistic noninterference,” in _Proc. 37th Int. Colloq. ICALP 2010, Part II_ , 2010, pp. 223–235.
  * [5] ——, “A Kantorovich-monadic powerdomain for information hiding, with probability and nondeterminism,” in _Proc. 27th Symp. LiCS_ , 2012, pp. 460–70.
  * [6] A. McIver, C. Morgan, G. Smith, B. Espinoza, and L. Meinicke, “Abstract channels and their robust information-leakage ordering,” in _Proc. 3rd Conf. PoST (ETAPS)_ , ser. Lecture Notes in Computer Science, M. Abadi and S. Kremer, Eds., vol. 8414. Springer, 2014, pp. 83–102.
  * [7] M. S. Alvim, K. Chatzikokolakis, A. McIver, C. Morgan, C. Palamidessi, and G. Smith, “Additive and multiplicative notions of leakage, and their capacities,” in _Proc 27th IEEE Symp. CSF_. IEEE, 2014, pp. 308–322.
  * [8] M. S. Alvim, K. Chatzikokolakis, C. Palamidessi, and G. Smith, “Measuring information leakage using generalized gain functions,” in _Proc. 25th IEEE Symp. CSF_ , Jun. 2012, pp. 265–79.
  * [9] G. Smith, “On the foundations of quantitative information flow,” in _Proc. 12th Conf. FoSSaCS (ETAPS)_ , ser. Lecture Notes in Computer Science, L. de Alfaro, Ed., vol. 5504, 2009, pp. 288–302.
  * [10] T. Dalenius, “Towards a methodology for statistical disclosure control,” _Statistik Tidskrift_ , vol. 15, pp. 429–44, 1977.
  * [11] C. Dwork, “Differential privacy,” in _Proc. 33rd Int. Colloq. ICALP_ , 2006, pp. 1–12.
  * [12] D. Jurafsky and J. Martin, _Speech and Language Processing_. Prentice Hall International, 2000.
  * [13] T. M. Cover and J. A. Thomas, _Elements of Information Theory_ , 2nd ed. John Wiley & Sons, Inc., 2006\.
  * [14] D. Fremlin, _Measure Theory_. Torres Fremlin, 2000.
  * [15] J. Gibbons, A. McIver, C. Morgan, and T. Schrijvers, “Quantitative information flow with monads in haskell,” 2018, submitted for review.
  * [16] J. Landauer and T. Redmond, “A lattice of information,” in _Proc. 6th IEEE CSFW’93_ , Jun. 1993, pp. 65–70.
  * [17] F. van Breugel, “The metric monad for probabilistic nondeterminism,” 2005, www.cse.yorku.ca/
$\sim$franck/research/drafts/monad.pdf.

  * [18] K. R. Parthasarathy, _Probability Measures on Metric Spaces_. AMS Chelsea Publishing, 1967.
  * [19] A. L. Gibbs and F. E. Su, “On choosing and bounding probability metrics,” _International Statistical Review_ , vol. 70, no. 3, pp. 419–435, 2002. [Online]. Available: http://dx.doi.org/10.1111/j.1751-5823.2002.tb00178.x
  * [20] E. Dijkstra, _A Discipline of Programming_. Prentice-Hall, 1976.
  * [21] D. Kozen, “A probabilistic PDL,” in _Proc. 15th ACM Symp. Theory of Computing_. ACM, 1983, pp. 291–7.
  * [22] C. Morgan, A. McIver, and K. Seidel, “Probabilistic predicate transformers,” _ACM Trans Prog Lang Sys_ , vol. 18, no. 3, pp. 325–53, 1996.
  * [23] C. Jones, “Probabilistic nondeterminism,” Edinburgh University, Monograph ECS-LFCS-90-105, 1990, (Ph.D. Thesis).
  * [24] A. McIver and C. Morgan, _Abstraction, Refinement and Proof for Probabilistic Systems_ , ser. Tech Mono Comp Sci. Springer, 2005.
  * [25] M. H. Stone, “The generalized Weierstrass approximation theorem,” _Math Magazine_ , vol. 21, no. 4, pp. 167–184, March 1948.
  * [26] R. Ranga Rao, “Relations between weak and uniform convergence of measures with applications,” _Annals of Mathematical Statistics_ , vol. 33, no. 2, pp. 659–680, January 1962.
  * [27] K. Chatzikokolakis, Private communications, 2014.
  * [28] A. McIver, C. C. Morgan, and T. M. Rabehaja, “Algebra for quantitative information flow,” in _Relational and Algebraic Methods in Computer Science - 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings_ , 2017, pp. 3–23. [Online]. Available: https://doi.org/10.1007/978-3-319-57418-9_1
  * [29] C. Jones and G. Plotkin, “A probabilistic powerdomain of evaluations,” in _Proc. 4th IEEE Symp. LiCS_ , 1989, pp. 186–95.
  * [30] R. Tix, K. Keimel, and G. Plotkin, “Semantic domains for combining probability and non-determinism,” _Electron. Notes Theor. Comput. Sci._ , vol. 222, pp. 3–99, 2009.
  * [31] E. Doberkat, “The converse of a stochastic relation,” in _Proc. 6th Conf. FoSSaCS (ETAPS)_ , ser. LNCS, A. Gordon, Ed., vol. 2620. Springer-Verlag, 2003, pp. 233–49.
  * [32] J. Goubault-Larrecq, “Continuous previsions,” in _Proc. 16th EACSL_ , ser. Lecture Notes in Computer Science, vol. 4646. Springer, 2007, pp. 542–57.
  * [33] P. Chaput, V. Danos, P. Panangaden, and G. D. Plotkin, “Approximating Markov processes by averaging,” _J. ACM_ , vol. 61, no. 1, 2014.
  * [34] F. Gretz, J. Katoen, and A. McIver, “Operational versus weakest pre-expectation semantics for the probabilistic guarded command language,” _Perform. Eval._ , vol. 73, pp. 110–132, 2014.
  * [35] B. Jacobs, “Measurable spaces and their effect logic,” in _Proc. 28th LiCS_ , 2013, pp. 83–92.