Reasoning about resources used during the execution of programs, such
as time, is one of the fundamental questions in computer science. When
programming with probabilistic primitives, however, different samples
may result in different resource usage, making the cost of a program
not a single number but a distribution instead.

The expected cost is an important metric used to quantify the
efficiency of probabilistic programs. In this work we introduce
$\mathbf{cert}$, a call-by-push-value (CBPV) metalanguage extended
with primitives for probability, cost and unbounded recursion, and
give it denotational semantics for reasoning about the average cost of
programs. We justify the validity of the semantics by presenting
case-studies ranging from randomized algorithms to stochastic
processes and showing how the semantics captures their intended cost.

For the purpose of Open Access the author has applied a CC BY public copyright
licence to any Author Accepted Manuscript version arising from this submission.

§ INTRODUCTION

In a field where efficiency is almost as important as correctness, reasoning about the runtime cost of algorithms is of upmost importance.
As such, algorithm designers and theoreticians have developed mathematical tools to aid them in reasoning about the cost of programs.
A notable example is the use of recurrence relations to express the recursive cost structure of recursive programs. Computer scientists
very early in their education learn, for instance, that merge sort's cost is given by the follwing recurrence relation

\begin{align*}
T(0) &= 0\\
T(n) &= 2T(n/2) + n
\end{align*}

Which gives $O(n \log n)$ complexity. How can we formalize this claim? For simple pseudocode we can use our intuitions to correctly reason about its cost. But, when
the language is more expressive either because it has computational effects, higher-order functions or inductive types, it becomes less clear how
to assign costs to programs.

These issues have been explored by Danner et al <cit.>, where the authors, in a span of several papers, have developed semantic techniques that lay on firm ground
the cost analysis of functional programs with inductive types. This line of work has culminated in <cit.>, where the authors use
a Call-By-Push-Value (CBPV) metalanguage and the writer monad to define a recurrence extraction mechanism for a functional language with recursion and list datatypes.

Though their results are impressive, the only effect their technique can handle is recursion. This is limiting because many problems can be solved
more efficiently by, for instance, having access to probabilistic primitives, so-called randomized algorithms <cit.>.

A notable example is a probabilistic variant of the quicksort algorithm. In the worst case, i.e. when the list is in reverse order,
quicksort requires $O(n^2)$ comparisons, a far-cry from its promised complexity $O(n\log(n))$. By being able to uniformly sample
elements from the input list you can average out this worst case and recover an average cost of $O(n\log(n))$.

Due to the applicability of probabilistic algorithms, a lot of theoretical work has gone in developing the mathematical definitions and
tools used for reasoning about them. In particular, for these algorithms, the familiar notion of cost is replaced by
expected cost. Instead of considering the cost of a single execution, you average it over every probabilistic sampling done throughout
the execution of the program. Familiar tools from deterministic cost analysis such as recurrence relations, have also been successfully
developed in the probabilistic setting <cit.>.

Unfortunately, much like in the deterministic case before the work of Danner et al,
there has not been a systematic semantic study of how to bring these cost analysis concepts to expressive functional languages.

Our Work: Compositional Methods for Probabilistic Cost In this work we give semantic foundations for
reasoning about expected cost in the context of recursive probabilistic functional programs with lists. We start
by defining $\meta$: a CBPV metalanguage with operations for sampling from uniform distributions and for incrementing the cost of programs.
This metalanguage is expressive enough to represent the cost structure of recursive probabilistic algorithms and stochastic processes.

Besides equipping our metalanguage with an equational theory, we make its semantics concrete by providing two denotational semantics for
reasoning about the cost of probabilistic programs. The first one, which we call the cost semantics, uses the familiar
writer monad transformer to combine the cost monad with a subprobability monad. The second semantics, which we call the
expected cost semantics, encapsulates the compositional structure of the expected cost as a monad, allowing us to give a
denotational semantics that keeps track of the expected cost of programs.

Then, in order to justify the mutual validity of these distinct semantics, we show that the expected cost semantics is a sound
approximation to the cost semantics and to the equational theory. In the absence of recursion, we show that this approximation
is an equality while it is an inequality in the presence of unbounded recursion.

As applications, we showcase the capabilities of our semantics by using it to reason about the expected cost of the probabilistic algorithms quicksort and quickselect
and stochastic processes such as a symmetric random walk. As a guiding example, throughout the paper we will use geometric distributions to illustrate
different aspects of $\meta$ and its semantics.

Our approach contrasts with other work done on expected cost analysis <cit.>
where the language analyzed was either imperative or first-order, or the cost structure was given by non-compositional methods.
In spirit, the closest to what we have done is <cit.>, which does denotational cost analysis in a deterministic recursive setting.

Our contributions In summary, our contributions are the following:

* We define $\meta$, a CBPV variant with primitives for increasing cost ($\charge c$) and for sampling from uniform distributions ($\rand$) (<ref>)

* We define an equational theory for reasoning about the expected cost of programs (<ref>)

* We define a cost semantics, an expected cost semantics and show that the latter is sound with respect to the former (<ref>)

* We prove that both semantics are sound with respect to the equational theory (<ref>)

* We justify the validity of the expected cost semantics by reasoning about two stochastic processes and two randomized algorithms (<ref>)

§ $\META$ : A PROBABILISTIC COST-AWARE METALANGUAGE

\begin{align*}
& \overline{\tau} \defined F \tau \smid \tau \to \overline \tau \\
& \tau \defined U \overline{\tau} \smid 1 \smid \nat \smid \tau \times \tau
\end{align*}

\begin{align*}
& t,u \defined \lamb x t \smid \app t V \smid \ifthenelse V t u \smid \force\, V \smid (x \leftarrow t); u\\
& \smid \produce V \smid \letbe x V t \smid \mathsf{succ}\, t \smid \mathsf{pred}\, t \\
&\smid \letin {(x, y)} V t \\
& V \defined x \smid () \smid n \in \nat \smid \thunk\, t \smid (V_1, V_2)
\end{align*}

Types and Terms of CBPV

Γ_1, x : τ, Γ_2 x : τ

n ∈Γn :

Γ() : 1

ΓV :
Γt : τ
Γu : τΓ⊢^c V t u : τ

ΓV_1 : τ_1
ΓV_2: τ_2Γ(V_1, V_2) : τ_1 ×τ_2

Γt : F Γ𝗉𝗋𝖾𝖽  t : F

Γt : F Γ𝗌𝗎𝖼𝖼  t : F

Γ, x : τt : τΓx t : τ→τ

ΓV : τ
Γt : τ→τΓt V : τ

ΓV : τΓV : F τ

Γt : τΓt : U τ

ΓV : U τΓV : τ

Γt : F τ'
Γ, x : τ' u : τΓ(x ←t); u : τ

ΓV : τ_1 ×τ_2
Γ, x : τ_1, y : τ_2 t : τΓ(x,y) V t : τ

CBPV typing rules

Call-By-Push-Value is a metalanguage that provides fine-grained control over
the execution of programs. This is achieved by distinguishing, at the type level, between values and computations, and by adding syntax for suspending and resuming
the execution of programs <cit.>.
By appropriately using these forcing and suspension primitives, it is possible to embed both Call-By-Name (CBN) and Call-By-Value (CBV) calculi into CBPV. Since
we are interested in a uniform treatment of expected cost without restricting ourselves to one particular evaluation strategy, we use CBPV as our base language.

<Ref> depicts the CBPV syntax, note that the base types $1$ and $\nat$ are value types and arrow types are computation types that receive as input a value type and output a computation type. At the center of the CBPV formalism are the type
constructors $F$ and $U$ which allows types to move between value types and computation types. The constructor $F$ plays a similar role to the monadic type constructor $T$ from the monadic $\lambda$-calculus <cit.>, while $U$ is used to represent suspended — or thunked — computations.

This two-level approach also manisfests itself at the type judgement level, where the judgement $\Gamma \vdashval V : \tau$ is only defined for value types while $\Gamma \vdashcomp t : \overline{\tau}$ is defined for computation types, as shown in <Ref>. Both contexts only bind values, which justifies the arrow type having a value type in its domain, so that lambda abstractions will only introduce values to the context. The if-then-else operation checks if the value $V$ is $0$, in which case it returns the first branch, and otherwise it returns the second branch. The operations $\mathsf{pred}$ and $\mathsf{succ}$ are the predecessor and successor functions, respectively. The product introduction rule pairs two values while its elimination rule unpairs a product and uses them in a computation. Lambda abstraction binds a new value to the context while application applies a function to a value.

The less familiar rules are those for the type constructors $F$ and $U$. The introduction rule for computations is $\produce V$, which is the computation that does not incur any effect and just outputs the value $V$, while the introduction rule for $U$, $\thunk\, t$ suspends the computation $t$. Its elimination rule, $\force V$ resumes the
suspended computation $V$. The last rule, $x \leftarrow t; u$ is what makes it possible to chain effectful computations together, since it receives a computation of type $F\tau$ as input, runs it and binds the result to the continuation $u$, which eventually will output a computation of type $\overline \tau$. This is a generalization of the monadic $\mathsf{let}$ rule where the output type does not have to be of type $F\tau$.

Though the syntax differs a bit from the monadic semantics of effects, every strong monad over a Cartesian closed category can interpret
the CBPV calculus, as we describe in <Ref>.

Though this language is effective as a core calculus, by itself it cannot do much, since it has no “native” effect operations,
meaning that there are no programs with non-trivial side-effects. In this section we will extend it CBPV so that it can program with
three different effects: cost, probability and unbounded recursion. We call this extension $\meta$, for calculus for expected run time,
and we conclude the section by presenting its equational theory.

§.§ Cost and Probabilistic Effects

As it is common in denotational approaches to cost semantics, it is assumed that there is a cost
monoid $\cmon$ — usually interpreted by $\nat$ and addition — which acts on programs by
operations $\charge c$ that increases the current cost of the computation
by $c$ units, for every $c : \cmon$. The value types are extended with a type $\cmon$ and constants $\cdot \vdashval c : \cmon$.
Furthermore, since we also want to program with probabilities and unbounded recursion, we
extend the language with a sampling primitive, as well as recursive definitions:

ΓV : ΓV : F 1
ΓV : Γ  V : F
Γ, x : U τt : τΓx.  t : τ

The operation $\rand\, V$ uniformly samples a natural number in the
interval $[ 0, V ]$ and $\fix$ is the familiar fixed-point operator used for defining recursive programs.
In interest of reducing visual polution,
$\charge V; t$ desugars to $(x \leftarrow \charge V);  t$, when $x$ is not used in the body of $t$.

[Geometric distribution]
With these primitives we can already program non-trivial distributions. For instance, the geometric distribution
can be expressed as the program

\[\cdot \vdashcomp \fix x.\, (\produce 0) \oplus ((y \leftarrow \force x); \produce (1 + y)) : F \nat,\]

where $t \oplus u$ is syntactic sugar for $(x \leftarrow \rand\, 1); {\ifthenelse x t u}$, i.e. it uniformly chooses between
the left and right branch. Operationally, the program
flips a fair coin, if the output is $0$, it outputs $0$, otherwise it recurses on $x$, binds the value to $y$ and
outputs $1 + y$.

By having fine-grained control over which operations have a cost, it is possible to decide which costs are reasoned about.
For instance, if we want to keep track of how many coins were tossed when running the geometric distribution, we can modify it
as such

\[
\fix x.\, \charge 1 ; (\produce 0) \oplus (y \leftarrow \force x; \produce (1 + y)) : F \nat
\]

[Deterministic Programs]
The $\mathsf{charge}$ operation can also be used to keep track of the number of recursive calls
in your program. For instance, a recursive program that computes the factorial function can be instrumented
to count the number of recursive calls as follows:

\[\fix f.\, \lamb n {\ifthenelse{n}{(\produce 0)}{(\charge 1; n * f(n-1))}}\]

Whenever the if-guard is false, the cost is incremented by $1$ and the function is recursively called.

§.§ Lists

Frequently, cost analysis are defined for algorithms defined over inductive data types, such as lists.
As such, we will also extend our language with lists over value types.

\begin{align*}
\tau \defined \cdots \smid \listty \tau
\end{align*}

Γ⊢^v 𝗇𝗂𝗅 : τ
Γ⊢^v V_1 : τ
Γ⊢^v V_2 : τΓ⊢^v 𝖼𝗈𝗇𝗌  V_1   V_2 : τ
Γ⊢_v V : τ
Γ⊢^c t : τ
Γ, x : τ, xs : τ⊢^c u : τ
Γ⊢^c Vtu : τ

The primitive $\mathsf{nil}$ is the empty list, $\mathsf{cons}$ appends a value to the front of a list and $\mathsf{case}$ is for
pattern-matching on lists and, in the presence of $\fix$, can be used for defining non-structurally recursive functions over lists.

The function that computes the length of a list can be defined as

\begin{align*}
&\mu f : \listty \tau \to F \nat.\, \lambda l : \listty \tau.\,\\
&\mathsf{case} \, l \, \mathsf{of}\\
& \mid \mathsf{nil} \Rightarrow \\
& \quad \produce 0\\
&\mid \mathsf{(hd, tl)} \Rightarrow \\
& \quad n \leftarrow \app {(\force f)} {tl}\\
&\quad \produce (1 + n)
\end{align*}

A binary version of the familiar filter function that outputs two lists, one for the true elements and the other for the false elements can be written as

\begin{align*}
&\mu f : \listty \tau \to F (\listty \tau \times \listty \tau) .\,\\
&\lambda l : \listty \tau\,.\\
&\lambda p : \tau \to F \nat.\,\\
&\mathsf{case} \, l \, \mathsf{of}\\
& \mid \mathsf{nil} \Rightarrow \\
& \quad \produce (\mathsf{nil}, \mathsf{nil})\\
&\mid \mathsf{(hd, tl)} \Rightarrow \\
& \quad n \leftarrow \app p hd\\
& \quad (l_1, l_2) \leftarrow \app {\app{(\force f)} p} tl\\
&\quad \mathsf{if}\, n \, \mathsf{then}\\
& \quad \quad \produce (\mathsf{cons}\, hd\, l_1, l_2)\\
&\quad \mathsf{else}\\
& \quad \quad \produce (l_1,\mathsf{cons} \, hd\, l_2)\\
\end{align*}

Since we have adopted a $\nat$-valued if-statement, the predicate $p$ above
outputs a natural number.

We can use the functions above and write a randomized version of the quicksort algorithm that counts the number of comparisons done as follows:

\begin{align*}
&\mu f : \listty \nat \to F (\listty \nat) .\,\\
&\lambda l : \listty \nat.\,\\
&\mathsf{case} \, l \, \mathsf{of}\\
& \mid \mathsf{nil} \Rightarrow \\
& \quad \produce \mathsf{nil}\\
&\mid \mathsf{(hd, tl)} \Rightarrow \\
& \quad len \leftarrow \app \mathsf{length}\, l\\
& \quad r \leftarrow \app \rand len\\
& \quad pivot \leftarrow l[r]\\
& \quad (l_1, l_2) \leftarrow \app {\app{biFilter} {(\lamb n {\charge 1; n \leq pivot})}} l\\
& \quad less \leftarrow \app {\force f} {l_1}\\
& \quad greater \leftarrow \app {\force f} {l_2}\\
& \quad \produce (less \mdoubleplus pivot :: greater)\\
\end{align*}

In the program above we are accessing the $r$-th element of a list $l$ using the familiar syntax $l[r]$.
The algorithm is very similar to the non-randomized quicksort with the exception of uniformly choosing an
element from the input list as the pivot.

We conclude this section by mentioning that there are many other sensible extensions, such as recursive and sum types. For our purposes,
they are not necessary and so, in order to keep the language simple, we omit them. That being said, from a semantic point of view,
these extensions are well-understood and straightforward to be accommodated by the denotational semantics we present in

§.§ Equational Theory

\begin{align*}
x \oplus_0 y &= x\\
x \oplus_{p} y &= y \oplus_{1-p} x\\
x \oplus_p x &= x\\
x\oplus_p (y \oplus_q z) &= (x \oplus_{pq} y) \oplus_{\frac{p(1-q)}{1 - pq}} z
\end{align*}

Barycentric Algebra Axioms

Γ, x : τt : τ
Γ⊢_v V : τΓ⊢t V x = (x t) V : τ

Γt : τ→τΓ(x t x) = t : τ→τ

Γt : τΓ⊢(0; t) = t : τ

Γ⊢c; d = c + d : F 1

Γt : τΓ⊢((t)) = t: τ

Γt : τ  Γu : τΓ⊢0 t u = t: τ

Γt : τ  Γu : τΓ⊢(n + 1) t u = u : τ

Γ, x : U τt : τΓ⊢t = t x (x.  t) : τ

Equational Theory (Selected Rules)

We want to define a syntactic sound approximation to the expected cost of programs. We do this by extending the usual equational
theory of CBPV with rules for the monoid structure of the $\mathsf{charge}$ operation. We present most of the equational theory
in <Ref>, with the other rules shown in <Ref>.

An alternative axiomatization of probabilistic effects
is given by barycentric algebras, which are sets equipped with a collection of binary operations $\{\oplus_p\}_{p\in[0,1]}$ satisfying the
equations depicted in <Ref>. From an
operational point of view, these operations capture a weighted binary choice between two computations.

Under this axiomatization and by making the cost monoid “continuous”, it is also reasonable to add the equation:

\[(\charge {c_1}; t) \oplus_p (\charge {c_2}; u) = \charge {pc_2 + (1-p)c_1}; (t \oplus_p u)\]

This equation can be quite useful for simplifying branching processes. For instance, for a modified geometric distribution where you only
keep track of the number of non-zero coin flips we get the following rewrites

\begin{align*}
&(\produce 0) \oplus (\charge 1; y \leftarrow \force x; \produce (1 + y)) =\\
&(\charge 0; \produce 0) \oplus (\charge 1; y \leftarrow \force x; \produce (1 + y)) =\\
&\charge {0.5}; (\produce 0) \oplus (y \leftarrow \force x; \produce (1 + y))
\end{align*}

Which allows us to get quantitative bounds on how this variant relates to the original geometric distribution.
Indeed, it can be calculated that the original distribution has expected value $2$ while this one has expected cost $1$.

In order to keep $\meta$ as simple as possible, only $\rand$ will be a part of its surface syntax, but in its full equational
definition in <Ref>, we present it with the barycentric algebra operations and equations.
Though this seems like a simple equatoinal theory, as we will see in <Ref>, the interaction of cost, probability and recursion has unexpected consequences.

§ DENOTATIONAL SEMANTICS

This section presents two concrete denotational semantics to our language. Since $\meta$ contains higher-order functions,
unbounded recursion and probabilistic primitives, we are somewhat limited in our choice of semantic domain. Work by Vakar et al. <cit.>
on probabilistic semantics has defined the category of $\omega$-quasi Borel spaces $\wqbs$ which satisfies all of our requirements and
we choose it as our base category. This category was first defined as a variant of the quasi Borel space category <cit.> that preserves many of its good
categorical properties, such as being Cartesian closed and having commutative probability monads, with the exception that it can interpret unbounded recursion,
which is of significant importance for programming language semantics.

The category $\wqbs$ admits commutative probabilistic powerdomains that can interpret
probabilistic primitives such as $\rand$. In particular, $\wqbs$ admits a probabilistic powerdomain of subprobability distributions $\Psub$
and, by using the writer monad transformer $\Psub(\cmon \times -)$, it can also accommodate cost operations, as we explain in <Ref>.
With this new monad, it is possible
to use the CBPV algebraic semantics to reason about the expected cost of programs by computing the marginal distribution over $\cmon$
and computing its expected value.

Unfortunately, this approach is non-compositional. In order to compute the expected cost of a program of type $F\tau$,
we must first compute its (compositional) semantics which can then be used to obtain a distribution over the cost and then apply the expectation formula to it.
We work around this issue by constructing a novel expected cost monad in <Ref> that makes the expected cost a part of the semantics
and, as such, it is compositionally computed.

We start this section by going over the important constructions for $\wqbs$, we define the cost semantics, followed by the expected cost semantics
and, in order to justify their soundness, we show that the expected cost semantics is a sound approximation of the cost semantics by a logical relations
argument. We conclude by showing that they are also sound with respect to the equational theory.

§.§ $\omega$-quasi Borel spaces

A significant limitation, for the purposes of semantics, of the traditional category of measurable spaces and measurable functions $\cat{Meas}$
is that it is not Cartesian closed, meaning that it cannot interpret higher-order functions.

This led to an arduous search for a Cartesian closed category that conservatively extends $\cat{Meas}$, resulting in the definition of quasi
Borel spaces <cit.>. Though this category is very interesting in its own right, it is not fully adequate as a semantic basis for probabilistic programming
languages, since it cannot handle unbounded recursion. This limitation has led to the discovery of $\omega$-quasi Borel spaces, which we now define.

An $\omega$-quasi Borel space is a triple $(X, \leq, M_X)$ such that, $(X, \leq)$ is a $\omega$-complete partial order ($\omega$CPO),
i.e. it is a partial order closed under suprema of ascending sequences, and $M_X \subseteq \R \to X$
is the set of random elements with the following properties:

* All constant functions are in $M_X$

* If $f : \R \to \R$ is a measurable function and $p \in M_X$, then $p \circ f \in M_X$

* If $\R = \bigcup_{n\in \nat} U_n$, where for every $n$, $U_n$ are pairwise-disjoint
and Borel-measurable, and $\alpha_n \in M_X$ then the function $\alpha(x) = \alpha_n(x)$
if, and only if, $x \in U_n$ is also an element of $M_X$.

* For every ascending chain $\{f_n\}_n \subseteq M_X$, i.e. for every $x \in \R$, $f_n(x) \leq f_{n+1}(x)$,
the pointwise supremum $\bigsqcup_n f_n $ is in $M_X$.

Note that, in the definition above, $\omega$CPOs do not assume the existence of a least element, e.g. for every set $X$,
the discrete poset $(X, =)$ is an $\omega$CPO.

A measurable function between $\omega$-quasi Borel spaces is a Scott continuous function $f : X \to Y$  — i.e. preserves
suprema of ascending chains — such that for every $p \in M_X$, $f \circ p \in M_Y$.

The category $\wqbs$ has $\omega$-quasi Borel spaces as objects and measurable functions as morphisms.

The category $\wqbs$ is Cartesian closed.

Furthermore, there is a full and faithful functor $\cat{Meas} \to \wqbs$. More concretely, if
you interpret a program that has as inputs and output measurable spaces,
its denotation in $\wqbs$ will be a measurable function, even if the program uses higher-order functions,
and any measurable function could potentially be the denotation of the program.

Inductive types
As shown in previous work <cit.>, $\wqbs$ can also soundly accommodate full recursive types.
In particular, it can give semantics to lists over $A$ by solving the domain equation
$\listty A \cong 1 + A \times \listty A$.

It is convenient that in $\wqbs$ the set of lists over $A$
with appropriate random elements and partial order is a solution to the domain equation and it is the smallest one, i.e. it is an initial algebra.
This means that when reasoning about lists expressed in $\meta$, you may assume that they are just the set of lists over sets.

Probability and Partiality Monads
It is possible to construct probabilistic powerdomains in $\wqbs$, making it possible to use this category as a semantic
basis for languages with probabilistic primitives. Furthermore, the $\omega$CPO structure can also be used
to construct a partiality monad, making it possible to give semantics to programs with unbounded recursion

Let $\cat{C}$ be a category, a monad is a triple $(T, \eta^T, (-)^{\#}_T)$ where $T:\cat{C} \to \cat{C}$ is an endofunctor,
$\eta^T : id \to T$ and $(-)^\#_T : \cat{C}(-, T =) \to \cat{C}(T -, T =)$ are natural transformations such that

\begin{align*}
f^\#_T\circ \eta &= f\\
\eta^\#_T &= id\\
(f^\#_T \circ g)^\#_T &= f^\#_T \circ g^\#_T
\end{align*}

The monad is said to be strong if there is a natural transformation $st_{A,B} : A \times T B \to T(A\times B)$
making certain diagrams commute <cit.>. When it is clear from the context, we will simply write $\eta$ and $(-)^\#$,
without the sub and superscript, respectively.

The category $\wqbs$ admits strong commutative monads $P$ and $\Psub$ of probability and sub-probability distributions, respectively.

At the categorical level, $\Psub$ is defined as a submonad of the continuation monad $( - \to [0, \infty]) \to [0, \infty]$ and
its monad structure is similar to the one from probability monads in $\cat{Meas}$, i.e. the unit at a point $a : A$ is given
by the point mass distribution $\delta_a$ and $f^\#(\mu)$ is given by integrating $f$ over the input distribution $\mu$.

Furthermore, by construction, $\wqbs$ admits a morphism $\int_A : (\Psub A) \times (A \to \{0,1\}) \to [0,1]$
that maps a subprobability distribution and a “measurable set” of $A$ into its measure. For example, if $A$ is a measurable
space, for every measurable set $X : A \to \{0,1\}$, and for every subprobability distribution $\mu : \Psub A$, the map $(\mu, X) \mapsto \mu(X)$
is an $\wqbs$ morphism and is equal to $\int_A$.

As we have mentioned above, it is also possible to define a lifting monad in $\wqbs$ that adds a least element $\bot$ to a space, making them
pointed $\omega$CPOs. This monad, combined with the $\omega$CPO strucure, is used to guarantee the existence of fixed points of
endomorphisms between pointed $\omega$CPOs.

The lifting monad in $\wqbs$ $X_\bot$ adds a fresh element $\bot$ to $X$, makes it the least element and the random elements $M_{X_\bot}$
are the functions $f : \R \to X_\bot$ such that there is a Borel measurable set $\mathcal B$ and a map $\alpha : \R \to X$ in $M_X$
such that $f(x) = \alpha (x)$ for $x \in \mathcal B$ and $\bot$ otherwise.

The machinery we have defined so far is expressive enough to interpret $\meta$, with exception of
its cost operations. In non-effectful languages, the writer monad $(\cmon \times -)$ can be used to give
semantics to cost operations such as $\charge c$.

If $(\cmon, 0, +)$ is a monoid, then $\cmon \times -$ is a monad — the writer monad — where the unit at a point $a$ is $(0, a)$
and given a morphism $f : A \to \cmon \times B$, $f^\#(c, a) = (c + (\pi_1 \circ f)(a), (\pi_2 \circ f)(a))$.

What follows is how to combine the non-probabilistic cost monad $(\cmon \times -)$ with
$\Psub$ in order to define a probabilistic cost semantics.

§.§ A probabilistic cost semantics

As opposed to the deterministic case, the cost of a probabilistic computation is not a single value; instead, it
is a distribution over the costs. For instance, consider the program:

\[\cdot \vdashcomp (\charge 1; \produce 0) \oplus (\produce 2) : F \nat\]

it either returns $2$ without costing anything, or it returns $0$ with a cost of $1$. Denotationally, this program should
be the distribution $\frac 1 2 (\delta_{(1,0)} + \delta_{(0, 2)})$. With equal probability, the program will either
cost $1$ and output $0$ or cost $0$ and output $2$.

In the deterministic case, it is possible to encode the cost at the semantic-level by using the writer monad $\cmon \times -$.
For probabilistic cost-analysis we can use the writer monad transformer.

If $T : \cat{C} \to \cat{C}$ is a strong monad then $T(\cmon \times -)$ is a strong monad.

The strength of a monad is a natural transformation $A \times T B \to T(A \times B)$. When
instantiating $A$ to be $\cmon$, we can conclude that there is a distributive law between
the writer monad and $T$, which allows us to conclude that $T(\cmon \times -)$ is a monad.
Its strength is defined as
$st^T;T (st^{\cmon \times -}) : A \times T(\cmon \times B) \to T( A \times (\cmon \times B)) \to T(\cmon \times (A \times B))$.

When instantiating $T$ to be the subprobability monad $P_{\leq 1}$, we get a monad for probabilistic cost,
which justifies the denotation of the program $(\charge 1; \produce 0) \oplus (\produce 2)$ being
a distribution of a pair of a cost and natural number.

By using the monadic semantics of CBPV, we get a cost-aware probabilistic semantics, where
most of its definitions follow the standard monadic CBPV semantics shown in <Ref> — denoted
as $\semcs{\cdot}^v$ for values and $\semcs{\cdot}^c$ for computations. The noteworthy interpretations are for the one for the cost monoid,
which is interpreted as $\nat$, and for the
effectful operations, whose semantics are depicted in <Ref>.

c = δ_(c, ())
V = ∑_i = 0^V 1/Vδ_(0,i)
x.  t = _n t^n()

Cost semantics of operations

With this semantics we now define the expected cost of a distribution:

Let $\mu : \Psub [0,\infty]$, its expected value is $\mathbb{E}(\mu) = \int_{[0,\infty]} x \diff\mu$.

In the definition above we have chosen the most general domain for $\mathbb{E}$, but for every subset
$X\subseteq[0,\infty]$ the expected distribution formula can be restricted to distributions over $X$.

[Geometric Distribution]
This semantics makes it possible to reason about the geometric distribution defined as the program [For the sake of simplicity we have elided the some of the bureacracy of CBPV, such as $\produce$ and $\force$.]
$\cdot \vdash \fix x. 0 \oplus (1 + x) : F \nat$. It is possible to show that this program indeed denotes
the geometric distribution by unfolding the semantics and obtaining the fixed point equation
$\mu =  \frac{1}{2}(\delta_0 + P_{\leq 1}(\lambda x. 1 + x)(\mu))$, for which the geometric distribution
is a solution.

Since we are interested in reasoning about the cost of programs, it is possible to reason about the
expected amount of coins flipped during its execution by adding the $\charge 1$ operation as follows
$\fix x.\, \mathsf{charge}_1; (0 \oplus (1 + x)) : F \nat$, i.e. whenever a new coin is flipped, as modeled
by the $\oplus$ operation, the cost increases by one. By construction, the cost distribution will also
follow a geometric distribution.

If we want to compute the actual expected value we must compute
$\sum_{n:\nat} \frac{n}{2^{n}}$. This particular infinite sum can be calculated by using a standard trick.
As we will in the next section, it is possible to encode this trick in the semantics itself, which
simplifies significantly computing the expected value.

Expected cost and non-termination
When designing metalanguages for reasoning about cost of programs, it is expected that the cost
of a non-terminating computation is infinite. Therefore, since subprobability distributions
of mass less than $1$ model possibly non-terminating computation, their cost should be $
\infty$, This can be achieved this by modifying the expected
cost function to $\infty \cdot (1 - \mu(\cmon)) + \int_\cmon x \diff \mu$ and defining
$\infty \cdot 0 = 0$, meaning that every computation with non-zero chance of termination would,
by definition, have infinite expected cost.

There are a few problems with this solution. Since the soundness proof of <Ref>
requires the expected cost to be a morphism $\Psub(\cmon) \to [0, \infty]$ in $\wqbs$, we have to equip
the extended positive real line with a set of random elements and a partial order.
Traditionally, the bottom element of $[0,\infty]$ would
be interpreted as $\infty$, in line with the slogan that “no information” equals
infinite cost — this is the approach taken by <cit.>. However, as we will see in
<Ref>, when we have recursively defined programs of type $F \tau$, their expected
costs are given by the supremum of increasing sequences of real numbers, starting from $0$. Suggesting
that $0$ needs to be the bottom element while $\infty$ is the top element.

This alternative is also problematic, unfortunately, since it is not Scott-continuous. As an example
consider the geometric distribution, where its cost distribution is given by the supremum of
the sequence $\{\sum_i^n 2^{-i}\delta_i\}_n$. Therefore, $\mathbb E(\sum_i^n 2^{-i}\delta_i) = \infty$,
for every $n \in \nat$, resulting in

\[\sup_n \mathbb E\left ( \sum_{i = 1}^n 2^{-i}\delta_i\right ) = \infty \neq \mathbb E \left ( \sup_n \sum_{i = 1}^n 2^{-i}\delta_i\right ) = \mathbb E(\mathsf{geom}) = 2,\]

Where $\mathsf{geom}$ is the geometric distribution. Other approaches have not dealt with
these difficulties because, unlike other effects, probabilities present genuinely
interesting recursive programs of type $F \nat$, as illustrated by the geometric distribution itself.
In contrast, in <cit.>, by a monotonicity argument, every recursive program of type $F\nat$ either
diverges or outputs a constant. Therefore, assigning infinite cost to these programs, though not very realistic
from a modeling point of view, is not too damaging to the semantics.

With this in mind we argue that <Ref> is a sensible choice. In <Ref>, we
go over the consequences of this definition insofar as the cost semantics interacts with the expected cost semantics.

§.§ A semantics for expected-cost

The semantics defined in the previous section can be used to compositionally compute the cost
distribution for computations of type $F \tau$. In turn, by using <Ref>,
its expected cost can be calculated.

Though the approach above is sound, it is not compositional. Indeed, after computing
the distribution, we must compute the expected cost of an arbitrarily complex distribution. Instead,
if we could compute the expected cost as we compute the semantics, we would avoid this lack
of compositionality altogether.

We achieve this by making the expected value a part of the semantics by
constructing a new monad that keeps track of the average cost. More concretely, computations
of type $F\tau$ will denote a pair of an extended positive real number and a subprobability distribution.
Intuitively, a computation will output its expected cost and the output subprobability distribution.
We can show that this pair can be equipped with a monad structure, where the functorial action on morphisms
is $f \mapsto id_{[0,\infty]} \times \Psub f$, the unit at a point $a : A$
is the pair $(0, \delta_a)$ and the bind operation $(-)^\#$ adds the expected cost of the input
with the average of the expected cost of the output, given the input distribution. Formally,
given an $\wqbs$ morphism $f : X \to [0,\infty] \times \Psub Y$, its bind is the function
$f^\#(r, \mu) = (r + \int (\pi_1 \circ f) \diff \mu, (\pi_2\circ f)^\#_{\Psub}(\mu))$.

The triple $([0,\infty] \times \Psub, \eta, (-)^\#)$ is a strong monad.

Since $\Psub$ is a monad, and the second component of the monad operations of $[0,\infty] \times \Psub -$
are identical to the ones of $\Psub$, we only need to prove the monad laws for the first component.
The unit laws follow from:

\begin{align*}
&\pi_1(\eta^\#(r ,\mu)) = r + 0 = r\\
&\pi_1((f^\# \circ \eta)(x)) = \pi_1(f^\#(0, \delta_x)) = 0 + \pi_1(f(x))
\end{align*}

While the last law requires a bit more work:

\begin{align*}
&\pi_1((f^\# \circ g^\#)(r, \mu)) =\\
&\pi_1(f^\#(r + \int (\pi_1 \circ g)\diff\mu, (\pi_2 \circ g)^\#_{\Psub}(\mu))) = \\
&r + \int (\pi_1 \circ g)\diff\mu + \int (\pi_1 \circ f) \diff((\pi_2 \circ g)^\#_{\Psub}(\mu)) =\\
&\pi_1((f^\# \circ g)^\#(r, \mu))
\end{align*}

The last equation follows from the monad laws of $\Psub$.

With this monad it is possible to define a new semantics to $\meta$ that interprets
the effectful operations a bit differently from the cost semantics, as we depict in
<Ref>, where $\semec{\cdot}^c$ is the computation semantics while $\semcs{\cdot}^v$ is
the value semantics; the cost monoid is still interpreted as $\nat$.

[Revisiting the geometric distribution]
Now that we have this new semantics, we can revisit a slightly generalized variant of the geometric distribution
example where the fair coin $\oplus$ is replaced by its biased version $\oplus_p$, for $p \in [0,1]$.

By unfolding the semantics we obtain the fixed point equation
$E = 1 + (1 - p) E$, i.e. $E = \frac{1}{p}$.
Note that if $p = 0$ the equation above does not have a solution. Concretely, in this case
the program would never terminate.

As we have noted in the previous section,
the cost semantics can be used to reason about the expected cost by using <Ref>.
Something which will play an important role in our soundness proof is the fact that this
definition interacts well with the monadic structure of $\Psub$.

c = (c, δ_())
V = (0, ∑_i = 0^Vδ_i/V + 1)
x.  t = _n t^n()

Expected cost semantics of operations

Let $\mu : \Psub A$ and $f : A \to \Psub ([0,\infty])$, $\mathbb E(f^\#(\mu)) = \int_A \mathbb E(f(a))\mu(\diff a)$.

This can be proved by unfolding the definitions

\begin{align*}
&E(f^\#(\mu)) = \int_{[0,\infty]} x f^\#(\mu)(\diff x) = \int_{[0,\infty]} x \left ( \int_A f(a) \mu(\diff a)\right ) (\diff x) = \\
&\int_A \int_{[0,\infty]} x f(a)(\diff x)\mu(\diff a) = \int_A \mathbb E (f(a))\mu(\diff a)
\end{align*}

Note that in the third equation we had to reorder the integrals, which is valid
because $\Psub$ is commutative.

With this lemma in mind, we may state some basic definitions that allows us to describe
precisely how the cost and expected cost semantics relate.

A monad morphism is a natural transformation $\gamma : T \to S$, where $(T, \eta^T, (-)^\#_T)$
and $(S, \eta^S, (-)^\#_S)$ are monads over the same category, such that

\begin{align*}
&\gamma \circ \eta^T = \eta^S\\
&(\gamma \circ g)^\#_S \circ \gamma= \gamma \circ g^\#_T, \text{ for every $g: A \to T B$}
\end{align*}

There is a monad morphism $E : P(\nat \times -) \to [0,\infty] \times P$.

We define the morphism

\[E_A(\mu) = (\mathbb{E}(P(\pi_1)(\mu)), P(\pi_2)(\mu))\]

The first monad morphism equation follows by inspection and the second one follows mainly from <Ref>,
when restricting it to the probabilistic distributions, i.e. total mass equal to $1$.

The natural transformation $E$, when extend to subprobability distributions, is not a monad morphism.

Let $\frac 1 2 (\delta_{(0,1)} + \delta_{(1, 2)})$
be a distribution over $\cmon \times \nat$ and $f(0) = \frac 1 2 \delta_0$, $f(n+1) = 0$ be a subprobability
kernel. It follows by inspection that $((E \circ f)^\#_{[0,\infty] \times \Psub} \circ E) (\mu) \neq (E \circ f^\#_{\Psub(\nat \times -)})(\mu)$

<Ref> says that the different cost semantics interact
well in the probabilistic case. In the subprobabilistic case this is not
true, as illustrated by <Ref>. This formalizes the intuitions
behind the subtleties in the interaction of expected cost and non-termination
explained in the previous section.

§.§ Soundness Theorems

We have three ways for reasoning about expected cost: by using the equational theory or by using either of
the denotational semantics. Now, we want to understand how they relate to one
another. When we restrict the language and semantics to the probabilistic case, i.e. without unbounded
recursion, we can prove strong guarantees about the different semantics. For instance, the expected cost
semantics gives the same value as the expected cost of the cost distribution in the cost semantics. Furthermore,
both of these semantics satisfy the same equations.

Unfortunately, in the presence of unbounded recursion,
i.e. subprobability distributions, the two semantics are not “the same” anymore. What we show in this section
is that in the presence of subprobability distributions, the expected cost semantics is an upper bound on the
expected cost of the cost distribution. Furthermore, even though both of these semantics validate the base equational theory,
many useful extensions are not sound in the cost semantics and some unusual equations do hold in it, as we explain
in Section <ref>. This leads us to believe that the expected cost semantics provides the right level of
abstraction for reasoning about the cost of recursive probabilistic programs.

§.§.§ Denotational Soundness

Denotational Soundness: Probabilistic Case
As we have seen, by using <Ref> it is possible to compositionally
reason about the expected cost of running programs. The problem is that it is unclear
if this new semantics agrees with the cost semantics or if it is reasoning about
a different property altogether. In this section we will restrict the monad to its
total submonad of probability distributions, i.e. use the monads $P(\cmon \times -)$
and $ [0,\infty ] \times P$ and remove the recursion operation.

In order to solve this problem we must show that the expected cost semantics is sound
with respect to the cost semantics. Intuitively, we want to show that if we have
a program $\vdashcomp t : F \nat$, then its
denotations under both $\semcs{ \cdot }$ and $\semec{\cdot}$ agree in the sense that
the expected value for the second marginal
of $\semcs{t}$ is equal to $\pi_1(\semec{t})$, and the distribution of
the second marginal of $\semcs{t}$ is equal to $\pi_2(\semec{t})$.

In the literature, this property has been called the effect simulation problem
and many semantic techniques have been developed for solving it <cit.>.
One of the most general ones uses a construction called $\top\top $-lifting <cit.>,
which consists of extending ideas from the categorical logical relations literature to the monadic

A simplified version of the main theorem in <cit.> is the following:

Let $\cat{C}$ be a category, $T : \cat C \to \cat C$ and $S : \cat C \to \cat C$ be monads
such that there is a monad morphism $\gamma : T \to S$, then for every program $\cdot \vdashcomp t : F \nat$,
$\gamma_\nat(\semcs {t}^c) = \semec{t}^c$.

We can see how this theorem is relevant to what we want to prove: there are two monads $P(\cmon \times -)$
and $[0,\infty] \times P$, a monad morphism between them and we want to prove that their output distributions are the same
and the expected cost of both semantics are equal — precisely how the monad morphism $E$ is defined.

The problem with the theorem above is that, even in its most general form proved by <cit.>, it can
only handle base types and it gives no guarantees for programs of type, say $\listty \nat \to F(\listty \nat)$, which
is a significant limitation to the case studies we study in <Ref>.

We circumvent these issues by defining a two-level version of the
$\top\top$-lifting construction that works for our particular case, though we do not have a general
categorical construction yet. Concretely, we construct a two-level logical relations argument,
mimicking the two-level structure present in CBPV. At the base of our argument is the
relational-lifting construction, defined as follows:

Let $\mathcal{R} \subseteq A \times B$ be a complete binary relation, i.e. it is closed under suprema of
ascending sequences, its lifting
$\mathcal{R}^{\#} \subseteq \Psub(A) \times \Psub(B)$ is defined as $\mu\, \mathcal{R}^\#\, \nu$
if there is a distribution $\theta : \Psub(\mathcal R)$ such that its first and second
marginals are, respectively, $\mu$ and $\nu$.

This definition interacts well with the monadic structure of $\Psub$. Concretely, it is stable
with respect to the unit and bind of $\Psub$. The same definition can be restricted to $P$.
We can now define two families of relations, one for value types and one for computation types:

\begin{align*}
&\V_\tau \subseteq \semcs{\tau}^v \times \semec{\tau}^v \\
&\V_\nat = \set{(n,n)}{n\in\nat}\\
&\V_{U\overline{\tau}} = \C_{\overline{\tau}}
\\
\\
&\C_{\overline\tau} \subseteq \semcs{\overline\tau}^c \times \semec{\overline\tau}^c \\
&\C_{F \tau} = \set{((r, \nu), \mu)}{\mathbb E(\mu_1) = r \land \nu \V^\#_\tau \mu_2}\\
&\C_{\tau \to \overline{\tau}} = \set{(f_1, f_2)}{\forall x_1, x_2, x_1 \V_\tau x_2 \Rightarrow f_1(x_1) \C_{\overline{\tau}} f_2(x_2)}
\end{align*}

We can prove by induction the following lemma:

For every $\tau$ (resp. $\overline{\tau})$, the relation $\VRel_\tau$ (resp. $\CRel_{\overline\tau}$) is an $\omega$CPO,
where the partial order structure is the same as the one from $\semcs{\tau}^v \times \semec{\tau}^v$
(resp. $\semcs{\overline\tau}^c \times \semec{\overline\tau}^c$). Furthermore, the computation relations have
a least element.

For every type $\tau$ (resp. $\overline \tau$), there is a set $M$ and partial order $\leq$ such that the triple $(\VRel_\tau, M, \leq)$ (resp. $(\CRel_{\overline\tau}, M, \leq)$)
is an $\omega$-quasi Borel space with the such that the injection function is a morphism in $\wqbs$.

We only make explicit the proof for value types, since the case of computation types is basically the same.
We define the order $\leq$ to be the same as the one in $\semcs{\tau}^v \times \semec{\tau}^v$ and $M$ to be
the restricted random elements $\{f \in M_{\tau_1} \smid f(\R) \subseteq \VRel_\tau\}$.

Since by the lemma above the logical relations are $\omega$CPOs, $M$ is closed under suprema of ascending chains.
and $(\VRel_\tau, M, \leq)$ is an $\omega$-quasi Borel space. The injection into $\semcs{\tau}^v \times \semec{\tau}^v$
being a morphism follows by construction.

We can now state the denotational soundness theorem:

For every $\Gamma = x_1 : \tau_1, \dots, x_n : \tau_n$, $\Gamma \vdashval V : \tau$, $\Gamma \vdashcomp t : \overline\tau$ and if for every $1 \leq i \leq n$, $\cdot \vdashval V_i : \tau_i$ and $\semcs{V_i} \VRel_{\tau_i} \semec{V_i}$, then

\begin{align*}
&\semcs{\letin {\overline{x_i}} {\overline{V_i}} t} \CRel_{\overline \tau}^c \semec{\letin {\overline{x_i}} {\overline{V_i}} t}^c \text{ and }\\
&\semcs{\letin {\overline{x_i}} {\overline{V_i}} V}^v \VRel_\tau \semec{\letin {\overline{x_i}} {\overline{V_i}} V}^v,
\end{align*}

where the notation $\overline{x_i} = \overline{V_i}$ means a list of $n$ let-bindings or, in the case of values,
a list of substitutions.

The proof follows by induction and is shown in <Ref>.

We now have a very precise sense in which the expected-cost semantics is related to the cost semantics:

The expected-cost semantics is sound with respect to the cost semantics, i.e. for every program
$\cdot \vdash_c t : F\tau$, the expected cost of the second marginal of $\semcs{t}^c$ is equal to

That being said, the theorem above is only valid for probability distributions. The key lemma in
<Ref> relies on the fact that the total mass of distributions is always $1$.

Denotational Soundness: Subprobabilistic Case

Though both cost semantics are “equivalent” in the sense explained above, programming without recursion
is somewhat limiting when it comes to probabilities. Indeed, without an infinitely supported base distribution,
every definable distribution has finite support. In particular, it would not be possible to define the
geometric distribution.

Therefore, it seems reasonable to prove the soundness theorem above for $\Psub$. Unfortunately, it does not hold in
the subprobabilistic case, as alluded by <Ref>.

Consider the programs

\begin{align*}
t &= \charge 2; \produce 0\\
u &= \lamb x {\ifthenelse x {(\bot \oplus (\charge 4; \produce 0))} {\bot}}
\end{align*}

We can show

\[
\semcs{x \leftarrow t; \app u x}^c = (3, \frac 1 2 \delta_0) \neq (4, \frac 1 2 \delta_0) = \semec{x \leftarrow t; \app u x}^c
\]

The counter-example above leaves us in a predicament: which semantics is the “true” semantics? We
argue that the expected cost semantics is better suited for reasoning about programs. Consider
the program $\charge c; \bot$. From a programming point of view, the programs charges $c$ units of
costs and then loops forever. The cost semantics of the program above will be the zero distribution over $\cmon$ and
the terminal object $1$. Therefore,
using <Ref>, its cost is $0$. The expected cost semantics, however, gives a much more sensible
semantics, it is the pair $(c, 0)$, where $0$ is the zero distribution over $1$.

That being said, these two semantics are not completely unrelated and we can still prove a weaker version
of <Ref>. This is achieved by defining basically the same logical relations as before, with the
exception of $\CRel_{F\tau}$, which now becomes

\[\CRel_{F \tau} = \set{((r, \nu), \mu)}{\mathbb E(\mu_1) \leq r \land \nu \V^\#_\tau \mu_2}\]

The expected-cost semantics is sound with respect to the cost semantics, i.e. for every program
$\cdot \vdash_c t : F\tau$, the expected cost of the second marginal of $\semcs{t}^c$ is at most

The proof can also be found in <Ref>.

§.§.§ Equational Soundness

The last section has argued that in the presence of unbounded recursion, the cost semantics validates some
unrealistic equations that are not validated by the expected cost semantics.
That being said, when it comes to the base equational theory of <Ref>,
both semantics are sound with respect to it.

If $\Gamma \vdashcomp t = u : \overline{\tau}$ then $\semec{t}^c = \semec{u}^c$ and $\semcs{t}^c = \semcs{u}^c$.

The proof follows by induction on the equality rules, where the inductive cases follow directly from the inductive hypothesis
while the base cases follow by inspection. For instance, the equation $\charge 0; t = t$ is true because $\nat$ is a monoid
and $0$ is its unit.

It is interesting to understand to what extent these equational theories differ.
For instance, the cost semantics validates the equation $\bot; t = \bot = t; \bot$. As we have argued before,
this equation is too extreme for the purposes of expected cost, since it says that $\charge c; \bot = \bot$.
An even more egregious equation that it satisfies is $\fix x.\, \charge 1; x = \bot$. That equation says that
the cost of infinity is the same as no cost at all, as long as the program does not terminate.

These equations are connected to the commutativity equation:

\[
\inferrule{\Gamma \vdashcomp x : F \tau_1 \\ \Gamma \vdashcomp u : F \tau_2 \\ \Gamma, x : \tau_1, y : \tau_2 \vdashcomp t' : \overline\tau}{\Gamma \vdashcomp (x \leftarrow t; y \leftarrow u; t')  = (y \leftarrow u; x \leftarrow t; t') : \overline{\tau}}
\]

The cost semantics validates the commutativity equation.

The proof follows basically by commutativity of $\Psub$:

\begin{align*}
& \semcs{x \leftarrow t; y \leftarrow u; t'} = \\
&\int_{\nat \times A} \int_{\nat \times B} \Psub(f)(\semcs{t'}(a, b)) \semcs u(\diff n_1 \diff a)\semcs t(\diff n_2 \diff b) = \\
&\int_{\nat \times B} \int_{\nat \times A} \Psub(f)(\semcs{t'}(a, b)) \semcs t(\diff n_2 \diff b)\semcs u(\diff n_1 \diff a) = \\
& \semcs{y \leftarrow u; x \leftarrow t; t'}, \text{ where $f(n, c) = (n + n_1 + n_2, c)$}
\tag*{\qedhere}
\end{align*}

This equation is usually useful for reasoning about probabilistic programs. However, it is too strong for the purposes
of reasoning about expected cost. Indeed, consider the programs

\begin{align*}
&t = \bot; \charge c; \produce ()\\
&u =\charge c; \bot; \produce ()
\end{align*}

From an operational point of view, the first program will run a non-terminating program and never reach the $\charge c$ operation,
while the second one starts by increasing the cost by $c$ and then loops forever — closer to how cost works in the real world, e.g.
if the charge operation is modeling a monetary cost, such as a call to an API, only the second program will cost something.

The monad $[0, \infty] \times \Psub$ is not commutative.

The two terms above are a counter example when $c > 0$:

\begin{align*}\semec t = (0,0) \neq (c, 0) = \semec u
\tag*{\qedhere}
\end{align*}

Inequational theory

In the context of cost analysis, it can also be useful to reason about upper/lower bounds on the cost. The different versions
of geometric distributions have already demonstrated this. Though reasoning semantically about these bounds is immediate,
this is not the case at the syntactic level. One way of addressing this is by defining inequational theories where
you can reason about programs being less than or equal to other programs.

For the expected cost, however, one must be careful in terms of which rules to include. While the rule $\charge c \leq \charge d$,
whenever $c \leq d$ is reasonable whenever the cost monoid comes equipped with a partial order, in the presence of probability
it is not so easy to syntactically reason about these properties. A simple non-trivial example would be comparing the two variants of

Since in this work we were mainly interested on the denotational aspects of expected cost, we leave a more thorough investigation
of the inequational properties of expected cost to future work.

§ EXAMPLES

In this section we will show how the expected cost semantics can be used to reason about the expected cost of probabilistic programs.
We present four examples, two randomized algorithms and two recursive stochastic processes, illustrating the versability
of $\meta$.

§.§ Expected coin tosses

A classic problem in basic probability theory is computing the expected number of coin flips necessary in order to
obtain $n$ heads in a row. We can model this stochastic process as the following recursive probabilistic program:

\begin{align*}
&\mu f : \nat \to F 1.\, \lambda n : \nat.\,\\
&\mathsf{if} \, n \, \mathsf{then}\\
&\quad \produce ()\\
& \mathsf{else}\\
&\quad \app {(\force f)} {(n-1)};\\
&\quad\charge 1; \\
&\quad (\produce () \oplus \app {(\force f)} n)
\end{align*}

For every $n$, the program above simulates the probabilistic structure of flipping coins until obtaining $n$ heads
in a row.
When its input is $0$, it outputs $()$ without flipping any coins. If the input is greater than $0$, in
order to flip $n$ heads in a row it must first flip $n - 1$ heads in a row — hence the call to $f (n - 1)$ —
flip a new coin while increasing the current counter by $1$ and, if it is heads, you have obtained $n$ heads in a
row and may output $()$, otherwise you must recursively start the process again from $n$: the left and
right branches of $\oplus$, respectively.

By unfolding the semantics, we obtain that the expected number of coin tosses is given by the following recurrence relation:

\begin{align*}
T(0) &= 0\\
T(n+1) &= 1 + T(n) + \frac{1}{2}T(n + 1)
\end{align*}

Which has the closed-form solution $T(n) = 2(2^n - 1)$.

§.§ Randomized Quicksort

Quicksort is one of the main sorting algorithms and, as the name suggests, it is very fast.
The problem with it is that it has an obvious worst-case scenario: if the input list is in
reverse order, quicksort requires $O(n^2)$ comparisons. However, if you randomly choose
an element of the list as your pivot, you can prove that it only requires $O(n\log(n))$ comparisons.

In <Ref> we present a program that implements the randomized algorithm. If we
simply interpret the expected cost of this program denotationally, it will be a function mapping
lists to real numbers. This is not how such an analysis is done in practice,
where people reason about how the cost increases as the length of the list increases, regardless of
which elements it contains.

\begin{align*}
&\mu f : \nat \to F \nat.\, \lambda n : \nat.\,\\
&\mathsf{if} \, n \, \mathsf{then}\\
&\quad \produce 0\\
& \mathsf{else}\\
&\quad \charge {n - 1}; \\
&\quad x \leftarrow \rand \, n;\\
&\quad (\force \, f)\, x;\\
&\quad (\force \, f)\, (n - x);\\
&\quad \produce n
\end{align*}

Quicksort over natural numbers

In our semantics, the denotation of the program is hiding the fact that its cost only depends on
the length of its argument. We make this precise by defining a measurable function using the program in <ref>
$qck_\nat : \nat \to \R \times \Psub \nat$ that corresponds to the quicksort structure
assuming that the input is a natural number. Let $len : \listty \nat \to \nat$ be the function that
outputs the length of its input.

The following diagram commutes:

\[\begin{tikzcd}
{\listty \nat} & \nat \\
{F \listty \nat} & {F \nat}
\arrow["{qck_{\listty \nat}}"', from=1-1, to=2-1]
\arrow["len", from=1-1, to=1-2]
\arrow["{qck_{\nat}}", from=1-2, to=2-2]
\arrow["{F(len)}"', from=2-1, to=2-2]
\end{tikzcd}\]

This can be proved by strong induction on the length of the input list.
If the list is empty, then its length is $0$ and the diagram commutes.
If, however, the list not not empty, there will be a bijection between
the recursive calls to lists of size $n'$ to sampling $n'$ in $qck_\nat$.
By using the strong inductive hypothesis to these lists of size $n'$,
we can conclude.

We can now conclude our analysis, since by the soundness theorem and the commutative diagram above,
the expected cost of $\mathsf{quickSort}$ is given by $\pi_1 \circ qck_\nat \circ len$.
Since the expression $\pi_1 \circ qck_\nat$ satisfies the recursive definition:

\begin{align*}
T(0) &= 0\\
T(n) &= n - 1 + \frac{2}{n}\sum_{i = 0}^{i-1}T(i)
\end{align*}

This allows us to conclude that $\mathsf{quickSort}$ has an expected cost of $O(n \log (n))$.

§.§ Quickselect

Consider the Quickselect problem, which receives as input an unordered list $l$ and a natural number $n$
and outputs the the $n$-th largest element of $l$. This algorithm is very similar to quicksort:
you choose a pivot, split the list into elements larger and smaller than it, then recurse on the
appropriate list.

\begin{align*}
&\mu f : \listty \nat \to \nat \to F (\nat) .\,\\
&\lambda l : \listty \nat.\,\\
&\lambda n : \nat.\,\\
&\mathsf{case} \, l \, \mathsf{of}\\
& \mid \mathsf{nil} \Rightarrow \\
& \quad \produce \mathsf{nil}\\
&\mid \mathsf{(hd, tl)} \Rightarrow \\
& \quad len \leftarrow \app \mathsf{length}\, l\\
& \quad r \leftarrow \app \rand len\\
& \quad pivot \leftarrow len[r]\\
& \quad (l_1, l_2) \leftarrow \app {\app{biFilter} {(\lamb n {\charge 1; n \leq pivot})}} l\\
& \quad lgth \leftarrow \mathsf{len} \, l_1\\
& \quad \mathsf{if} \, lgth< n - 1\, \mathsf{then}\\
& \quad \quad (\force f)\, l_1\, n\\
& \quad \mathsf{elseif} \, lgth == n - 1\, \mathsf{then}\\
& \quad \quad \produce pivot\\
& \quad \mathsf{else}\\
& \quad \quad (\force f)\, l_2\, (n - lgth)\\
\end{align*}

In the best case, this algorithm runs in linear time and in the worst case, quadratic time.
If we choose the pivot uniformly random, we get linear time, which is given by the following
recurrence relation.

\begin{align*}
T(0) &= 0\\
T(n) &= n - 1 + \frac 1 n \sum_i T(i)
\end{align*}

§.§ Random Walks

Random walks are classic examples of probabilistic processes. For this example we are interested in
the symmetric random walk over the natural numbers. At every point $n$ the probability of moving to
$n-1$ or $n+1$ is $\frac{1}{2}$. Furthermore, we are assuming the variant where at $0$
you move to $1$ with probability $1$. We can write a program that simulates such a random walk
with a point of departure $i : \nat$ and a point of arrival $j : \nat$:

\begin{align*}
&\mathsf{randomWalk} = \mu f : \nat \to \nat \to F 1.\, \lambda i : \nat \, j : \nat.\\
&\mathsf{if} \, i = j \, \mathsf{then}\\
&  \quad \produce ()\\
& \mathsf{else}\\
&\quad \charge 1;\\
&\quad\mathsf{if} \, i \, \mathsf{then}\\
& \quad \quad (\force f) \, 1 \, j\\
&\quad \mathsf{else}\\
&\quad \quad ((\force f) \, (i-1) \, j) \oplus ((\force f) \, (i+1) \, j)
\end{align*}

The program receives the starting and end points, $i$ and $j$, respectively, as arguments,
and if they are equal, you stop the random walk. Otherwise, you take one step
of the random walk, i.e. you take step to either $i - 1$ or $i + 1$ with equal probability,
with the  exception of when $i = 0$, in which case you go to $1$. This iterative behaviour
can be straightforwardly captured with recursion, as illustrated by the program above.

It is now possible to compute the expected value on the number of rounds that are necessary in order
to reach your target. This is given by the following two-argument recursive relation.

\begin{align*}
T(i, i) &= 0\\
T(0, j) &= 1 + T(1, j)\\
T(i, j) &= 1 + \frac{1}{2} (T (i-1, j) + T(i + 1, j))
\end{align*}

This recurrence relation is well-known in the theory of Markov chains — see <cit.> for an introduction.
Something interesting about it is that when $i > j$, this stochastic process reduces to the symmetric random walk
without an absorbing state, which is known to have $\infty$ expected cost.

§ RELATED WORK

There has been much work done on logic and language techniques for reasoning about the cost of programs.

Type Theories for Cost Analysis Recent work <cit.> have developed (in)equational
theories for reasoning about costs of programs inside a modal depedently-typed logic. Their framework
can reason about monadic effects by using the Writer monad transformer, similarly to what we have done,
but, due to being inside a total dependent type theory, they cannot represent fixed-point combinators. Furthermore,
they can only handle discrete probabilities, whereas we can easily accommodate both arbitrary recursion
as well as continuous distributions.

Other work has focused in designing type theories for doing relational reasoning of programs <cit.>.
Even though these approaches can reason about functional programs as well, they are limited to deterministic programs.

Automatic Resource Analysis One fruitful research direction has been the automatic amortized resource analysis (AARA)
which uses a type system to annotate programs with their
cost and automatically infer the cost of the program. By now, these techniques have been extended to reason
about recursive types <cit.>, probabilistic programs <cit.> and programs <cit.> with local state.

Something quite appealing about their approach is that it is completely automatic, whereas our approach requires solving a, possibly
hard, recurrence relation by hand. That being said, their system can only accommodate polynomial bounds, meaning that
they cannot infer the $n\log(n)$ bound for the probabilistic quicksort like we do. Recently, AARA has been extended to
accommodate exponential bounds <cit.> in deterministic programs, though it is still unclear if the same
technique can be extended to the probabilistic setting, meaning that they cannot analyse the
behaviour of exponentially slow programs such as the expected coin tosses one.

There have been other type-based approach to automatically reasoning about cost of programs, such as the language TiML <cit.>.
This language allow users to annotate type signatures with cost-bounds and the type checking algorithm and infer and check these bounds.
The main limitation of TiML in comparison to our work is that it cannot handle probabilistic programs.

It is an interesting line of future work understanding to what extent solving recurrence relations can be automated in the context
of $\meta$.

Recurrence for Expected Cost There has been some work done in exploring languages for expressing
recurrence relations for expected cost. For example, <cit.> provides a language for representing probabilistic
recurrence relations and a tool for analysing their tail-bounds. The main drawback of these approaches is that the languages
are not very expressive. In particular they do not have higher-order functions.

<cit.> define a first-order probabilistic functional language for manipulating data structures and
automatically infer bounds on the expected cost of programs. The main limitation of their approach compared to ours is that
their language is first-order.

Reasoning about expected cost has also been explored for imperative languages. For instance, in <cit.> the authors fevelop a weakest pre-condition calculus for reasoning about the expected cost of programs. Again, they can only reason about first-order imperative programs.

§ CONCLUSION AND FUTURE WORK

In this work we have presented $\meta$, a metalanguage for reasoning about expected cost of recursive probabilistic programs.
It extends the existing work of <cit.> to the probabilistic setting. We have proposed two different kinds of
extensions, one based on the writer monad transformer while the second one uses a novel expected cost monad. Furthermore,
we have showed that in the absence of unbounded recursion, these two semantics coincide, while when programming with subprobability distributions
we have proved that the expected cost semantics is an upper bound to the cost semantics.

We have justified the versatility of our expected cost semantics by presenting a few case-studies. In particular, the expected cost
semantics obtains, compositionally, the familiar recurrence cost relations for non-trivial programs. In particular, for the randomized quicksort algorithm,
the semantic recurrence relation recovers the $O(n\log n)$ bound.

We conjecture that the techniques presented in this paper can be used in various other tantalizing directions. By slightly modifying
the expected cost monad we suspect that we can also reason about higher-moments of probabilistic programs. In particular, the variance
of costs is a useful measure to be able to reason about.

Going beyond probability, by adopting a more abstract approach on the expected cost monad, it might be possible to reason about other
kinds of effects. For instance, when reasoning about non-deterministic programs it is useful to give bounds on the worse/best case

More generally, we are also interested in laying on firm categorical grounds our logical relations technique. Furthermore, the lack
of a monad morphism in the subprobabilistic case suggests that there might extensions of this techniques based on $2$-category theory,
where the monad morphism laws do not hold exactly, only up to a $2$-cell, or inequality in this particular case.

#1     #1DOI:0#1
#1     #1     #1     #1     #1#1          #1#1   #1#1

[Batz, Kaminski, Katoen, Matheja, and
VerschtBatz et al2023]
authorpersonKevin Batz,
personBenjamin Lucien Kaminski, personJoost-Pieter
Katoen, personChristoph Matheja, and personLena
Verscht. year2023.
titleA calculus for amortized expected runtimes.

[Chatterjee, Fu, Novotnỳ, and
HasheminezhadChatterjee et al2016]
authorpersonKrishnendu Chatterjee,
personHongfei Fu, personPetr Novotnỳ, and
personRouzbeh Hasheminezhad. year2016.
Algorithmic analysis of qualitative and
quantitative termination problems for affine probabilistic programs. In
booktitlePrinciples of Programming Languages (POPL).

[Çiçek, Barthe, Gaboardi, Garg, and
HoffmannÇiçek et al2017]
authorpersonEzgi Çiçek,
personGilles Barthe, personMarco Gaboardi,
personDeepak Garg, and personJan Hoffmann.
Relational cost analysis. In
booktitlePrinciples of Programming Languages (POPL).

[Cutler, Licata, and DannerCutler
et al2020]
authorpersonJoseph W Cutler, personDaniel R
Licata, and personNorman Danner.
titleDenotational recurrence extraction for amortized

[Danner, Licata, and RamyaaDanner
et al2015]
authorpersonNorman Danner, personDaniel R
Licata, and personRamyaa Ramyaa.
Denotational cost semantics for functional
languages with inductive types. In booktitleInternational
Conference on Functional Programming (ICFP).

[Danner, Paykin, and RoyerDanner
et al2013]
authorpersonNorman Danner, personJennifer
Paykin, and personJames S Royer.
A static cost analysis for a higher-order
language. In booktitle7th workshop on Programming languages
meets program verification.

[Grodin, Sterling, Niu, and HarperGrodin
et al2023]
authorpersonHarrison Grodin, personJonathan
Sterling, personYue Niu, and personRobert Harper.
Decalf: A Directed, Effectful Cost-Aware Logical
journalarXiv preprint arXiv:2307.05938

[Grosen, Kahn, and HoffmannGrosen
et al2023]
authorpersonJ. Grosen, personD. M. Kahn,
and personJ. Hoffmann. year2023.
Automatic Amortized Resource Analysis with Regular
Recursive Types. In booktitleLogic in Computer Science

[Heunen, Kammar, Staton, and YangHeunen
et al2017]
authorpersonChris Heunen, personOhad
Kammar, personSam Staton, and personHongseok
Yang. year2017.
A convenient category for higher-order probability
theory. In booktitleLogic in Computer Science (LICS).

[Hoffmann, Das, and WengHoffmann
et al2017]
authorpersonJan Hoffmann, personAnkush Das,
and personShu-Chun Weng. year2017.
Towards automatic resource bound analysis for
OCaml. In booktitleSymposium on Principles of Programming
Languages (POPL).

[Hoffmann and ShaoHoffmann and Shao2015]
authorpersonJan Hoffmann and personZhong
Shao. year2015.
Automatic static cost analysis for parallel
programs. In booktitleEuropean Symposium on Programming

[Kahn and HoffmannKahn and Hoffmann2020]
authorpersonDavid M Kahn and personJan
Hoffmann. year2020.
Exponential automatic amortized resource analysis.
In booktitleFoundations of Software Science and Computation
Structures (FoSSaCS).

[Kaminski, Katoen, Matheja, and
OlmedoKaminski et al2016]
authorpersonBenjamin Lucien Kaminski,
personJoost-Pieter Katoen, personChristoph Matheja,
and personFederico Olmedo. year2016.
Weakest precondition reasoning for expected
run–times of probabilistic programs. In booktitleEuropean
Symposium on Programming (ESOP).

authorpersonRichard M Karp.
Probabilistic recurrence relations.
journalJournal of the ACM (JACM)

authorpersonShin-ya Katsumata.
A semantic formulation of $\top\top$-lifting and
logical predicates for computational metalanguage. In
booktitleInternational Workshop on Computer Science Logic.
Springer, pages87–102.

authorpersonShin-ya Katsumata.
Relating computational effects by
journalInformation and Computation

[Kavvos, Morehouse, Licata, and DannerKavvos
et al2019]
authorpersonGA Kavvos, personEdward
Morehouse, personDaniel R Licata, and personNorman
Danner. year2019.
Recurrence extraction for functional programs
through call-by-push-value. In booktitlePrinciples of
Programming Languages (POPL).

[Kura, Urabe, and HasuoKura
et al2019]
authorpersonSatoshi Kura, personNatsuki
Urabe, and personIchiro Hasuo.
Tail probabilities for randomized program runtimes
via martingales for higher moments. In booktitleTools and
Algorithms for the Construction and Analysis of Systems (TACAS).

[Leutgeb, Moser, and ZulegerLeutgeb
et al2022]
authorpersonLorenz Leutgeb, personGeorg
Moser, and personFlorian Zuleger.
Automated expected amortised cost analysis of
probabilistic data structures. In booktitleComputer Aided
Verification (CAV).

authorpersonPaul Blain Levy.
thesistypePh.D. Dissertation.

[Lichtman and HoffmannLichtman and
authorpersonBenjamin Lichtman and
personJan Hoffmann. year2017.
Arrays and references in resource aware ML. In
booktitleFormal Structures for Computation and Deduction
(FSCD 2017).

authorpersonE Moggi. year1989.
Computational lambda-calculus and monads. In
booktitleLogic in Computer Science (LICS).

[Motwani and RaghavanMotwani and
authorpersonRajeev Motwani and
personPrabhakar Raghavan. year1995.
booktitleRandomized algorithms.
publisherCambridge university press.

[Ngo, Carbonneaux, and HoffmannNgo
et al2018]
authorpersonVan Chan Ngo, personQuentin
Carbonneaux, and personJan Hoffmann.
Bounded expectations: resource analysis for
probabilistic programs. In booktitleProgramming Language
Design and Implementation (PLDI).

[Niu, Sterling, Grodin, and HarperNiu
et al2022]
authorpersonYue Niu, personJonathan
Sterling, personHarrison Grodin, and personRobert
Harper. year2022.
A cost-aware logical framework. In
booktitlePrinciples of Programming Languages (POPL).

authorpersonJames R Norris.
booktitleMarkov chains.
Number 2. publisherCambridge university press.

[Rajani, Gaboardi, Garg, and HoffmannRajani
et al2021]
authorpersonVineet Rajani, personMarco
Gaboardi, personDeepak Garg, and personJan
Hoffmann. year2021.
A unifying type-theory for higher-order (amortized)
cost analysis. In booktitleSymposium on Principles of
Programming Languages (POPL).

[Sun, Fu, Chatterjee, and GoharshadySun
et al2023]
authorpersonYican Sun, personHongfei Fu,
personKrishnendu Chatterjee, and personAmir Kafshdar
Goharshady. year2023.
Automated Tail Bound Analysis for Probabilistic
Recurrence Relations. In booktitleComputer Aided
Verification (CAV).

[Vákár, Kammar, and
StatonVákár et al2019]
authorpersonMatthijs Vákár,
personOhad Kammar, and personSam Staton.
A domain theory for statistical probabilistic
programming. In booktitlePrinciples of Programming Languages

[Wang, Kahn, and HoffmannWang
et al2020]
authorpersonDi Wang, personDavid M Kahn,
and personJan Hoffmann. year2020.
Raising expectations: automating expected cost
analysis with types. journalInternational Conference on
Functional Programming (ICFP) (year2020).

[Wang, Wang, and ChlipalaWang
et al2017]
authorpersonPeng Wang, personDi Wang, and
personAdam Chlipala. year2017.
TiML: a functional language for practical
complexity analysis with invariants. In booktitleObject-oriented Programming, Systems, Languages, and Applications (OOPSLA).

§ MONADIC SEMANTICS OF CBPV

Let $\cat{C}$ be a Cartesian closed category and $T : \cat{C} \to \cat{C}$ a strong monad over it. An alternative
definition of monads is it being a triple $(T, \eta, \mu)$, where $T$ and $\eta$ are natural transformations as before,
but $\mu : T^2 \to T$, the multiplication, replaces the bind natural transformation. The monad laws under this
definition become:

\[\begin{tikzcd}
{T^3} & {T^2} & T & {T^2} & T \\
{T^2} & T && T
\arrow["1"', from=1-3, to=2-4]
\arrow["T\eta", from=1-3, to=1-4]
\arrow["\mu", from=1-4, to=2-4]
\arrow["1", from=1-5, to=2-4]
\arrow["{\eta_T}"', from=1-5, to=1-4]
\arrow["{\mu_T}"', from=1-1, to=2-1]
\arrow["\mu"', from=2-1, to=2-2]
\arrow["\mu", from=1-2, to=2-2]
\arrow["T\mu", from=1-1, to=1-2]
\end{tikzcd}\]

It is possible to show that these definitions are equivalent: given bind $(-)^\#$, the multiplication can be defined as $\mu = id_{TA}^\#$.
Conversely, given a multiplication, the bind is defined as $f^\# = T f; \mu$.
This alternative definition is a bit better suited for the original purposes of monads, where it was used as a unifying way of representing
concepts from universal algebra.

This alternative presentation lend itself quite well to the semantics of CBPV-based calculi where, given a monad $T$, computation types denote

A $T$-algebra is a pair $(A, \alpha)$, where $A$ is a $\cat{C}$ object and $\alpha : T A \to A$ is a morphism, such that

\[\begin{tikzcd}
A & TA & {T^2A} & TA \\
& A & TA & A
\arrow["{\eta_A}", from=1-1, to=1-2]
\arrow["\alpha", from=1-2, to=2-2]
\arrow["{id_A}"', from=1-1, to=2-2]
\arrow["T\alpha"', from=1-3, to=2-3]
\arrow["\alpha"', from=2-3, to=2-4]
\arrow["{\mu_A}", from=1-3, to=1-4]
\arrow["\alpha", from=1-4, to=2-4]
\end{tikzcd}\]

Given a $T$-algebra $(A, \alpha)$ we denote by $A_\bullet$ the object of the $T$-algebra.

Given an object $A$, the pair $(TA, \mu_A)$ is a $T$-algebra.

Given a $T$-algebra $(A, \alpha)$ and an objects $B$, we can equip $B \to B$ with the $T$-algebra structure $\alpha_{B \to A} = \varepsilon; B\Rightarrow (st; T(ev; \alpha))$,
where $\varepsilon_A : A \to (B \Rightarrow (B \times A))$ is the unit of the Cartesian closed adjunction.

Algebras and their morphisms can be organized as a category, frequently denoted by $\cat{C}^T$. However, for the purposes of CBPV
a different category is used:

The category $\widetilde{\cat{C}}^T$ is the full subcategory of $\cat{C}$ that contain $T$-algebras as objects. This category
is also called the category of algeras and plain maps.

The idea is that values are interpreted as objects in $\cat{C}$ while computation types are $T$-algebras. Assuming the only the base
type in the calculus to be $\nat$ and an object $\nat$ in the base category, The interpretation of values and
computations are as follows:

\begin{align*}
\sem{\nat}^v &= \nat\\
\sem{U \overline\tau}^v &= \sem{\overline\tau}^c_\bullet\\
\sem{\tau_1 \times \tau_2}^v &= \sem{\tau_1}^v \times \sem{\tau_2}^v\\
\\
\sem{F \tau}^c &= (T \sem{\tau}^v, \mu_{\sem{\tau}^v})\\
\sem{\tau \to \overline{\tau}}^c &= (\sem{\tau}^v \Rightarrow \sem{\overline \tau}^c, \alpha_{\sem{\tau}^v \to \sem{\overline \tau}^c})
\end{align*}

It is also possible to give semantics to the terms of the language as depicted in <Ref>. The semantics of if-statements
use the fact that $\nat \cong 1 + \nat$, so you can define its semantics by using the universal property of coproducts $[t, (!_\nat; u)]$, where
$!_A : A \to 1$ is the unique arrow into the terminal object. The abstraction and application rule use the adjoint structure $(\Lambda, ev)$,
of Cartesian closed categories, where $\Lambda$ and $ev$ are the unit and counit of the adjunction, respectively. The produce rule uses the
unit of the monad while the bind rule is the sequential composition of a free algebra with a non-free algebra and, therefore, requires applying
the functor $T$ and using the algebra structure of the output — when the output map is a free algebra, this operation is equal to the bind
of the monad. Thunk and force are basically no-ops in this semantics, while the rules let and unpair are sequential compositions. Pair is
the universal property of products.

[var] Γ_1 ×(τ×Γ_2) !×π_1 τ

[if]ΓV   Γt τ   Γu τΓ⟨id;  V⟩; [t, (!; u)] τ

[abstraction]Γ×τt τΓΛ_Γ; τ⇒t τ⇒τ

[application]ΓV τ  Γt : τ→τΓ⟨t, V⟩; ev : τ

[produce]ΓV τΓV; η_τ T τ

[bind]Γt T τ'
Γ×τ' u (τ, α_τ)Γ⟨id_Γ, t⟩; st; T u; α_τ (τ, α_τ)

[thunk]Γt (τ, α_τ)Γt τ

[force]ΓV τΓV (τ, α_τ)

[let]ΓV τ'
Γ×τ' t τΓ⟨id_Γ, V⟩; t τ

[pair]Γt_1 τ_1   Γt_2 τ_2Γ⟨t_1, t_2⟩ τ_1×τ_2
[unpair]ΓV τ_1 ×τ_2   Γ×τ_1 ×τ_2 t τΓ⟨id, V⟩; t τ

CBPV monadic semantics

§.§ Equational presentation of $\meta$

For the sake of simplicity of the equational theory, we will assume the barycentric operations $\oplus_p$
with the syntactic sugar

\begin{align*}
&rnd(0) \rightsquigarrow \produce 0\\
&rnd(n+1) \rightsquigarrow T(n) \oplus_{\frac 1 {n+2}} \produce (n + 1)
\end{align*}

For every $n : \nat$, $\sem {rnd(n)} = \sem{\rand\, n}$.

The proof follows by induction.

Below we present the non-structural equations of $\meta$. The first block is present in every CBPV calculus
with natural numbers. The second block is the recursion equation, the third block are the barycentric
algebra equations and the final three are the monoid equations.

\begin{align*}
&\ifthenelse 0 t u \equiv t\\
&\ifthenelse {(n + 1)} t u \equiv u\\
&t \equiv \ifthenelse x t t\\
&\app{(\lamb x t)} V \equiv \subst t V x\\
&\letbe x V t \equiv \subst t V x \\
& t \equiv \lamb x {\app t x}\\
& \force(\thunk\, t) \equiv t\\
& \thunk(\force\, V) \equiv V\\
& x \leftarrow (\produce V); t \equiv \subst t V x\\
& x \leftarrow t; \produce x \equiv t\\
\\
\\
\\
& \fix x.\, t = t\, (\thunk (\fix x.\, t))\\\\
&t \oplus_0 u \equiv t\\
&t \oplus_{p} u \equiv u \oplus_{1-p} t\\
&t \oplus_p t \equiv t\\
&t\oplus_p (u \oplus_q t') \equiv (t \oplus_{pq} u) \oplus_{\frac{p(1-q)}{1 - pq}} t'\\
\\
&\charge n; \charge m \equiv \charge {n + m}\\
&\charge 0; t \equiv t\\
&t; \charge 0 \equiv t
\end{align*}

§ DENOTATIONAL SOUNDNESS PROOF

If $\mu_1 \CRel_{F\tau} \mu_2$ then for every pair of functions $f_1 : A_1 \to \R$ and $f_2 : A_2 \to \R$, such that for every
$a_1 \CRel_A a_2$, $f_1(a_1) = f_2(a_2)$, $\int f_1 \diff \mu_1 = \int f_2 \diff \mu_2$

Since by assumption $\mu_1 \CRel_{F\tau} \mu_2$, there is a coupling $\nu$ over the support of $\VRel_\tau$, which allows us to conclude:

\[\int f_1 \diff\mu_1 = \int \frac 1 2 (f_1 + f_2) \diff \nu = \int f_2 \diff \mu_2\]

The equalities above hold because in the support of $\nu$, $f_1(a_1) = f_(a_2)$, making $f_1 = \frac 1 2 (f_1 + f_2) = f_2$ and since
$\nu$ is a joint distribution with marginals $\mu_1$ and $\mu_2$, we have the equality of integrals above.

The following lemma is the most technical aspect of the soundness proof and, intuitively, is saying that the logical relations for
computation types can be equipped with "algebra" structures. Furthermore, since we are proving two similar looking theorems for the
probabilistic and subprobabilistic cases, and the soundness proof in both cases
is basically the same, we will only present the proof to the subprobabilistic case, and highlight in the proof what would differ for
the probabilistic case.

Let $\tau_1$, $\tau_2$ and $\overline{\tau}$ be types and $f_1 : \semcs{\tau_1}^v \times \semcs{\tau_2}^v \to \semcs{\overline{\tau}}^c$, and
$f_2 : \semec{\tau_1}^v \times \semec{\tau_2}^v \to \semec{\overline{\tau}}^c$ be $\wqbs$ morphisms such that $f_1 \times f_2$, when the
input is restricted to $\VRel_{\tau_1} \times \VRel_{\tau_2}$, the output is restricts to $\CRel_{\overline\tau}$. It is true
that $(st; T_1(f_1); \alpha_{\overline{\tau}}) \times (st; T_2(f_2); \alpha_{\overline{\tau}})$, when its input is restricted to
$\VRel_{\tau_1} \times \CRel_{F\tau_2}$, the output is still restricted to $\CRel_{\overline\tau}$.

This can be proved by induction on the computation type $\overline{\tau}$:

$F\tau$: In order to prove $f_1^\#(r, \nu) \CRel_{F\tau'} f^\#_2(\mu)$ we have to prove that their expected costs are
related by the inequality given by the definition of $\CRel_{F\tau}$
and show that there is a coupling over $\nu$ and $\mu_2$, where $\mu_2$ is the second marginal of $\mu$, such that it
factors through the inclusion $\Psub (\VRel_{\tau'}) \hookrightarrow \Psub (\semcs{\tau'}^v \times \semec{\tau'}^v)$.
By unfolding the definitions, we get

\begin{align*}
\pi_1(f_1^\#(r, \nu)) &= r + \int (\pi_1 \circ f_1) \diff \nu \\
\mathbb E(f_2^\#(\mu)) &= \int\int n \norm{f_2(a)} \mu(\diff n, \diff a) + \int n \diff(f_2^\#(\mu))
\end{align*}

In the second expression the left hand side term being add corresponds to the expected cost of the input
while the second one corresponds to the cost of the continuation. As such, it is sensible that in order to
reason about their difference we should reason individually about $r - \int\int n \norm{f_2(a)}$ and
$\int (\pi_1 \circ f_1) \diff \nu - \int n \diff(f_2^\#(\mu))$.

\begin{align*}
& \int\int n \norm{f_2(a)} \diff \mu \leq \int\int n \diff \mu \leq r
\end{align*}

For the second expression, assuming $\forall a' \VRel_{\tau'} a, \mathbb{E}(f_2(a)) \leq (\pi_1 \circ f_1)(a')$,

\begin{align*}
& \int \mathbb{E}(f_2(a)) \gamma(\diff a, \diff a') \leq \int (\pi_1 \circ f_1)(a') \gamma(\diff a, \diff a') = \int (\pi_1 \circ f_1)(a') \nu(\diff a')\\
& \int n \diff(f_2^\#(\mu)) = \int \mathbb{E}(f_2(a)) \mu(\diff a) = \int \mathbb{E}(f_2(a)) \gamma(\diff a, \diff a')\\
\end{align*}

By adding these two inequalities we obtain exactly the first condition of the relation $\CRel_{F\tau}$. In the probabilistic
case every inequality is an equality, since $\norm{f(a)} = 1$ and the definition of the $\CRel_{F\tau}$ would be equalities as well.
The second condition follows from observing that when restricting the domain of $f_1\times f_2$
to $\VRel_\tau$, we can extract from it a function $g : \VRel_\tau \to \Psub(\VRel_{\tau'})$ such that, given inputs $(v_1, v_2)$,
the marginals of $g(v_1, v_2)$ are equal to $\pi_2(f_1(v_1))$ and $f_2(v_2)_2$ since, by assumption, $f_1(v_1) \CRel_{F\tau'} f_2(v_2)$.
Given this function, we define the coupling $g^\#(\mu')$, where $\mu'$ is the coupling given by $(r, \nu)\CRel_{F\tau} \mu$. Showing
that it has the right marginals follows from linearity of the marginal function, concluding the proof. This part of the proof remains the
same in the probabilistic case

$\tau \to \overline{\tau}$: This case relies more on notation and, therefore, in order to simplify the presentation, we will
rely on the symmetry of $f_1$ and $f_2$ and work on the generic expression $st; T(f); \alpha_{\tau \to \overline{\tau}}$ that
can be instatiated to both $f_1$ and $f_2$.
By definition of $\CRel_{\tau\to\overline{\tau}}$, in order to define a morphism
$\VRel_{\tau_1} \times \VRel_{\tau_2} \to \CRel_{\tau \to \overline{\tau}}$, it suffices to defines its transpose
$\VRel_{\tau} \times (\VRel_{\tau_1} \times \VRel_{\tau_2}) \to \CRel_{\overline{\tau}}$.
Since the algebra structure of $\alpha_{\tau \to \overline{\tau}}$ is defined as $\eta; id_\tau \Rightarrow (st; T(ev); \alpha_{\overline{\tau}})$,
we want to show that the the map $id_\tau \times (st; T f; \eta; id_\tau \Rightarrow (st; T(ev); \alpha_{\overline{\tau}})); ev$, i.e.
can be rewritten in the format $st; T(f'); \alpha_{\overline\tau}$, so that we can apply the inductive hypothesis. This equation
holds, up to isomorphism, by the following commutative diagram:

\[\begin{tikzcd}
{\tau \times (\tau_1 \times T\tau_2) } & {\tau \times T(\tau_1 \times \tau_2) } & {\tau \times T(\tau \Rightarrow\overline{\tau})} && {\tau \times (\tau \Rightarrow(\tau \times T(\tau \Rightarrow\overline{\tau})))} \\
&& {\tau\times T(\tau\Rightarrow\overline\tau)} && {\tau \times(\tau \Rightarrow \overline{\tau})} \\
{(\tau \times \tau_1) \times T\tau_2} & {T(\tau \times (\tau_1 \times \tau_2))} & {T(\tau \times (\tau \Rightarrow\overline\tau))} & T\overline\tau & \overline\tau
\arrow["{id_\tau\times st}", from=1-1, to=1-2]
\arrow["{st; T(a^{-1})}"', from=3-1, to=3-2]
\arrow["{T(\tau \times f)}"', from=3-2, to=3-3]
\arrow["{T ev}"', from=3-3, to=3-4]
\arrow["{\alpha_{\overline\tau}}"', from=3-4, to=3-5]
\arrow["a"', from=1-1, to=3-1]
\arrow["st"', from=1-2, to=3-2]
\arrow["{\tau\times Tf}", from=1-2, to=1-3]
\arrow["ev", from=2-5, to=3-5]
\arrow["{id_\tau \times (id_\tau \Rightarrow (st; Tev ; \alpha_{\overline\tau}))}", from=1-5, to=2-5]
\arrow["\tau\times\eta", from=1-3, to=1-5]
\arrow["ev", from=1-5, to=2-3]
\arrow["st", from=2-3, to=3-3]
\arrow[Rightarrow, no head, from=1-3, to=2-3]
\arrow[from=1-1, to=1-2]
\end{tikzcd}\]

From left to right, the first diagram commutes by definition of strong monad, the second commutes from naturality of the
strength of $T$, the triangular diagram commutes by the Cartesian closed adjunction and the final diagram commutes by
naturality of $ev$.

Note that the same argument also holds for the parametric case where the domain has shape $\sem{\Gamma}^v \times \sem{\tau}^v$ and
you must use the strength $st_{\Gamma, \tau}$ of the monad in order to only Klesli-lift the second input of $f_i$.

We can now prove the full statement.

The proof follows from mutual induction on $\Gamma \vdash^v V : \tau$ and $\Gamma \vdash^c t : \overline{\tau}$. Many
of the cases follow by just applying the induction hypothesis or by assumptions of theorem. We go over the most
interesting cases:

Comp This case follows from <Ref>.

Fix This theorem follows from the induction hypothesis and from the fact that the relations $\CRel^c_{\overline{\tau}}$
are closed under suprema of ascending chains.

First apply the induction hypothesis to $V$ and assume that $\sem{V}_1 = v_1$ and $\sem{V}_2 = v_2$.
By construction, $\eta^{T_1}(v_1) \CRel^v_{F\tau}\eta^{T_2}(v_2)$, since they both have the same expected
value and the coupling is $\delta_{(v_1, v_2)}$.

By applying the inductive hypothesis to $V$ we may do case analysis on it and if it is the empty list,
we use the inductive hypothesis on $t$ and, otherwise, we use the inductive hypothesis on $u$.