# Convexity and Order in Probabilistic Call-by-Name FPC

Mathys Rennela  Centrum Wiskunde & Informatica, Amsterdam<EMAIL_ADDRESS>
###### Abstract.

Kegelspitzen are mathematical structures coined by Keimel and Plotkin, in
order to encompass the structure of a convex set and the structure of a dcpo.
In this paper, we ask ourselves what are Kegelspitzen the model of. We adopt a
categorical viewpoint and show that Kegelspitzen model stochastic matrices
onto a category of domains. Consequently, Kegelspitzen form a denotational
model of pPCF, an abstract functional programming language for probabilistic
computing. We conclude the present work with a discussion of the
interpretation of (probabilistic) recursive types, which are types for
entities which might contain other entities of the same type, such as lists
and trees.

###### Key words and phrases:

convex set, kegelspitze, domain, recursive type, probabilistic computation

###### 1991 Mathematics Subject Classification:

F.3.2 Semantics of Programming Languages

The interplay between convexity and order in the semantics of probabilistic
programs has been a highly-coveted field of research since the first research
programs [20, 21] on the semantics of probabilistic computing, a programming
language paradigm which allows probabilistic branching of programs and also
updating of distributions.

Starting from an intuitive and minimalistic programming language perspective
on Keimel & Plotkin’s approach to probabilistic computations [23], the present
work provides a new take on the mathematical characterization of probabilistic
programs and brings an important building block to the study of the
interactions between the concepts of convexity and order within the theory of
probabilistic computing, namely by defining Kegelspitzen as mathematical
structures which combine convex sets with dcpos.

We introduce Kegelspitzen as pointed dcpos with a compatible convex structure
which carries a clear probabilistic interpretation (see Section 1). We pursue
in Section 2 with a categorical study of Kegelspitzen, which was absent from
Keimel & Plotkin’s original work [23].

Now, recall that (sub)convex sets are sets equipped with a (sub)convex
structure. After defining the Lawvere theory $\mathbb{L}$ of convex sets and
the Lawvere theory $\mathbb{L}_{\leq 1}$ of subconvex sets, and establishing
that those categories have all finite products (see Lemma 2.2), we show the
following theorem.

######  Theorem 2.3 (paraphrased).

The category of Kegelspitzen and affine Scott-continuous maps, i.e. Scott-
continuous maps which preserve the convex structures, is equivalent to the
order-enriched category of models (i.e. finite product-preserving order-
enriched functors) of the Lawvere theory of subconvex sets into the category
of pointed dcpos and strict Scott-continuous maps.

In a second step, we show that the category of Kegelspitzen and affine Scott-
continuous maps is monoidal closed (see Proposition 2.5), when equipped with
the smash product $\otimes_{\perp}$ [3, 1], i.e. the quotient of the cartesian
product $X\times Y$ (of two pointed dcpos $X$ and $Y$) by the relation
generated by the relation $\sim$ such that
$(x,\perp)\sim(\perp,y)\sim(\perp,\perp)$ for $x\in X$ and $y\in Y$. Moreover,
we show that the category of Kegelspitzen and Scott-continuous maps is
cartesian closed (see Proposition 2.6).

Then in Section 3, we use the cartesian closed structure of the category of
Kegelspitzen and Scott-continuous maps to interpret a probabilistic extension
called Probabilistic PCF (or shortly, pPCF) of the language PCF [26]. In
short, we extend PCF with terms $\text{coin}(\kappa)$ (where
$\kappa\in[0,1]\cap\mathbb{Q}$ is a probability) which reduce to the numeral
$\underline{0}$ with probability $\kappa$ and the numeral $\underline{1}$ with
probability $1-\kappa$. Therefore, pPCF’s transition system is probabilistic:
reductions are weighted by probabilities, and deterministic reductions are
weighted by the probability $1$.

We proceed to interpret types as Kegelspitzen and terms as Scott-continuous
maps. In particular, the type ${\rm Nature}$ is denoted by the Kegelspitze of
sub-distributions on the natural numbers:

$\mathcal{D}_{\leq
1}^{\infty}(\mathbb{N})\stackrel{{\scriptstyle\text{def}}}{{=}}\left\\{\varphi:\mathbb{N}\to[0,1]~{}\middle|~{}\sum_{n\in\mathbb{N}}\varphi(n)\leq
1\right\\}$

We obtain the following soundness property.

######  Proposition 3.4 (paraphrased).

The denotation under a context $\Gamma$ of a term $M$ (which isn’t a value) is
the sum of the denotations under the context $\Gamma$ of the terms that $M$
reduces to.

This mathematical observation leads us to the following adequacy result.

######  Theorem 4.4 (paraphrased).

The denotation of a closed term $M$ of type ${\rm Nature}$ maps every natural
number $n$ to the probability that $M$ reduces to the number $\underline{n}$
in pPCF’s leftmost outermost strategy.

We conclude the present work with a proof that the category of Kegelspitzen
and affine Scott-continuous maps is algebraically compact for locally
continuous endofunctors (see Corollary 5.5), and as such a model of the
language FPC, an extension of PCF with recursive types [12]: this settles
Kegelspitzen as an adequate categorical setting for denoting recursive types.

It is worth mentioning that previous work proved that probabilistic coherence
spaces constitute a fully abstract model of pPCF (see e.g. [6, 7, 10, 9]).
Moreover, probabilistic coherence spaces give an interpretation of recursive
types based on the relational model111Recall that in the relational model of
linear logic, all linear logic connectives are Scott continuous functions on
the class of sets ordered by inclusion. of linear logic, i.e. based on the
category $\mathbf{Rel}$ of sets and relations (see e.g. [9]).

Kegelspitzen offer an interesting categorical semantics within the scope of
probabilistic computing, especially as a step towards the study of the
semantics for a higher-order quantum programming language with recursive types
but also as a subset of the probabilistic fragment of a categorical model of a
language for quantum circuits based on C*-algebras (see [27]). Indeed, the
category $\mathbf{Fd}\mathbf{C}\mathbf{C^{*}\\-Alg}_{\mathrm{CPU}}$ of finite-
dimensional commutative C*-algebras and completely positive unital maps
between them is equivalent to the Lawvere theory of convex sets [15, Prop.
4.3].

##  1\. An introduction to the theory of Kegelspitzen

In this section, we give a concise introduction to Kegelspitzen, introduced by
Keimel & Plotkin [23] as pointed dcpos with a compatible convex structure
which carries a clear probabilistic interpretation. The word Kegelspitze
(plural Kegelspitzen) is the german term for “cone tip”.

But first, let us recall the formal definition of a convex set.

######  Definition 1.1.

A _convex set_ (resp. _subconvex set_) is a set $X$ together with an $m$-ary
function $(\overrightarrow{r})_{X}:X^{m}\to X$ for each vector
$\overrightarrow{r}=(r_{1}\dots r_{m})$ of non-negative real numbers with
$\sum_{i}r_{i}=1$ (resp. $\sum_{i}r_{i}\leq 1$), such that for each $m\times
n$ matrix $(s_{i,j})_{i,j}$ of non-negative real numbers such that
$\sum_{j}s_{i,j}=1$, we have
$\sum_{i}r_{i}.(\sum_{j}(s_{i,j}.x_{j}))=\sum_{j}((\sum_{i}(r_{i}.s_{i,j})).x_{j})$.

A _homomorphism_ of (sub)convex sets is a function that preserves the
algebraic structure. Homomorphisms are often called _affine maps_. We write
$\mathbf{Conv}$ (resp. ${\mathbf{Conv}_{\leq 1}}$) for the category of convex
sets (resp. subconvex sets) and affine maps between them.

A _convex dcpo_ is a convex set equipped with a dcpo structure such that the
functions that constitute its convex structure are Scott-continuous. A simple
example of a convex dcpo is the unit interval $[0,1]$ of the reals. We will
consider the category $\mathbf{dConv}$ of convex dcpos and affine Scott-
continuous maps, i.e. Scott-continuous functions which preserve the algebraic
structure. For two convex dcpos $D_{1}$ and $D_{2}$, the homset
$\mathbf{dConv}(D_{1},D_{2})$ can be seen as a dcpo (and is considered as such
in this chapter) or as a convex set.

A _pointed convex dcpo_ (or _subconvex dcpo_) is a convex set and a dcpo with
a least element that is a zero element for the convex structure. We will
consider the category $\mathbf{d}{\mathbf{Conv}_{\leq 1}}$ of pointed convex
dcpos and affine strict Scott-continuous maps.

A _Kegelspitze_ is a pointed convex dcpo $X$ with a convex structure such that
the scalar multiplication $\cdot:[0,1]\times X\to X$, defined by $\lambda\cdot
x=x\ \oplus_{\lambda}\perp$, is Scott-continuous in both arguments. When the
unit interval $[0,1]$ carries the Scott topology, the requirement is that the
scalar multiplication is continuous in the product topology of its domain. We
will refer to this assumption as the “Kegelspitzen condition”. The interested
reader can consult [23] for more details.

Alternatively, one can define a Kegelspitze as a pointed convex dcpo $X$ with
the following properties:

  * •

the function $f:[0,1]\times X^{2}\to X$ defined by
$f(\lambda,(x,y))=x\oplus_{\lambda}y$, where $[0,1]$ is endowed with the usual
Hausdorff topology, is continuous in both arguments;

  * •

for every natural number $n$, the function $\theta_{n,X}:S_{n}\times X^{n}\to
X$ defined by

$((\lambda_{i})_{i\leq n},(x_{i})_{i\leq n})\mapsto\sum_{i}\lambda_{i}\cdot
x_{i}$

(where $S_{n}=\mathcal{D}_{\leq
1}^{\infty}(n)\cong\\{(q_{1},\cdots,q_{n})\in[0,1]^{n}\mid\sum_{i=1}^{n}q_{i}\leq
1\\}$ carries the Scott topology) is continuous in both arguments

A _homomorphism of Kegelspitzen_ is an affine strict Scott-continuous map of
Kegelspitzen. Such homomorphisms are called _affine Scott-continuous maps_.
Then, the category $\mathbf{KS}$ is the category of Kegelspitzen and affine
Scott-continuous maps between them. For an historical account of the different
notions of Kegelspitzen, see [23, Remark 2.28].

Since we intend to use Kegelspitzen as a categorical model for higher-order
probabilistic computation, it seems natural to check whether it is a monoidal
closed category suitable for the interpretation of recursive types. A step
towards this goal requires to give a categorical account of Kegelspitzen, as
models of the Lawvere theory of subconvex sets in the category of pointed
dcpos and strict Scott-continuous maps.

##  2\. A categorical account of convexity and order

In this section, we will formally justify the definition of Kegelspitzen by
proving that they are models of the order-enriched Lawvere theory of subconvex
sets in the category $\mathbf{Dcpo}_{\perp!}$ of pointed dcpos and strict
Scott-continuous maps. But first, let us recall the preliminary notions
involved in our categorical construction of Kegelspitzen.

######  Definition 2.1 ([18]).

The monad $\mathcal{D}^{\infty}$ (resp. the monad $\mathcal{D}_{\leq
1}^{\infty}$) is the _infinitary (sub)probabilistic discrete distribution
monad_ on the category $\mathbf{Set}$. It is defined as follows on sets:

$\mathcal{D}^{\infty}(X)=\left\\{\varphi:X\to[0,1]~{}\middle|~{}\sum_{x}\varphi(x)=1\right\\}$
$\mathcal{D}_{\leq
1}^{\infty}(X)=\left\\{\varphi:X\to[0,1]~{}\middle|~{}\sum_{x}\varphi(x)\leq
1\right\\}$

In particular, when $X$ is a finite set of cardinality $n\in\mathbb{N}$,
identified with the $n$-element set noted $n$:

$\mathcal{D}^{\infty}(n)=\left\\{(x_{k})_{1\leq k\leq
n}\in[0,1]^{n}~{}\middle|~{}\sum_{k}x_{k}=1\right\\}$ $\mathcal{D}_{\leq
1}^{\infty}(n)=\left\\{(x_{k})_{1\leq k\leq
n}\in[0,1]^{n}~{}\middle|~{}\sum_{k}x_{k}\leq 1\right\\}$

For every function $f:X\to Y$, the function $\mathcal{D}_{(\leq
1)}^{\infty}(f):\mathcal{D}_{(\leq 1)}^{\infty}(X)\to\mathcal{D}_{(\leq
1)}^{\infty}(Y)$ is defined by:

$\varphi\mapsto\left(y\mapsto\sum_{x\in
f^{-1}(y)}\varphi(x)=\sum\left\\{\varphi(x)\in[0,1]~{}\middle|~{}f(x)=y\right\\}\right)$

The unit $\eta:\text{Id}_{X}\Rightarrow\mathcal{D}_{(\leq 1)}^{\infty}$ and
the multiplication $\mu:\mathcal{D}_{(\leq 1)}^{\infty}\mathcal{D}_{(\leq
1)}^{\infty}\Rightarrow\mathcal{D}_{(\leq 1)}^{\infty}$ are given for every
set $X$ by the following:

$\displaystyle\eta_{X}:X$ $\displaystyle\to\mathcal{D}_{(\leq 1)}^{\infty}X$
$\displaystyle\mu_{X}:\mathcal{D}_{(\leq 1)}^{\infty}\mathcal{D}_{(\leq
1)}^{\infty}X$ $\displaystyle\to\mathcal{D}_{(\leq 1)}^{\infty}X$
$\displaystyle x$ $\displaystyle\mapsto\delta_{x}$ $\displaystyle\Phi$
$\displaystyle\mapsto\left(x\mapsto\sum_{\varphi\in\mathcal{D}_{(\leq
1)}^{\infty}X}\Phi(\varphi)\cdot\varphi(x)\right)$

where $\delta_{x}$ is the Dirac notation for $x\in X$, i.e. for every $y\in
X$, $\delta_{x}(y)=1$ if $x=y$ and $\delta_{x}(y)=0$ if $x\neq y$.

Recall that a Lawvere theory is a small category $\mathbb{T}$ with (finite)
products such that every object is identified with a natural number
$n\in\mathbb{N}$ and that a model of a Lawvere theory $\mathbb{T}$ is a
product-preserving functor $\mathbb{T}\to\mathbf{Set}$ [24]. More generally, a
model of a Lawvere theory $\mathbb{T}$ into a monoidal category $\mathbf{V}$
is a tensor-preserving functor $\mathbb{T}\to\mathbf{V}$.

In what follows, we want to construct the categories $\mathbb{L}$ and
$\mathbb{L}_{\leq 1}$ to be the Lawvere theories of the equational theories of
convex sets and subconvex sets respectively. We define $\mathbb{L}$ (resp.
$\mathbb{L}_{\leq 1}$) as the opposite category of free
$\mathcal{D}^{\infty}$-algebras (resp. free $\mathcal{D}_{\leq
1}^{\infty}$-algebras) on finitely many generators. In the language of monads,
this means that $\mathbb{L}$ (resp. $\mathbb{L}_{\leq 1}$) is the category
$\text{Kl}_{\mathbb{N}}(\mathcal{D}^{\infty})^{\mathbf{op}}$ (resp.
$\text{Kl}_{\mathbb{N}}(\mathcal{D}_{\leq 1}^{\infty})^{\mathbf{op}}$), i.e.
the opposite category of the Kleisli category of the monad
$\mathcal{D}^{\infty}$ (resp. $\mathcal{D}_{\leq 1}^{\infty}$) with objects
restricted to natural numbers $n$ seen as finite sets of cardinality $n$. To
be precise, the category $\mathbb{L}$ (resp. $\mathbb{L}_{\leq 1}$) is the
category with natural numbers as objects together with arrows $n\to m$ seen as
probabilistic transition matrices $m\to\mathcal{D}^{\infty}(n)$ (resp. sub-
probabilistic transition matrices $m\to\mathcal{D}_{\leq 1}^{\infty}(n)$),
i.e. as stochastic matrices of size $m\times n$, i.e. $m\times n$ matrices
with positive entries such that each column sums up to $1$ (resp. sums up to a
value below or equal to $1$).

This view of distribution monads via Lawvere theories has been explored by
various authors (see e.g. [15, 14, 5, 17]). We prove that $\mathbb{L}$ and
$\mathbb{L}_{\leq 1}$ have all finite coproducts, adopting the view of Kleisli
maps as stochastic matrices, where the Kleisli composition corresponds in this
context to matrix multiplication. This approach is also present in [14].

######  Lemma 2.2.

The categories $\mathbb{L}$ and $\mathbb{L}_{\leq 1}$ have all finite
products.

###### Proof.

We show that the Lawvere theories $\mathbb{L}$ and $\mathbb{L}_{\leq 1}$ have
all finite products (with addition as product) by showing that the Kleisli
categories $\text{Kl}_{\mathbb{N}}(\mathcal{D}^{\infty})$ and
$\text{Kl}_{\mathbb{N}}(\mathcal{D}_{\leq 1}^{\infty})$ have all finite
coproducts (with addition as coproduct).

For every natural number $n\in\mathbb{N}$, there is exactly one stochastic
matrix of size $n\times 0$ and therefore $0$ is an initial object for
$\text{Kl}_{\mathbb{N}}(\mathcal{D}_{(\leq 1)}^{\infty})$.

Identity maps are defined to be $\eta_{n}:n\to\mathcal{D}_{(\leq
1)}^{\infty}(n)$. We call the corresponding $n\times n$ stochastic matrix
$1_{n}$ and consider the inclusion maps $\kappa_{1}:n_{1}\to n_{1}+n_{2}$ and
$\kappa_{2}:n_{2}\to n_{1}+n_{2}$ as the stochastic matrices
$K_{1}=\left(\begin{smallmatrix}1_{n_{1}}\\\
0_{n_{2}}\end{smallmatrix}\right)$ and
$K_{2}=\left(\begin{smallmatrix}0_{n_{1}}\\\
1_{n_{2}}\end{smallmatrix}\right)$.

Now, consider a pair of stochastic matrices $A_{1}$ and $A_{2}$, with
corresponding maps $f_{1}:n_{1}\to p$ and $f_{2}:n_{2}\to p$ (with
$n_{1},n_{2},p\in\mathbb{N}$).

Recall that to satisfy the universal property of the coproduct, we must
construct an unique map $f:n_{1}+n_{2}\to p$ such that the equation
$f_{i}=f\circ\kappa_{2}$ holds for $i\in\\{1,2\\}$. Then, we observe that the
stochastic matrix
$A=\left(\begin{smallmatrix}A_{1}&A_{2}\end{smallmatrix}\right)$ is the unique
stochastic matrix whose multiplication by $K_{i}$ gives $A_{i}$ (for
$i\in\\{1,2\\}$) and therefore, we define $f$ to be the Kleisli map
corresponding to the stochastic matrix $A$.

∎

Then, the coproduct $f_{1}+f_{2}:n_{1}+n_{2}\to p_{1}+p_{2}$ of two Kleisli
maps $f_{1}:n_{1}\to p_{1}$ and $f_{2}:n_{2}\to p_{2}$ is defined as the
diagonal
$A_{1}+A_{2}\stackrel{{\scriptstyle\text{def}}}{{=}}\left(\begin{smallmatrix}A_{1}&0\\\
0&A_{2}\end{smallmatrix}\right)$ of their corresponding stochastic maps
$A_{1}$ and $A_{2}$. It follows that $\mathbb{L}$ and $\mathbb{L}_{\leq 1}$
are Lawvere theories, since they are strict monoidal categories when one
consider $+:\mathbb{L}_{(\leq 1)}\times\mathbb{L}_{(\leq
1)}\to\mathbb{L}_{(\leq 1)}$ as tensor product, with the natural number $0$ as
unit.

Recall that the category $\mathbf{Dcpo}_{\perp!}$ of pointed dcpos and strict
Scott-continuous maps is monoidal closed when equipped with the smash product
defined in the introduction. Now, observe that the Lawvere theory
$\mathbb{L}_{\leq 1}$ is a small $\mathbf{Dcpo}_{\perp!}$-category: for every
pair $(n,m)$ of natural numbers, the homset

$\mathbb{L}_{\leq
1}(n,m)\stackrel{{\scriptstyle\text{def}}}{{=}}\mathcal{D}_{\leq
1}^{\infty}(n)^{m}$

is a dcpo as a finite product of dcpo. Indeed, the set $\mathcal{D}_{\leq
1}^{\infty}(X)$ is known to be a dcpo when equipped with the pointwise order
[16]:

$\varphi\leq\psi\iff\forall x.\varphi(x)\leq\psi(x)$

In fact, one can observe that the coproduct functor $+:\mathbb{L}_{(\leq
1)}\times\mathbb{L}_{(\leq 1)}\to\mathbb{L}_{(\leq 1)}$ is a
$\mathbf{Dcpo}_{\perp!}$-enriched functor, turning the category
$\mathbb{L}_{\leq 1}$ into a small symmetric monoidal
$\mathbf{Dcpo}_{\perp!}$-enriched category $(\mathbb{L}_{\leq 1},+,0)$.

It turns out that Kegelspitzen are models of this Lawvere theory
$\mathbb{L}_{\leq 1}$, as explained in the following theorem. In essence, this
theorem represents Kegelspitzen as domain-theoretic stochastic matrices.

######  Theorem 2.3.

The category $\mathbf{KS}$ of Kegelspitzen and affine Scott-continuous maps is
equivalent to the category $[\mathbb{L}_{\leq
1},\mathbf{Dcpo}_{\perp!}]_{\times}$ of models of the
$\mathbf{Dcpo}_{\perp!}$-enriched Lawvere theory $\mathbb{L}_{\leq 1}$ of
subconvex sets, i.e. the category of finite product-preserving locally strict
Scott-continuous functors $\mathbb{L}_{\leq 1}\to\mathbf{Dcpo}_{\perp!}$ and
natural transformations between them.

###### Proof.

Recall that Kegelspitzen can be equivalently defined as dcpos $X$ with Scott-
continuous maps $X^{n}\to X$ and a product $(x_{i})_{1\leq i\leq n}\in X^{n}$
as the convex sum $\sum_{i}r_{i}\cdot x_{i}\in X$ for $r\in\mathbb{L}_{\leq
1}(n,1))$, one can define a functor $\Phi:\mathbf{KS}\to[\mathbb{L}_{\leq
1},\mathbf{Dcpo}_{\perp!}]_{\times}$ which acts as follows on objects:

$\displaystyle\Phi(X)(n)$ $\displaystyle=X^{n}\quad(n\in\mathbb{N})$
$\displaystyle\Phi(X)(r:n\to 1)((x_{i})_{i})$
$\displaystyle=\sum_{i}r_{i}\cdot x_{i}$

Indeed, any Kegelspitze $X$ can be identified with a (finite) product-
preserving functor $\Phi(X):\mathbb{L}_{\leq 1}\to\mathbf{Dcpo}_{\perp!}$,
i.e. a model of the Lawvere theory $\mathbb{L}$ in the category
$\mathbf{Dcpo}_{\perp!}$, defined as follows. For $n\in\mathbb{N}$,
$\Phi(X)(n)=X^{n}\in\mathbf{Dcpo}_{\perp!}$.

A function $r:n\to 1$ is a $n$-ary operation definable in the Lawvere theory
$\mathbb{L}_{\leq 1}$ of subconvex sets. and as such it induces a function
$f_{r}:X^{n}\to X$, defined by

$f_{r}(x_{1},\ldots,x_{n})=\sum_{i}r_{i}\cdot x_{i}$

which is Scott-continuous in each argument since $X$ is taken to be a
Kegelspitze. Consequently, the function $f_{r}:X^{n}\to X$ is taken to be
$\Phi(X)(r):\Phi(X)(n)\to\Phi(X)(1)$.

Then the mapping $\Phi$ can be turned into a functor
$\Phi:\mathbf{KS}\to[\mathbb{L}_{\leq 1},\mathbf{Dcpo}_{\perp!}]_{\times}$
which acts as follows on maps: an affine Scott-continuous map $f:X\to Y$ is
associated to a natural family of strict Scott-continuous maps
$\Phi(f):\Phi(X)\Rightarrow\Phi(Y)$, where $\Phi(f)_{n}:X^{n}\to Y^{n}$ is the
strict Scott-continuous map

$f^{n}:(x_{i})_{1\leq i\leq n}\mapsto(f(x_{i}))_{1\leq i\leq n}$

for every $n\in\mathbb{N}$.

The faithfulness of the functor $\Phi$ is entailed by its construction:

$\forall f,g\in\mathbf{KS}(X,Y).(\Phi(f)=\Phi(g)\implies
f=\Phi(f)_{1}=\Phi(g)_{1}=g)$

Additionally, we are required to prove that the functor $\Phi$ is full.
Consider a natural transformation $\alpha:\Phi(X)\Rightarrow\Phi(Y)$ for some
Kegelspitzen $X$ and $Y$. In what follows we show that there is an affine
strict Scott-continuous map $f$ such that $\alpha=\Phi(f)$.

By construction, the strict Scott-continuous map
$f\stackrel{{\scriptstyle\text{def}}}{{=}}\alpha_{1}:X\to Y$ induces the whole
natural transformation $\alpha$, i.e. $\alpha_{n}=f^{n}$ for every
$n\in\mathbb{N}$. Indeed, from the commuting square

$\textstyle{n\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta_{i}}$$\textstyle{X^{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{n}}$$\scriptstyle{\Phi(X)(\delta_{i})}$$\textstyle{Y^{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Phi(Y)(\delta_{i})}$$\textstyle{1}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{Y}$

where $1\leq i\leq n$ and $\delta_{i}$ is the Dirac notation introduced in
Definition 2.1, we deduce that for every $1\leq i\leq n$ and for
$x=(x_{1},\ldots,x_{n})\in X^{n}$,

$f(x_{i})=f(\Phi(X)(\delta_{i})(x))=\Phi(Y)(\delta_{i})(\alpha_{n}(x))=(\alpha_{n}(x))_{i}$

Moreover, the strict Scott-continuous map $\alpha_{1}:X\to Y$ is affine, i.e.
is a morphism in $\mathbf{KS}$: this is entailed by the commuting square

$\textstyle{n\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r}$$\textstyle{X^{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{n}}$$\scriptstyle{\Phi(X)(r)}$$\textstyle{Y_{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Phi(Y)(r)}$$\textstyle{1}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{1}}$$\textstyle{Y}$

where $r\in\mathbb{L}_{\leq 1}(n,1))$, which means that

$\forall x=(x_{1},\ldots,x_{n})\in X^{n}.\alpha_{1}(\sum_{i}r_{i}\cdot
x_{i})=\sum_{i}r_{i}\cdot(\alpha_{n}(x))_{i}$

i.e.

$\forall x=(x_{1},\ldots,x_{n})\in X^{n}.\alpha_{1}(\sum_{i}r_{i}\cdot
x_{i})=\sum_{i}r_{i}\cdot\alpha_{1}(x_{i})$

This concludes our proof that the functor $\Phi$ is full, since
$\alpha_{n}=f^{n}=\Phi(f)(n)$ for every $n\in\mathbb{N}$, and therefore
$\alpha=\Phi(f)$. The full and faithful functor $\Phi$ turns out to be
essentially surjective, and therefore an equivalence: a model
$F:\mathbb{L}_{\leq 1}\to\mathbf{Dcpo}_{\perp!}$ is equivalent to the model
$\Phi(X)$, where $X$ is the Kegelspitze formed by the dcpo $F(1)$ together
with the Scott-continuous convex structure $F(\mathbb{L}(n,1))$.

∎

It is worth noting that using a similar reasoning, one can show that the
category $\mathbf{Conv}$ of convex sets and affine maps is equivalent to the
category $[\mathbb{L},\mathbf{Set}]_{\times}$ of models of the Lawvere theory
$\mathbb{L}$ of convex sets, and that the category $\mathbf{dConv}$ of convex
dcpos and Scott-continuous affine maps is equivalent to the category
$[\mathbb{L},\mathbf{Dcpo}]_{\times}$ of models of the Lawvere theory
$\mathbb{L}$ of convex sets in the category $\mathbf{Dcpo}$ of dcpos and
Scott-continuous maps. Those observations along with Theorem 2.3 can be seen
as instances of the standard result (see e.g. [18]) that the Eilenberg Moore
category $\mathcal{EM}(T)$ of a monad $T$ is equivalent to the category
$[\text{Kl}_{\mathbb{N}}(T)^{\mathbf{op}},\mathbf{Set}]_{\times}$, since we
have the following chain of equivalences

${\mathbf{Conv}_{\leq 1}}\cong\mathcal{EM}(\mathcal{D}_{\leq
1}^{\infty})\cong[\text{Kl}_{\mathbb{N}}(\mathcal{D}_{\leq
1}^{\infty})^{\mathbf{op}},\mathbf{Set}]_{\times}\cong[\mathbb{L}_{,}\mathbf{Set}]_{\times}$

Cones also have their order-theoretic counterpart.

######  Definition 2.4.

An ordered cone $C$ is a cone equipped with a partial order $\leq$ such that
addition and scalar multiplication are monotone. That is, $a\leq b$ implies
that $a+c\leq b+c$ and $r\cdot a\leq r\cdot b$, for every $a,b,c\in C$ and
every $r\in\mathbb{R}^{+}$. An ordered cone $A$ is a d-cone (resp. a b-cone)
when its order is directed-complete (resp. bounded directed-complete), and its
addition $+:A\times A\to A$ and its scalar multiplication $\cdot:[0,1]\times
A\to A$ are Scott-continuous maps. We refer the interested reader to [23] for
a thorough study of those domain-theoretic structures.

These definitions give rise to the categories $\mathbf{dCone}$ and
$\mathbf{bCone}$ of d-cones and b-cones respectively, with Scott-continuous
maps. In this setting, the Lawvere theory of cones $\mathbb{L}_{\text{Cone}}$
is defined with the multiset monad $\mathcal{M}$ on the semiring
$\mathbb{R}^{+}$ which acts as follows on objects

$\mathcal{M}(X)=\left\\{~{}\varphi:X\to\mathbb{R}^{+}~{}\middle|~{}\text{supp}(\varphi)\text{
finite}~{}\right\\}\qquad\text{ where
}\quad\text{supp}(\varphi)=\left\\{~{}x\in X~{}\middle|~{}\varphi(x)\neq
0~{}\right\\}$

In other words, the Lawvere theory of cones $\mathbb{L}_{\text{Cone}}$ is the
category of natural numbers together with functions $n\to m$ seen as Kleisli
maps $m\to\mathcal{M}(n)$, i.e. $\mathbb{L}_{\text{Cone}}$ is the opposite
category $\text{Kl}_{\mathbb{N}}(\mathcal{M})^{\mathbf{op}}$ of the restricted
Kleisli category of the multiset monad $\mathcal{M}$. Replaying every step of
our reasoning with the multiset monad instead of the distribution monad leaves
us with the following equivalences:

$\mathbf{dCone}\cong[\mathbb{L}_{\text{Cone}},\mathbf{Dcpo}]_{\times}\qquad\qquad\mathbf{bCone}\cong[\mathbb{L}_{\text{Cone}},\mathbf{BDcpo}]_{\times}$

In other words, d-cones are models of the Lawvere theory of cones in the
category of dcpos and Scott-continuous maps, while b-cones are models of the
Lawvere theory of cones in the category of bdcpos and Scott-continuous maps.

Last but not least: the isomorphism between the categories $\mathbf{KS}$ and
$[\mathbb{L}_{\leq 1},\mathbf{Dcpo}_{\perp!}]_{\times}$ establish a formal
relation between the category $\mathbf{KS}$ and the category
$\mathbf{Dcpo}_{\perp!}$, which is known to be symmetric monoidal closed when
equipped with the smash product $\otimes_{\perp}$, with its internal hom
$\mathbf{KS}(-,-)$ as exponential (see e.g. [22, Section 1.3]).

######  Proposition 2.5.

The category $\mathbf{KS}$ is monoidal closed with respect to the smash
product $\otimes_{\perp}$ and the internal hom functor $\mathbf{KS}(-,-)$

###### Proof.

As the smash product of two pointed (convex) dcpos, the smash product of two
Kegelspitzen is a pointed convex dcpo whose convex structure is defined
componentwise.

Now, we observe that for every pair $(X,Y)$ of Kegelspitzen, the set
$\mathbf{KS}(X,Y)$ is convex when equipped with a convex structure defined
pointwise on the convex structure of the Kegelspitze $Y$. The least upper
bound $\bigvee_{i}f_{i}$ of a directed set $\\{f_{i}\\}_{i\in I}$ of strict
Scott-continuous functions between Kegelspitzen is also strict Scott-
continuous. It remains to show that when every $f_{i}$ ($i\in I$) is affine,
so does $\bigvee_{i}f_{i}$ since $Y$ is a Kegelspitzen and therefore
$\theta_{n,Y}:S_{n}\times Y\to Y$ is affine in both coordinates:

$\displaystyle(\bigvee_{i}f_{i})(\sum_{1\leq j\leq n}r_{j}\cdot x_{j})$
$\displaystyle=\bigvee_{i}(f_{i}(\sum_{j}r_{j}\cdot x_{j}))$
$\displaystyle=\bigvee_{i}(\sum r_{j}\cdot f_{i}(x_{j})))$
$\displaystyle=\bigvee_{i}(\theta_{n,Y}((r_{j})_{j\leq
n},(f_{i}(x_{j}))_{j\leq n})$ $\displaystyle=(\theta_{n,X}((r_{j})_{j\leq
n},(\bigvee_{i}(f_{i}(x_{j})))_{j\leq n})$
$\displaystyle=\sum_{j}r_{j}\cdot(\bigvee_{i}f_{i})(x_{j})$

for every convex sum $\sum_{1\leq j\leq n}r_{j}\cdot x_{j}$ in the Kegelspitze
$X$.

Therefore, $\mathbf{KS}(X,Y)$ is a pointed convex dcpo, which satisfies the
Kegelspitzen condition since $Y$ does:

$\displaystyle\forall\lambda\in[0,1].\forall x\in
X.\quad(\lambda\cdot(\bigvee_{i}f_{i}))(x)$
$\displaystyle=\lambda\cdot((\bigvee_{i}f_{i})(x))=\lambda\cdot(\bigvee_{i}f_{i}(x))$
$\displaystyle=\bigvee_{i}\lambda\cdot f_{i}(x)=\bigvee_{i}(\lambda\cdot
f_{i})(x)$ $\displaystyle=(\bigvee_{i}(\lambda\cdot f_{i}))(x)$

Moreover, the strict Scott-continuous evaluation map
$\text{ev}_{X,Y}:\mathbf{KS}(X,Y)\otimes_{\perp}X\to Y$, given by the monoidal
closed structure of $\mathbf{Dcpo}_{\perp!}$ [22, Section 1.3], is affine:

$\text{ev}_{X,Y}(\sum_{i}r_{i}\cdot f_{i},x)=(\sum_{i}r_{i}\cdot
f_{i})(x)=\sum_{i}r_{i}\cdot(f_{i}(x))=\sum_{i}r_{i}\cdot(\text{ev}_{X,Y}(f_{i},x))$

for every convex sum $\sum_{1\leq i\leq n}r_{i}\cdot f_{i}$ in the Kegelspitze
$\mathbf{KS}(X,Y)$. Similarly,

$\text{ev}_{X,Y}(f,\sum_{i}r_{i}\cdot x_{i})=f(\sum_{i}r_{i}\cdot
x_{i})=\sum_{i}r_{i}\cdot f(x_{i})=\sum_{i}r_{i}\cdot\text{ev}_{X,Y}(f,x_{i})$

for every convex sum $\sum_{1\leq i\leq n}r_{i}\cdot f_{i}$ in the Kegelspitze
$X$.

Finally, the curryfied form $\Lambda(f):X\to\mathbf{KS}(Y,Z):x\mapsto f(x,-)$
of an affine strict Scott-continuous map $f:X\otimes_{\perp}Y\to Z$ is also
strict Scott-continuous [22, Section 1.3] and affine, since one can verify
that for every convex sum $\sum_{i}r_{i}\cdot x_{i}\in X$ and every $y\in Y$,

$\Lambda(f)(\sum_{i}r_{i}\cdot
x_{i})(y)=\sum_{i}r_{i}\cdot\Lambda(f)(x_{i})(y)$

This concludes our proof that we have, for every triplet $(X,Y,Z)$ of
Kegelspitzen, the following bijective correspondence in $\mathbf{KS}$:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
10.81674pt\hbox{$\displaystyle\penalty 1\qquad f:X\otimes_{\perp}Y\to
Z\qquad$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to125.3333pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\qquad\Lambda(f):X\to\mathbf{KS}(Y,Z)\qquad$}}}}$

for which the equation
$\text{ev}_{X,Y}\circ(\Lambda(f)\otimes_{\perp}\operatorname{id}_{X})=f$
holds. ∎

We now have a monoidal closed structure on the category $\mathbf{KS}$ of
Kegelspitzen and affine Scott-continuous maps. From the observation that every
full subcategory of the cartesian closed category $\mathbf{Dcpo}$ which
contains the singleton dcpo, the cartesian product $\times$ and the
exponential
$\multimap\stackrel{{\scriptstyle\text{def}}}{{=}}\mathbf{Dcpo}(-,-)$ is
itself cartesian closed [22], we obtain the following proposition.

######  Proposition 2.6.

The category $\mathbf{KS}_{\text{Scott}}$ of Kegelspitzen and Scott-continuous
maps is cartesian closed.

Note that in the category $\mathbf{KS}_{\text{Scott}}$, maps between
Kegelspitzen are not necessarily affine, and in particular do not necessarily
preserve least elements.

##  3\. Interpreting pPCF

In this section, we consider a probabilistic extension of PCF [26], named
pPCF222The presentation of this language essentially follows the work of
Ehrhard et al., see e.g. [8], whose types and terms are defined as follows:

$\displaystyle\text{Types: }t,u,\ldots$ $\displaystyle::=\text{nat}\mid
t\multimap u$ $\displaystyle\text{Terms: }M,N,\ldots$
$\displaystyle::=\underline{n}\mid x\mid\text{succ}(M)\mid\text{if}(M,P,z\cdot
Q)\mid\lambda x^{t}.M\mid(M)N\mid\text{coin}(\kappa)\mid\text{fix}(M)$

where $n\in\mathbb{N}$, $x,y,\ldots$ are symbols for variables and
$\kappa\in[0,1]\cap\mathbb{Q}$ is a probability. We associate those grammars
to the following typing rules.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.28452pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=56.56903pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma,x:t\vdash x:t$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
7.26117pt\hbox{$\displaystyle\penalty 1\Gamma,x:t\vdash M:u$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=78.28122pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda x^{t}.M:t\multimap
u$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash M:t\multimap
u\quad\Gamma\vdash N:t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=112.02953pt\hbox{}}}\hbox{\kern
26.18037pt\hbox{$\displaystyle\Gamma\vdash(M)N:u$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Gamma\vdash M:t\multimap t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=60.9302pt\hbox{}}}\hbox{\kern
2.08322pt\hbox{$\displaystyle\Gamma\vdash\text{fix}(M):t$}}}}$
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.68056pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.36111pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\underline{n}:\text{nat}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
11.69449pt\hbox{$\displaystyle\penalty 1\Gamma\vdash M:\text{nat}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=72.09717pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\text{succ}(M):\text{nat}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.90283pt\hbox{$\displaystyle\penalty 1\kappa\in[0,1]\cap\mathbb{Q}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=66.45602pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\text{coin}(\kappa):\text{nat}$}}}}$
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
M:\text{nat}\quad\Gamma\vdash P:t\quad\Gamma,z:\text{nat}\vdash Q:t$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=169.79042pt\hbox{}}}\hbox{\kern
41.52763pt\hbox{$\displaystyle\Gamma\vdash\text{if}(M,P,z\cdot Q):t$}}}}$

The associated reduction transition is probabilistic: terms
$\text{coin}(\kappa)$ reduce to $\underline{0}$ with probability $\kappa$ and
to $\underline{1}$ with probability $1-\kappa$. This construction is
associated to the following reduction rules.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
23.5394pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=47.0788pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{coin}(\kappa)\xrightarrow{\kappa}\underline{0}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
27.70607pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.41214pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{coin}(\kappa)\xrightarrow{1-\kappa}\underline{1}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.58684pt\hbox{$\displaystyle\penalty 1M\xrightarrow{\kappa}N$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.8519pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle(M)P\xrightarrow{\kappa}(N)P$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
26.1667pt\hbox{$\displaystyle\penalty 1M\xrightarrow{\kappa}N$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=83.01163pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{succ}(M)\xrightarrow{\kappa}\text{succ}(N)$}}}}$

We write $\to_{d}$ for deterministic reductions, i.e. probabilistic reductions
$\xrightarrow{\kappa}$ with $\kappa=1$. The deterministic reduction $\to_{d}$
allows us to reuse standard reduction rules, that is:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1M\to_{d}N$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=30.60907pt\hbox{}}}\hbox{\kern
0.3462pt\hbox{$\displaystyle M\xrightarrow{1}N$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
46.57253pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=93.14505pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle(\lambda x^{t}.M)N\to_{d}M[x\mapsto
N]$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 44.31157pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=88.62314pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{fix}(M)\to_{d}(M)\text{fix}(M)$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
23.42958pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=46.85916pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{succ}(\underline{n})\to_{d}\underline{n+1}$}}}}$

Let us focus on the probabilistic extension considered in this language. We
amend the traditional if-then-else instruction $\text{if}(M,P,Q)$ in order to
prevent the loss of the value $\underline{n}$ obtained from the evaluation of
the term $M$: when $M$ reduces to $\underline{0}$, one can evaluate $P$
knowing that $n=0$ but when $M$ reduces to $\underline{n+1}$
$(n\in\mathbb{N})$, it is necessary to associate a variable $z=\underline{n}$
in order for the term $Q$ to reuse the value of $n$. This leads to conditional
constructions $\text{if}(M,P,z\cdot Q)$ associated to the following reduction
rules which adopt a call-by-value strategy on the ground type nat, in the
sense that the term $M:\text{nat}$ is evaluated first, and the resulting value
is used for conditional branching.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
36.45868pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=72.91736pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{if}(\underline{0},P,z\cdot
Q)\to_{d}P$}}}}\qquad\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 45.71875pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=91.4375pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{if}(\underline{n+1},P,z\cdot
Q)\to_{d}Q[z\mapsto\underline{n}]$}}}}$ ${tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 48.86032pt\hbox{$\displaystyle\penalty
1M\xrightarrow{\kappa}N$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=128.39886pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{if}(M,P,z\cdot
Q)\xrightarrow{\kappa}\text{if}(N,P,z\cdot Q)$}}}}$

By construction, for every judgement $\Gamma\vdash M:t$, the judgement
$\Gamma\vdash M^{\prime}:t$ holds whenever $M\xrightarrow{\kappa}M^{\prime}$
holds.

######  Lemma 3.1 (Substitution Lemma).

Suppose that $\Gamma,x:u\vdash M:t$ and $\Gamma\vdash P:u$.
If $M\to_{d}M^{\prime}$ then $M[x\mapsto P]\to_{d}M^{\prime}[x\mapsto P]$.

###### Proof.

This lemma can be proven by induction on terms. Terms which apply a term to
another are the non-trivial cases of this proof.

Consider a term $M=(N)L$, when $N$ isn’t an abstraction and reduces to another
term $N^{\prime}$. Then, the reduction $N\to_{d}N^{\prime}$ implies that there
is a reduction

$M=(N)L\to_{d}(N^{\prime})L$

and since $M\to_{d}M^{\prime}$ by hypothesis, we have that
$M^{\prime}=(N^{\prime})L$.

First, let us observe that $N$ cannot be a variable since
$N\to_{d}N^{\prime}$. Now, assuming that $\Gamma\vdash P:u$, one can deduce
that $N[x\mapsto P]$ is not an abstraction since $N$ isn’t, and finally by
induction hypothesis, $N[x\mapsto P]\to_{d}N^{\prime}[x\mapsto P]$ and
therefore:

$((N)L)[x\mapsto P]=(N[x\mapsto P])L[x\mapsto P]\to_{d}(N^{\prime}[x\mapsto
P])L[x\mapsto P]=((N^{\prime})L)[x\mapsto P]$

∎

This extension of PCF allows to define the predecessor of a term $M$ by:

$\text{pred}(M)\stackrel{{\scriptstyle\text{def}}}{{=}}\lambda
x^{\text{nat}}.~{}\text{if}(x,0,z\cdot z)$

Moreover, probabilistic combinations of terms $M:t$ and $N:t$ under the
probability $\kappa$ are given by the term:

$M\oplus_{\kappa}N\stackrel{{\scriptstyle\text{def}}}{{=}}\text{if}(\text{coin}(\kappa),M,N)$

The language allows a manipulation of (first-order) probabilistic data (of
type nat) through a let construction which corresponds to a probabilistic
programming perspective to sampling:

$\text{let}\,x=M\,\text{in}\,N\stackrel{{\scriptstyle\text{def}}}{{=}}\text{if}(M,N[x\mapsto\underline{0}],z\cdot
N[x\mapsto\text{succ}(z)])$

It is possible to give an interpretation to this language in the cartesian
closed category $\mathbf{KS}_{\text{Scott}}$ of Kegelspitzen and Scott-
continuous maps. In short, types $t$ can be interpreted as Kegelspitzen
$[\\![t]\\!]$, contexts $\Gamma=(x_{1}:t_{1},\ldots,x_{n}:l_{n})$ as
Kegelspitzen $[\\![t_{1}]\\!]\otimes\cdots\otimes[\\![t_{n}]\\!]$, and terms
$\Gamma\vdash M:t$ as Scott-continuous maps $[\\![\Gamma\vdash
M:t]\\!]:[\\![\Gamma]\\!]\to[\\![t]\\!]$, with the following denotations:

$[\\![{\rm Nature}]\\!]=\mathcal{D}_{\leq 1}(\mathbb{N})\qquad\text{ and
}\qquad[\\![t\multimap
u]\\!]=[\\![t]\\!]\multimap[\\![u]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}\mathbf{Dcpo}([\\![t]\\!],[\\![u]\\!])$

In what follows, functions $\varphi:\mathbb{N}\to[0,1]$ in $\mathcal{D}_{\leq
1}^{\infty}(\mathbb{N})$ are written as sequences
$(\varphi(n))_{n\in\mathbb{N}}$. In particular, since closed terms $\vdash
M:\text{nat}$ are interpreted by functions $[\\![\vdash
M:\text{nat}]\\!]:\mathbb{N}\to[0,1]$ in $\mathcal{D}_{\leq
1}^{\infty}(\mathbb{N})$, we write $[\\![M:\text{nat}]\\!]_{n}$ for
$[\\![\vdash M:\text{nat}]\\!](n)$.

$[\\![\Gamma\vdash
x_{i}:t_{i}]\\!]=\pi_{i}:\rho\mapsto\rho_{i}\qquad[\\![\Gamma\vdash\underline{0}:\text{nat}]\\!](\rho)=(1,0,\cdots)$
$[\\![\Gamma\vdash\text{coin}(\kappa):\text{nat}]\\!](\rho)=\kappa\cdot[\\![\Gamma\vdash\underline{0}]\\!](\rho)+(1-\kappa)\cdot[\\![\Gamma\vdash\underline{1}]\\!](\rho)$
$[\\![\Gamma\vdash\text{succ}(M):\text{nat}]\\!](\rho)=(0,u_{0},u_{1},\cdots)\qquad\text{where
}u=[\\![\Gamma\vdash M:\text{nat}]\\!](\rho)$
$[\\![\Gamma\vdash\textbf{if}(M,P,z\cdot Q):t]\\!](\rho)=v_{0}u+(\sum_{i\geq
1}v_{i})u^{\prime}$ $\text{ where }v=[\\![\Gamma\vdash M:{\rm
Nature}]\\!](\rho)\text{, }u=[\\![\Gamma\vdash P:t]\\!](\rho),\text{ and
}u^{\prime}=[\\![\Gamma,z:\text{nat}\vdash Q:t]\\!](\rho,v)$
$[\\![\Gamma\vdash\text{fix}(M):t]\\!](\rho)=\textbf{fix}([\\![\Gamma\vdash
M:t\multimap t]\\!](\rho))\text{ where
}\textbf{fix}(f)=\bigvee_{n}f^{n}(\perp)$
$[\\![\Gamma\vdash(M)N:t]\\!](\rho)=f(x)\text{ where }f=[\\![\Gamma\vdash
M:u\multimap t]\\!](\rho)\text{, }x=[\\![\Gamma\vdash N:u]\\!](\rho)$
$[\\![\Gamma\vdash\lambda x^{u}.M:u\multimap
t]\\!](\rho)(x)=[\\![\Gamma,x:u\vdash M:t]\\!](\rho,x)$

One of the interesting properties of this denotational semantics is that the
interpretation of a term can be expressed as a sum of the interpretations of
the terms it reduces to.

######  Lemma 3.2 (Invariance of the interpretation).

Suppose that the judgement $\Gamma\vdash M:t$ holds, for some term $M$ which
isn’t a value. Then, the following equality holds

$[\\![\Gamma\vdash
M:t]\\!]=\sum_{M\xrightarrow{\kappa}M^{\prime}}\kappa\cdot[\\![\Gamma\vdash
M^{\prime}:t]\\!]$

###### Proof.

We first consider the case of judgements $\Gamma\vdash M:t$ such that the term
$M$ reduce through the deterministic reduction rules: if $M\to_{d}M^{\prime}$,
then the interpretations of the terms that we have just defined ensures that
$[\\![\Gamma\vdash M]\\!]=[\\![\Gamma\vdash M^{\prime}]\\!]$. For example, for
the judgement $\Gamma\vdash(\lambda x^{t}.M)N:u$ (with $x:t$ and $N:t$) such
that $(\lambda x^{t}.M)N\to_{d}M[x\mapsto N]$, we have

$[\\![\Gamma\vdash(\lambda x^{t}.M)N:u]\\!](\rho)=[\\![\Gamma,x:t\vdash
N:u]\\!](\rho,[\\![\Gamma\vdash N:t]\\!](\rho))=[\\![\Gamma\vdash M[x\mapsto
N]]\\!](\rho)$

It remains to show that the terms which reduce through probabilistic reduction
rules (with $\kappa<1$) satisfy the invariance property. By the construction
of our reduction system, such terms are of the form $\text{coin}(\kappa)$,
$(M)P$ or $\text{succ}(M)$. We now show that the invariance property is
satisfied in those three cases.

First, let us observe that the interpretation of
$\text{coin}(\kappa):\text{nat}$ under any context $\Gamma$ can be re-written
as follows:

$[\\![\Gamma\vdash\text{coin}(\kappa):\text{nat}]\\!](\rho)=\sum_{M\xrightarrow{\kappa}\underline{n}}\kappa\cdot[\\![\Gamma\vdash\underline{n}:{\rm
Nature}]\\!]$

For the remaining two cases, we proceed by induction on judgements. Consider
terms $\text{succ}(M):\text{nat}$ (where $M\neq\underline{n}$ for some
$n\in\mathbb{N}$) and $(N)P:t$ (with $P:u$) such that the judgements
$\Gamma\vdash M:\text{nat}$ and $\Gamma\vdash N:u\multimap t$ satisfy the
invariance property. From our operational semantics, we deduce that if
$\text{succ}(M)\xrightarrow{\kappa}Q$, then $Q$ is of the form
$\text{succ}(M^{\prime})$ for some term $M^{\prime}:\text{nat}$ such that
$M\xrightarrow{\kappa}M^{\prime}$. Similarly, if $(N)P\xrightarrow{\kappa}Q$
then $Q$ is of the form $(N^{\prime})P$ for some term $N^{\prime}:u\multimap
t$ such that $N\xrightarrow{\kappa}N^{\prime}$. And since by induction
hypothesis, we have

$[\\![\Gamma\vdash
M]\\!]=\sum_{M\xrightarrow{\kappa}M^{\prime}}[\\![\Gamma\vdash
M^{\prime}:\text{nat}]\\!]\qquad\text{ and }\qquad[\\![\Gamma\vdash
N]\\!]=\sum_{N\xrightarrow{\kappa}N^{\prime}}[\\![\Gamma\vdash
N^{\prime}:u\multimap t]\\!]$

then we have by the construction of our denotational semantics the following
equalities:

$[\\![\Gamma\vdash\text{succ}(M)]\\!]=\sum_{\text{succ}(M)\xrightarrow{\kappa}\text{succ}(M^{\prime})}[\\![\Gamma\vdash\text{succ}(M^{\prime}):\text{nat}]\\!]=\sum_{\text{succ}(M)\xrightarrow{\kappa}Q}[\\![\Gamma\vdash
Q:\text{nat}]\\!]$
$[\\![\Gamma\vdash(N)P:t]\\!]=\sum_{(N)P\xrightarrow{\kappa}(N^{\prime})P}[\\![\Gamma\vdash(N^{\prime})P:t]\\!]=\sum_{(N)P\xrightarrow{\kappa}Q}[\\![\Gamma\vdash
Q:t]\\!]$

∎

In line with similar approaches [6, 10], the probabilities of the transitions
of pPCF terms can be organised as follows (see [8, Sec. 1.2]).

######  Definition 3.3 ([8], Section 1.2).

In what follows, we write $\Lambda$ for the set of all pPCF terms and we say
that a term $M$ is _weak-normal_ when there is no probabilistic reduction
$M\xrightarrow{\kappa}M^{\prime}$. The _matrix of pPCF terms_ is the
stochastic matrix $\textbf{Prob}\in[0,1]^{\Lambda\times\Lambda}$ defined by

$\textbf{Prob}_{M,M^{\prime}}=\begin{cases}\kappa\text{ if
}M\xrightarrow{\kappa}M^{\prime}\\\ 1\text{ if }M=M^{\prime}\text{ is weak-
normal}\\\ 0\text{ otherwise}\end{cases}$

Using Definition 3.3, we formulate the following soundness property which is a
restatement of Lemma 3.2, which established the invariance of interpretation.
In this context,

######  Proposition 3.4 (Soundness).

Suppose that the judgement $\Gamma\vdash M:t$ holds, for some term $M$ which
isn’t a value. Then, the following equality holds

$[\\![\Gamma\vdash M:t]\\!]=\sum_{M^{\prime}\text{
term}}\textbf{Prob}_{M,M^{\prime}}\cdot[\\![\Gamma\vdash M^{\prime}:t]\\!]$

By applying repeatedly this lemma and considering the specific case of normal
forms, one obtains the following corollary.

######  Corollary 3.5.

Consider a closed type $\vdash t$.
For $\Gamma\vdash M:t$ and $k\in\mathbb{N}$, the following equality holds

$[\\![\Gamma\vdash M:t]\\!]=\sum_{M^{\prime}\text{
term}}\textbf{Prob}^{k}_{M,M^{\prime}}[\\![\Gamma\vdash M^{\prime}:t]\\!].$

where $\textbf{Prob}^{k}_{M,M^{\prime}}$ is the probability that the term $M$
reduces to the term $M^{\prime}$ in $k$ steps.

Then for every closed term $\vdash M:\text{nat}$, we have the inequality

$[\\![M:\text{nat}]\\!]_{n}\geq\textbf{Prob}^{\infty}_{M,\underline{n}}\text{
where
}\textbf{Prob}^{\infty}_{M,\underline{n}}\stackrel{{\scriptstyle\text{def}}}{{=}}\sup_{k}~{}(\textbf{Prob}^{k}_{M,\underline{n}})$

i.e. where $\textbf{Prob}^{\infty}_{M,\underline{n}}$ is the least upper bound
of the probabilities that $M$ reduced to $\underline{n}$ in finitely many
steps.

###### Proof.

Applying Proposition 3.4, we have:

$[\\![M:\text{nat}]\\!]_{n}=\sum_{M^{\prime}:\text{nat}}\textbf{Prob}_{M,M^{\prime}}\cdot[\\![M^{\prime}:\text{nat}]\\!]_{n}\geq\textbf{Prob}^{\infty}_{M,\underline{n}}\cdot[\\![\underline{n}]\\!]_{n}=\textbf{Prob}^{\infty}_{M,\underline{n}}\cdot
1=\textbf{Prob}^{\infty}_{M,\underline{n}}$

∎

##  4\. Computational adequacy

In this section, we provide a computational adequacy result (for the type
nat), that is we prove the converse of the inequality expressed in Corollary
3.5, which is:

$\forall\vdash
M:\text{nat},\quad[\\![M:\text{nat}]\\!]_{n}\leq\textbf{Prob}^{\infty}_{M,\underline{n}}$

The key to the proof of this inequality is to define a logical relation, taken
from [6] but inspired by the original article on the semantics of PCF [26].

######  Definition 4.1.

For every type $t$, consider the relation
$\triangleleft_{t}\subseteq[\\![t]\\!]\times\Lambda_{t}$ between the
denotation $[\\![t]\\!]$ and the set $\Lambda_{t}$ of all closed terms of type
$t$, written with an infix notation and defined by induction as follows:

$x=(x_{n})_{n\in\mathbb{N}}\triangleleft_{{\rm Nature}}M\equiv\forall
n.x_{n}\leq\textbf{Prob}^{\infty}_{M,\underline{n}}$
$f\triangleleft_{u\multimap t}M\equiv\forall x.\forall\vdash
P:u.(x\triangleleft_{u}P\implies f(x)\triangleleft_{t}(M)P)$

Note that once again, we follow the convention of presenting elements of
$\mathcal{D}_{\leq 1}^{\infty}(\mathbb{N})$ as sequences
$(x_{n})_{n\in\mathbb{N}}$.

This logical relation has the following closure properties.

######  Lemma 4.2 (Closure properties of the logical relation).

Consider $\vdash M:t$

  1. (1)

If $\vdash M:t$ and $M\to_{d}M^{\prime}$, then $x\triangleleft_{t}M$ holds if
and only if $x\triangleleft_{t}M^{\prime}$ holds;

  2. (2)

$0\triangleleft_{t}M$ holds;

  3. (3)

$\sup_{n}x_{n}\triangleleft_{t}M$ holds for every increasing sequence
$(x_{n})_{n}$ in $[\\![t]\\!]$ such that $x_{n}\triangleleft_{t}M$ for
$n\in\mathbb{N}$;

  4. (4)

$x_{0}\cdot y+(\sum_{i}x_{i+1})\cdot
z\triangleleft_{\text{nat}}\textbf{if}(M,P,z\cdot Q)$ holds for
$x,y,z\in[\\![\text{nat}]\\!]$ and $\vdash M:\text{nat},\vdash
P:\text{nat},\vdash Q:\text{nat}$ such that
$x\triangleleft_{\text{nat}}M,y\triangleleft_{\text{nat}}P,z\triangleleft_{\text{nat}}Q$.

###### Proof.

The closure property (2) follows from the fact that probabilities are positive
numbers, while the closure property (3) follows from the fact that Scott-
continuous functions are ordered pointwise.

As for the closure property (4), we first observe that if the term
$\text{if}(M,P,z\cdot Q)$ reduces to $\underline{n}$ for some
$n\in\mathbb{N}$, then either $M$ reduces to $\underline{0}$ and $P$ reduces
to $\underline{n}$, or $M$ reduces to $\underline{n+1}$ (for some
$n\in\mathbb{N}$) and $Q$ reduces to $\underline{n}$. Then, the closure
property (4) is induced by the following equation which is valid for every
$n\in\mathbb{N}$ (see [6, Lemma 38]):

$\textbf{Prob}^{\infty}_{\text{if}(M,P,z\cdot
Q),\underline{n}}=\textbf{Prob}^{\infty}_{M,\underline{0}}\cdot\textbf{Prob}^{\infty}_{P,\underline{n}}+\sum_{k\geq
0}\textbf{Prob}^{\infty}_{M,\underline{k+1}}\cdot\textbf{Prob}^{\infty}_{Q,\underline{n}}$

Now, we proceed by induction to obtain a proof of the closure property (1).
When $t=\text{nat}$, the property is straightforward from the observation that
$\textbf{Prob}^{k}_{M^{\prime},\underline{n}}=\textbf{Prob}^{k+1}_{M,\underline{n}}$.
Let us now consider the case in which $t=u\multimap v$.

Assume that $f\triangleleft_{t}M$. When $M$ isn’t an abstraction,
$(M)P\to_{d}(M^{\prime})P$ for every closed term $P$ of type $u$, and we can
apply the definition of the logical relation:

$\forall\vdash
P:u,x\in[\\![u]\\!],x\triangleleft_{u}P\xRightarrow{f\triangleleft_{t}M}f(x)\triangleleft_{v}(M)P\xRightarrow{\text{induction
hypothesis}}f(x)\triangleleft_{v}(M^{\prime})P$

When $M$ is an abstraction $\lambda x^{u}.N:v$ with $x:u\vdash N:v$, there is
a term $N^{\prime}$ such that $N\to_{d}N^{\prime}$. Then by the Substitution
Lemma,

$(M)P\to_{d}N[x\mapsto P]\to_{d}N^{\prime}[x\mapsto P]$

and therefore we obtain $f(x)\triangleleft_{v}N^{\prime}[x\mapsto P]$ by
applying the induction hypothesis twice. Hence, since
$(M^{\prime})P\to_{d}N^{\prime}[x\mapsto P]$, we have
$f(x)\triangleleft_{v}M^{\prime}(P)$ by induction, which concludes our proof
that $f\triangleleft_{t}M^{\prime}$.

Conversely, assume $f\triangleleft_{t}M^{\prime}$. We focus on the case in
which $M$ is an abstraction $\lambda x^{u}.N:v$ with $x:u\vdash N:v$ (since
the case in which $M$ isn’t an abstraction is again trivial). Then for every
closed term $\vdash P:u$ and every $x\in[\\![u]\\!]$, we have
$f\triangleleft_{t}\lambda x^{u}.N$ and therefore

$f(x)\triangleleft_{v}(\lambda x.N^{\prime})P\to_{d}N^{\prime}[x\mapsto P]$

therefore $f(x)\triangleleft_{v}N^{\prime}[x\mapsto P]$ (again by the
substitution lemma and the induction hypothesis). Then, we have
$f(x)\triangleleft_{v}N[x\mapsto P]$ and by induction
$f(x)\triangleleft_{v}(M)P=(\lambda x^{u}.N)P$ since $(\lambda
x^{u}.N)P\to_{d}N[x\mapsto P]$. ∎

Using the closure properties of the logical relation, we prove the following
lemma by induction.

######  Lemma 4.3.

Consider a judgment $\Gamma\vdash M:u$ where
$\Gamma\equiv(x_{1}:t_{1},\cdots,x_{n}:t_{n})$.
$[\\![\Gamma\vdash M:u]\\!](\rho)\triangleleft_{u}M[P/x]$ , every family
$P=\\{P_{i}\\}_{1\leq i\leq n}$ of closed terms of type $\\{t_{i}\\}_{1\leq
i\leq n}$ (i.e. $\vdash P_{i}:t_{i}$) and every family $x=\\{x_{i}\\}_{1\leq
i\leq n}$ of variables of type $t=\\{t_{i}\\}_{1\leq i\leq n}$ such that
$[\\![\Gamma\vdash x_{i}:t_{i}]\\!](\rho)\triangleleft_{t_{i}}P_{i}$.

###### Proof.

We will reason by induction on terms.

Case $M=x_{i}$: $[\\![\Gamma\vdash
x_{i}:t_{i}]\\!](\rho)\triangleleft_{t_{i}}P_{i}=x_{i}[P/x]$

Case $M=\underline{l}$: there is only one transition path
$\underline{l}\to\underline{l}$ of probability $1$ and length $0$.

Case $M=\text{succ}(N)$: straightforward induction.

Case $M=\textbf{if}(N,L,R)$: follows from the closure property of the logical
relation for if.

Case $M=\text{coin}(\kappa)$: There is exactly one transition path to
$\underline{0}$ with probability $\kappa$, and one transition path to
$\underline{1}$ with probability $1-\kappa$. It follows that

$\textbf{Prob}^{\infty}_{\text{coin}(\kappa),\underline{0}}=\kappa\text{ and
}\textbf{Prob}^{\infty}_{\text{coin}(\kappa),\underline{1}}=1-\kappa$

We write:

$[\\![\Gamma\vdash\text{coin}(\kappa):\text{nat}]\\!](\rho)=\textbf{Prob}^{\infty}_{\text{coin}(\kappa),\underline{0}}\cdot[\\![\Gamma\vdash\underline{0}:\text{nat}]\\!](\rho)+\textbf{Prob}^{\infty}_{\text{coin}(\kappa),\underline{1}}\cdot[\\![\Gamma\vdash\underline{1}:\text{nat}]\\!](\rho)$

and therefore

$[\\![\Gamma\vdash\text{coin}(\kappa):\text{nat}]\\!](\rho)(n)=\textbf{Prob}^{\infty}_{\text{coin}(\kappa),\underline{n}}$

for every $n\in\mathbb{N}$, i.e.

$[\\![\Gamma\vdash\text{coin}(\kappa):\text{nat}]\\!](\rho)\triangleleft\text{coin}(\kappa)=\text{coin}(\kappa)[x\mapsto
P]$

Case $M=(N)L$: straightforward induction, based on the definition of the
logical relation $\triangleleft_{t\multimap u}$ on the type $t\multimap u$.

Case $M=\lambda y^{t}.N:t\multimap u$: Given any element $y\in[\\![t]\\!]$ and
any closed term $Q$ of type $t$ such that $y\triangleleft_{t}Q$, we have that

$[\\![\Gamma\vdash\lambda y.N]\\!](\rho)=[\\![\Gamma,x:t\vdash
N]\\!](\rho,x)\triangleleft_{u}N[P/x,Q/y]$

by induction hypothesis. Then

$[\\![\Gamma\vdash\lambda x.N]\\!](\rho)(y)\triangleleft_{u}(\lambda
y^{t}.N[P/x])Q$

by the closure property of the logical relation for the deterministic
reduction

$(\lambda y^{t}.N[P/x])Q\to_{d}N[P/x,Q/y]$

Case $M=\textbf{fix}(N)$ with $\Gamma\vdash N:u\multimap u$: the function

$f\stackrel{{\scriptstyle\text{def}}}{{=}}[\\![\Gamma\vdash
N]\\!](\rho):[\\![u]\\!]\to[\\![u]\\!]$

is a Scott-continuous function such that

$[\\![\Gamma\vdash M]\\!](\rho)=\bigvee_{k}f^{k}(\perp)$

Then, by the closure property of the logical relation for fixpoints, it
suffices to prove by induction on $k$ that

$f^{k}(\perp)\triangleleft_{u}\textbf{fix}(N[P/x])$

for every $k\in\mathbb{N}$, knowing that the property already holds for $k=0$.
Suppose that $f^{k}(\perp)\triangleleft_{u}\textbf{fix}(N^{\prime})$, where
$N^{\prime}=N[P/x]$, for some $k\in\mathbb{N}$. By our induction hypothesis
(on terms),

$f\triangleleft_{u\multimap u}N^{\prime}=N[P/x]\qquad\text{ and thus }\qquad
f^{k+1}(\perp)\triangleleft_{u}N^{\prime}\textbf{fix}(N^{\prime})$

Finally, one can conclude that $f^{k+1}(\perp)\triangleleft_{u}N^{\prime}$ by
observing that
$\textbf{fix}(N^{\prime})\to_{d}N^{\prime}\textbf{fix}(N^{\prime})$ and
applying the closure property of the logical relation for deterministic
transitions. ∎

This lemma provides us an adequacy theorem.

######  Theorem 4.4 (Computational adequacy).

For every closed term $M$ of type nat,

$[\\![M:\text{nat}]\\!]_{n}=\textbf{Prob}^{\infty}_{M,\underline{n}}$

###### Proof.

For every closed term $\vdash M:\text{nat}$, we have proven previously that

$[\\![M:\text{nat}]\\!]_{n}\geq\textbf{Prob}^{\infty}_{M,\underline{n}}\qquad\text{
and thus
}\qquad[\\![M:\text{nat}]\\!]_{n}=\textbf{Prob}^{\infty}_{M,\underline{n}}$

since by the adequacy lemma, $[\\![M:\text{nat}]\\!]\triangleleft_{\rm
Nature}M$, i.e. $[\\![M]\\!]_{n}\leq\textbf{Prob}^{\infty}_{M,\underline{n}}$
for every $n\in\mathbb{N}$. ∎

We just provided a computationally adequate model for pPCF, alternative to
probabilistic coherence spaces (see e.g. [10]). Although the type nat has the
same denotation in the two semantics, the denotation as a probabilistic
coherent space (PCS) of the type $t\multimap u$ is a subset of the homset
$\mathbf{Dcpo}([0,1]^{[\\![t]\\!]},[0,1]^{[\\![u]\\!]})$, which only contains
linear maps. Therefore, the resemblance between the two semantical models is
lost at higher types. Although our adequacy theorem is formulated in a similar
fashion as in [10], it is unclear to us whether there exists an interesting
categorical relation between Kegelspitzen and probabilistic coherence spaces.

##  5\. Interpreting recursive types

In this section, we discuss the interpretation of recursive types, taking as a
basis their formalization in the language FPC (see Appendix A). But first, let
us pause for a moment and recall some categorical notions which are essential
in the interpretation of languages such as FPC, which cater for recursive
types.

###  5.1. Involutory category theory

As a preliminary to the description of the denotation of recursive types with
Kegelspitzen, we recall briefly here Fiore’s “Doubling Trick” [11, Section
6.3] (also mentioned in [25, Section 4.2.3]), an universal categorical
construction which allows to turn mixed-variance functors
$\mathbf{C}^{\mathbf{op}}\times\mathbf{C}\to\mathbf{D}$ into covariant
functors
$\mathbf{C}^{\mathbf{op}}\times\mathbf{C}\to\mathbf{D}^{\mathbf{op}}\times\mathbf{D}$.
This property is required because the denotation of recursive types requires
to be able to find fixpoints, not only for covariant (endo)functors but also
for mixed-variance functors. Indeed, the arrow functor
$\cdot\multimap\cdot:\mathbf{KS}^{\mathbf{op}}\times\mathbf{KS}\to\mathbf{KS}$
is a mixed variance functor.

In what follows, the category $|\mathbf{C}|$ is short for
$\mathbf{C}^{\mathbf{op}}\times\mathbf{C}$. Additionally, in categories with
binary products $\otimes$, we write

$f_{1}\stackrel{{\scriptstyle\text{def}}}{{=}}\pi_{1}\circ f:X\to
Y_{1}\qquad\text{ and }\qquad
f_{2}\stackrel{{\scriptstyle\text{def}}}{{=}}\pi_{2}\circ f:X\to Y_{2}$

for the composite of the morphism $f\in\mathbf{C}(X,Y_{1}\otimes Y_{2})$.

######  Definition 5.1 ([12], Definition 4.6).

An _involutory category_ is the pair $(\mathbf{C},\text{Inv}_{C})$ of a
locally small category $\mathbf{C}$ together with an _involution functor_
$\text{Inv}_{C}:\mathbf{C}\to\mathbf{C}^{\mathbf{op}}$, i.e. a functor
$\text{Inv}_{C}:\mathbf{C}\to\mathbf{C}^{\mathbf{op}}$ such that
$(\text{Inv}_{C})^{\mathbf{op}}\circ\text{Inv}_{C}=\mathrm{Id}_{C}$, the
identify functor on the category $\mathbf{C}$.

We write $\mathbf{InvCat}$ for the large cartesian category of involutory
categories and homomorphisms

$F:(\mathbf{C},\text{Inv}_{C})\to(\mathbf{D},\text{Inv}_{D})$

defined as functors $F:\mathbf{C}\to\mathbf{D}$ such that

$F^{\mathbf{op}}\circ\text{Inv}_{C}=\text{Inv}_{D}\circ F$

A canonical example is the pair $(|\mathbf{C}|,\text{Swap}_{C})$ where
$\text{Swap}_{C}\stackrel{{\scriptstyle\text{def}}}{{=}}\langle\Pi_{2},\Pi_{1}\rangle$
(with $\Pi_{1}$, $\Pi_{2}$ projections given by the cartesian structure).

######  Definition 5.2.

A functor $F:|\mathbf{C}|\to|\mathbf{D}|$ is _symmetric_ if
$F:(|\mathbf{C}|,\text{Swap}_{C})\to(|\mathbf{D}|,\text{Swap}_{D})$ is a
morphism in $\mathbf{InvCat}$, i.e.

$F_{1}(f,g)=F_{2}(g,f)\text{ for maps }f\text{ in the category
}\mathbf{C}^{\mathbf{op}}\text{ and }g\text{ in the category }\mathbf{C}$

It turns out that mixed-variance functors induce symmetric functors, and every
symmetric functor arises in that way, following a result due to Fiore in [12,
Section 4.4], re-proven by McCusker in [25, Section 4.2.3].

######  Proposition 5.3.

There is a one-to-one correspondence

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
7.49997pt\hbox{$\displaystyle\penalty 1F:|\mathbf{C}|\to\mathbf{D}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox
to53.79161pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle|F|:|\mathbf{C}|\to|\mathbf{D}|$}}}}$

between mixed variance functors $F:|\mathbf{C}|\to\mathbf{D}$ and symmetric
functors $|F|:|\mathbf{C}|\to|\mathbf{D}|$ defined by

$\displaystyle|F|(A,B)\stackrel{{\scriptstyle\text{def}}}{{=}}(F(B,A),F(A,B))\qquad\qquad|F|(f,g)\stackrel{{\scriptstyle\text{def}}}{{=}}(F(g,f),F(f,g))$

In particular, for every Bénabou cosmos $\mathbf{V}$, the functor $|F|$ is
$\mathbf{V}$-enriched whenever the categories $|\mathbf{C}|$ and $\mathbf{D}$,
and the functor $F$ are $\mathbf{V}$-enriched.

###  5.2. Algebraic compactness of the category of Kegelspitzen

One of the issues with the inclusion of recursive types in a probabilistic
language such as pPCF is that the cardinality of $[\\![t\multimap u]\\!]$
might be strictly larger than that of $[\\![t]\\!]$ in some cases, which might
prevent $[\\![t\to(t\multimap u)]\\!]$ from having a fixpoint. Exploiting the
presentation of the category $\mathbf{KS}$ as a category of models of the
Lawvere theory of subconvex sets, we re-use the notion of algebraic
compactness, which guarantees the existence of such fixpoints.

Recall that a category $\mathbf{C}$ is algebraically compact for a class
$\mathcal{L}$ of endofunctors on $\mathbf{C}$ if every endofunctor $F$ in the
class $\mathcal{L}$ has a canonical fixpoint $\mu F$, which is the initial
$F$-algebra and at the same time the inverse of the final $F$-coalgebra.

Additionally, recall that an endofunctor $F$ on a
$\mathbf{Dcpo}_{\perp!}$-enriched category $\mathbf{C}$ is locally continuous
(resp. locally monotone) if

$F_{X,Y}:\mathbf{C}(X,Y)\to\mathbf{C}(FX,FY)$

is Scott-continuous (resp. monotone).

To obtain the algebraic compactness of $\mathbf{KS}$ for locally continuous
endofunctors, we rely on the following result [12, Example 6.9].

######  Theorem 5.4.

For every small $\mathbf{Dcpo}_{\perp!}$-category $\mathbf{C}$, the
$\mathbf{Dcpo}_{\perp!}$-enriched category of locally strict continuous
functors $\mathbf{C}\to\mathbf{Dcpo}_{\perp!}$ and natural transformations
between them (ordered pointwise) is algebraically compact for the class of
locally continuous endofunctors.

Recall that the Lawvere theory $\mathbb{L}_{\leq 1}$ is a small
$\mathbf{Dcpo}_{\perp!}$-category. Then, the fact that the functor category
$[\mathbb{L}_{\leq 1},\mathbf{Dcpo}_{\perp!}]$ is algebraically compact for
locally continuous endofunctors leads us to the following corollary.

######  Corollary 5.5.

The category $\mathbf{KS}$, as a category equivalent to the category
$[\mathbb{L}_{\leq 1},\mathbf{Dcpo}_{\perp!}]_{\times}$, is algebraically
compact for locally continuous endofunctors.

###### Proof.

First, let us observe that every locally continuous endofunctor $F$ on
$[\mathbb{L}_{\leq 1},\mathbf{Dcpo}_{\perp!}]_{\times}$ extends to a locally
continuous endofunctor $G$ on $[\mathbb{L}_{\leq 1},\mathbf{Dcpo}_{\perp!}]$
defined by $G(X)=F(X)$ when $X:\mathbb{L}_{\leq 1}\to\mathbf{Dcpo}_{\perp!}$
is product-preserving, and $G(X)=X$ otherwise.

Now, consider a chain of embeddings $(D_{n},\alpha_{n}:D_{n}\Rightarrow
D_{n+1})_{n}$ formed of product-preserving functors $\mathbb{L}_{\leq
1}\to\mathbf{Dcpo}_{\perp!}$ and natural families of strict Scott-continuous
maps, where

$D_{0}\stackrel{{\scriptstyle\text{def}}}{{=}}1:\mathbb{L}_{\leq
1}\to\mathbf{Dcpo}_{\perp!}\qquad\text{ and }\qquad
D_{n+1}\stackrel{{\scriptstyle\text{def}}}{{=}}G(D_{n})=F(D_{n})\text{ for
}n\in\mathbb{N}$

By Theorem 5.4, we know that the functor $G$ has a fixpoint
$D:\mathbb{L}_{\leq 1}\to\mathbf{Dcpo}_{\perp!}$ given on objects by

$D(k)=\\{(x_{n})_{n}\in\Pi_{n}D_{n}(k)\mid\forall n\geq
0,\alpha_{n}^{P}(k)(x_{n+1})=x_{n}\\}$

where every $\alpha_{n}^{P}:D_{n+1}\Rightarrow D_{n}$ is part of an embedding
projection pair $\left\langle\alpha_{n}^{E},\alpha_{n}^{P}\right\rangle$, with
$\alpha_{n}^{E}\stackrel{{\scriptstyle\text{def}}}{{=}}\alpha_{n}$. Since
every functor $D_{n}:\mathbb{L}_{\leq 1}\to\mathbf{Dcpo}_{\perp!}$ is product-
preserving, so is $D$: for natural numbers $k$ and $l$, we have

$\displaystyle D(k+l)$
$\displaystyle=\\{(x_{n})_{n}\in\Pi_{n}D_{n}(k+l)\mid\forall n\geq
0,\alpha_{n}^{P}(k+l)(x_{n+1})=x_{n}\\}$
$\displaystyle\cong\\{((y_{n})_{n},(z_{n})_{n})\in\Pi_{n}D_{n}(k)\otimes\Pi_{n}D_{n}(l)\mid\forall
n\geq 0,(\alpha_{n}^{P}(k)(y_{n+1})=y_{n}$
$\displaystyle\wedge\alpha_{n}^{P}(l)(z_{n+1})=z_{n})\\}$ $\displaystyle\cong
D(k)\otimes D(l)$

It follows that $F(D)$ is equal to $G(D)$, which is itself equivalent to $D$.
∎

The denotational semantics of types introduced in Section 5.3 essentially
relies on the category
$\left|\mathbf{KS}\right|\stackrel{{\scriptstyle\text{def}}}{{=}}\mathbf{KS}^{\mathbf{op}}\times\mathbf{KS}$.
The algebraic compactness of $\left|\mathbf{KS}\right|$ can be obtained
through standard results of the literature [2, 4, 13], gathered in [12]:

  * •

Algebraic compactness is a self-dual property: if the category $\mathbf{C}$ is
algebraically compact for locally continuous endofunctors, then so does its
opposite category $\mathbf{C}^{\mathbf{op}}$.

  * •

If the categories $\mathbf{C}$ and $\mathbf{D}$ are algebraically compact for
locally continuous endofunctors, then so does their product category
$\mathbf{C}\times\mathbf{D}$.

######  Corollary 5.6.

The category $\left|\mathbf{KS}\right|$ is algebraically compact for locally
continuous endofunctors.

###  5.3. Kegelspitzen as a model of FPC

As an algebraically compact category, the category $\mathbf{KS}$ is a domain-
theoretic model of FPC [12, Def. 6.7] and therefore constitutes a
computationally adequate model for the language FPC, a functional programming
language with recursive types [12, Th. 7.14].

We recall here the foundations of the semantics of recursive types in FPC, and
refer the interested reader to Fiore’s thesis [11] for a complete account of
the axiomatization of computationally adequate models of FPC.

Type judgements $\Theta\vdash t$ and judgements $\Theta\mid\Gamma\vdash M:t$
(introduced in Appendix A) are respectively denoted by symmetric locally
Scott-continuous $n$-ary functors

$[\\![\Theta\vdash t]\\!]:|\mathbf{KS}|^{n}\to|\mathbf{KS}|$

and by natural transformations

$[\\![\Theta\mid\Gamma\vdash
M:t]\\!]:[\\![\Theta\vdash\Gamma]\\!]\Rightarrow[\\![\Theta\vdash t]\\!]$

i.e. natural families of morphisms

$\big{\\{}[\\![\Theta\mid\Gamma\vdash
M:t]\\!]_{X}:[\\![\Theta\vdash\Gamma]\\!](X)\to[\\![\Theta\vdash t]\\!](X)\mid
X\in|\mathbf{KS}|^{n}\big{\\}}$

in the category $|\mathbf{KS}|$.

The denotation $[\\![\Theta\vdash\Theta_{i}]\\!]$ of the type judgement
$\Theta\vdash\Theta_{i}$ (with $\Theta$ typing context of length $n$) is the
$i$-th projection functor
$\Pi^{|\mathbf{KS}|^{n}}_{i}:|\mathbf{KS}|^{n}\to|\mathbf{KS}|$. Moreover, the
denotation $[\\![\Theta\vdash\mu X.t]\\!]$ of a typing judgement
$\Theta\vdash\mu X.t$ involving a recursive type $\mu X.t$ to be
$\mu[\\![\Theta,X\vdash t]\\!]$, the fixpoint of the functor
$[\\![\Theta,X\vdash t]\\!]:|\mathbf{KS}|^{n+1}\to|\mathbf{KS}|$ by algebraic
compactness.

Now, recall that for functors $F,G:|C|\to|D|$, we have functors
$\Pi^{|\mathbf{C}|}_{2}F,\Pi^{|\mathbf{C}|}_{2}G:|\mathbf{C}|\to\mathbf{D}$,
and therefore a (mixed-variance) functor
$\Pi^{|\mathbf{C}|}_{2}F\otimes\Pi^{|\mathbf{C}|}_{2}G:|\mathbf{C}|\to\mathbf{D}$,
itself in one-to-one correspondence with a symmetric functor
$|\Pi^{|\mathbf{C}|}_{2}F\otimes\Pi^{|\mathbf{C}|}_{2}G|:|C|\to|D|$ by
Proposition 5.3. Then, the denotations of other type contexts is given as
follows.

$[\\![\Theta\vdash t_{1}\times
t_{2}]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}|\Pi^{|\mathbf{\mathbf{KS}}|}_{2}[\\![\Theta\vdash
t_{1}]\\!]\otimes_{\perp}\Pi^{|\mathbf{\mathbf{KS}}|}_{2}[\\![\Theta\vdash
t_{2}]\\!]|$ $[\\![\Theta\vdash
t_{1}+t_{2}]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}|\Pi^{|\mathbf{\mathbf{KS}}|}_{2}[\\![\Theta\vdash
t_{1}]\\!]\oplus\Pi^{|\mathbf{\mathbf{KS}}|}_{2}[\\![\Theta\vdash t_{2}]\\!]|$
$[\\![\Theta\vdash t_{1}\multimap
t_{2}]\\!]\stackrel{{\scriptstyle\text{def}}}{{=}}|\mathbf{KS}(\Pi^{|\mathbf{\mathbf{KS}}|}_{1}[\\![\Theta\vdash
t_{1}]\\!],\Pi^{|\mathbf{\mathbf{KS}}|}_{2}[\\![\Theta\vdash t_{2}]\\!])|$

where
$\Pi^{|\mathbf{\mathbf{KS}}|}_{1}:|\mathbf{\mathbf{KS}}|\to\mathbf{\mathbf{KS}}^{\mathbf{op}}$
and
$\Pi^{|\mathbf{\mathbf{KS}}|}_{2}:|\mathbf{\mathbf{KS}}|\to\mathbf{\mathbf{KS}}$
are the projections of the cartesian product $|\mathbf{\mathbf{KS}}|$,
$\otimes_{\perp}:\mathbf{\mathbf{KS}}\times\mathbf{KS}\to\mathbf{KS}$ is the
smash product functor,
$\mathbf{KS}(-,-):\mathbf{\mathbf{KS}}^{\mathbf{op}}\times\mathbf{KS}\to\mathbf{KS}$
is the homset functor (which acts as exponential in the monoidal closed
structure $(\mathbf{KS},\otimes_{\perp},\mathbf{KS}(-,-))$ of Proposition 2.5.
The functor $\oplus:\mathbf{\mathbf{KS}}\times\mathbf{KS}\to\mathbf{KS}$ is
the functor induced by the coproduct of convex sets, discussed in a
categorical setting in [19] and adapted for (pointed) convex dcpos in [28,
Section 3.1.2].

In detail, recall that the sum $A+B$ of two convex sets, $A$ and $B$, can be
described as the set $A\uplus B\uplus(A\times B\times(0,1))$, where $(0,1)$ is
the open unit interval. Its elements either come directly from $A$, or from
$B$, or are a non-trivial formal convex combination of elements from $A$ and
$B$. With a slightly informal notation, we write $(a,-,0)$ instead of $a$, and
$(-,b,1)$ instead of $b$. Then define the convex structure as follows

$\sum_{i}r_{i}.(a_{i},b_{i},\lambda_{i})\stackrel{{\scriptstyle\text{def}}}{{=}}(\sum_{i}\frac{r_{i}(1-\lambda_{i})}{1-\sum_{i}r_{i}\lambda_{i}}.a_{i},\sum_{i}\frac{r_{i}\lambda_{i}}{\sum_{i}r_{i}\lambda_{i}}.b_{i},({\textstyle\sum_{i}r_{i}\lambda_{i}}))$

taking the obvious convention where $({\textstyle\sum_{i}r_{i}\lambda_{i}})$
is $0$ or $1$. This has the universal property of the coproduct in the
category of convex sets. Therefore, if $A$ and $B$ are (sub)convex dcpos then
we define their _skew sum_ $A\oplus B$ as the coproduct $A+B$ of $A$ and $B$
as convex sets, equipped with the partial order
$(a,b,\lambda)\leq(a^{\prime},b^{\prime},\mu)$ if $a\leq a^{\prime}$ and
$b\leq b^{\prime}$ and $\lambda\leq\mu$. In which case, $A\oplus B$ is a
Kegelspitze when $A$ and $B$ are Kegelspitzen.

It is worth noting that this has a universal property similar to the universal
property of a coproduct, to the exception that there is an additional
requirement that $a\leq b$ for $a\in A$, $b\in B$. For example, we can freely
add a bottom element to a convex dcpo $A$ by taking the skew sum $(1\oplus
A)$.

#### Acknowledgements

I would like to thank Bart Jacobs, Robin Kaarsgaard, Ohad Kammar, Klaus
Keimel, Michael Mislove, Michele Pagani, Christine Tasson and Fabio Zanasi for
helpful discussions, and more particularly Sam Staton for suggesting the
problem. Some of the research leading to the results of the present work was
undertaken while the author was based at Radboud University, and funded by the
European Research Council under the European Union’s Seventh Framework
Programme (FP7/2007-2013) / ERC grant agreement n. 320571. The author’s visits
to the Department of Computer Science of Oxford University have been
financially supported by a Royal Society University Research Fellowship.

## References

  * [1] Samson Abramsky and Achim Jung.  Domain theory.  Handbook of logic in computer science, 3:1–168, 1994.
  * [2] Jirí Adamek.  Recursive data types in algebraically $\omega$-complete categories.  Information and Computation, 118(2):181–190, 1995.
  * [3] Roberto M Amadio and Pierre-Louis Curien.  Domains and lambda-calculi, volume 46.  Cambridge University Press, 1998.
  * [4] Michael Barr.  Algebraically compact functors.  Journal of Pure and Applied Algebra, 82(3):211–231, 1992.
  * [5] Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi.  Lawvere categories as composed PROPs.  In International Workshop on Coalgebraic Methods in Computer Science (CMCS 2016), pages 11–32. Springer, 2016.
  * [6] Vincent Danos and Thomas Ehrhard.  Probabilistic coherence spaces as a model of higher-order probabilistic computation.  Information and Computation, 209(6):966–991, 2011.
  * [7] Thomas Ehrhard, Michele Pagani, and Christine Tasson.  The computational meaning of probabilistic coherence spaces.  In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011), pages 87–96, 2011.
  * [8] Thomas Ehrhard, Michele Pagani, and Christine Tasson.  Full abstraction for probabilistic PCF.  arXiv preprint arXiv:1511.01272, 2015.
  * [9] Thomas Ehrhard and Christine Tasson.  Probabilistic Call by Push Value.  arXiv preprint arXiv:1607.04690, 2016.
  * [10] Thomas Ehrhard, Christine Tasson, and Michele Pagani.  Probabilistic coherence spaces are fully abstract for probabilistic PCF.  In ACM SIGPLAN Notices, volume 49, pages 309–320. ACM, 2014.
  * [11] Marcelo P Fiore.  Axiomatic domain theory in categories of partial maps, volume 14.  Cambridge University Press, 2004.
  * [12] Marcelo P Fiore and Gordon D Plotkin.  An axiomatisation of computationally adequate domain theoretic models of FPC.  In Proceedings of the Symposium on Logic in Computer Science, pages 92–102. IEEE, 1994.
  * [13] Peter Freyd.  Algebraically complete categories.  In Category Theory, pages 95–104. Springer, 1991.
  * [14] Tobias Fritz.  A presentation of the category of stochastic matrices.  arXiv preprint arXiv:0902.2554, 2009.
  * [15] Robert Furber and Bart Jacobs.  From Kleisli categories to commutative C*-algebras: probabilistic Gelfand duality.  In Proceedings of the International Conference on Algebra and Coalgebra in Computer Science (CALCO 2013), pages 141–157. Springer, 2013.
  * [16] Ichiro Hasuo, Bart Jacobs, and Ana Sokolova.  Generic trace semantics via coinduction.  Logical Methods in Computer Science, 3(4), 2007.
  * [17] Bart Jacobs.  Probabilities, distribution monads, and convex categories.  Theoretical Computer Science, 412(28):3323–3336, 2011.
  * [18] Bart Jacobs.  Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59.  Cambridge University Press, 2016.
  * [19] Bart Jacobs, Bas Westerbaan, and Bram Westerbaan.  States of convex sets.  In Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2015), pages 87–101. Springer, 2015.
  * [20] Claire Jones.  Probabilistic non-determinism.  PhD thesis, 1990.
  * [21] Claire Jones and Gordon D Plotkin.  A probabilistic powerdomain of evaluations.  In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), volume 89, pages 186–195, 1989.
  * [22] Achim Jung.  Cartesian closed categories of domains.  CWI Tracts, 66:1–110, 1989.
  * [23] Klaus Keimel and Gordon D Plotkin.  Mixed powerdomains for probability and nondeterminism.  submitted for publication, 2015.
  * [24] F William Lawvere.  Functorial semantics of algebraic theories.  Proceedings of the National Academy of Sciences, 50(5):869–872, 1963.
  * [25] Guy McCusker.  Games and full abstraction for a functional metalanguage with recursive types.  Springer Science & Business Media, 2012.
  * [26] G.D. Plotkin.  LCF considered as a programming language.  Theoretical Computer Science, 5(3):223 – 255, 1977.
  * [27] Mathys Rennela and Sam Staton.  Classical control and quantum circuits in enriched category theory.  In Proceedings of the 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). Electronic Notes in Theoretical Computer Science.
  * [28] Mathys Rennela and Sam Staton.  Complete positivity and natural representation of quantum computations.  319:369–385, 2015.

##  Appendix A FPC

The functional programming language FPC [12] can be seen as a “PCF with
recursive types”, and has been heavily used in the denotational study of
recursive types. A recursive type is an inductively defined data type for
terms which may contain type variables that are used in fixed points. It is an
important concept for high-level programming languages, which allows the
definition of data types such as the types for lists and trees, whose size can
dynamically grow. An example of recursive type in a ML-style functional
programming language is

⬇

type nat = zero | succ nat

which corresponds to the natural numbers.

In recursive type theory, recursive types are written $\mu X.t$, where $X$ is
a type variable which may appear in the type $t$. For example, the type nat is
written $\mu X.1+X$. Indeed, the constructor zero is a type without arguments
and therefore corresponds to the unit type $1$, and succ takes as argument
another term of type nat.

The syntax of FPC relies on two grammars, one for types and one for terms:

$\displaystyle\text{Types }t,u$ $\displaystyle::=X\mid t+u\mid t\times u\mid
t\to u\mid\mu X.t$ $\displaystyle\text{Terms }M,N,P$
$\displaystyle::=x\mid\textbf{inl}_{t,u}(M)\mid\textbf{inr}_{t,u}(M)\mid\textbf{case}(M,x\cdot
N,y\cdot P)$ $\displaystyle\mid(M,N)\mid\lambda
x^{\sigma}.M\mid\textbf{fst}(M)\mid\textbf{snd}(M)\mid\textbf{intro}_{\mu
X.t}(M)\mid\textbf{elim}(M)$

where $X$ is taken in the sort of type variables, and $x$ is taken in the sort
of variables. In detail, we have sum types $t+u$, product types $t\times u$,
function types $t\to u$, and recursive types $\mu X.t$, and corresponding
primitives to manipulate instances of such types. In particular, instructions
such as $\textbf{intro}_{\mu X.t}(M)$ and $\textbf{elim}(M)$ allow
respectively the introduction and the elimination of recursive types, through
a process that we now proceed to describe.

Firstly, we need to define the rules which describe well-formed types and
expressions. For that purpose, we introduce typing judgements $\Theta\vdash
t$, which indicate that the type $t$ is a well-formed type with respect to the
typing context $\Theta$. This means that the free variables of the type $t$
are in the list $\Theta$ of distinct type variables. Recall that a variable is
called free when it is not bound. In this setting, a type variable is free
when it is not used as a parameter of a recursive type. For example, the
variable $X$ is bound in $\mu X.t$ for every type $t$. A closed type is a
well-formed type with no typing context, that is a type $t$ such that the
typing judgement $\vdash t$ holds. The substitution in a type $t$ of every
occurence of a type variable $X$ by a type $t^{\prime}$ is written $t[X\mapsto
t^{\prime}]$. Well-formed types of FPC are defined inductively by the
following rules:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
21.0138pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.02759pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta,X\vdash X$}}}}\qquad\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.73497pt\hbox{$\displaystyle\penalty 1\Theta,X\vdash t$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.03923pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\vdash\mu X.t$}}}}\qquad\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\Theta\vdash t\quad\Theta\vdash u$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=58.22438pt\hbox{\kern
3.00003pt$\star\in\\{+,\times,\to\\}$}}}\hbox{\kern
10.0pt\hbox{$\displaystyle\Theta\vdash t\star u$}}}}$

Similarly, one can define well-formed expressions inductively, using
judgements $\Theta\mid\Gamma\vdash M:t$ which entails that the term $M$ of
well-formed type $t$ (associated with the typing judgement $\Theta\vdash t$)
is well-formed under the context $\Gamma$, defined as a list of distinct
variables, written as $x:t$. What follows is a set of rules which allows to
determine inductively which expressions are well-formed:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
6.89476pt\hbox{$\displaystyle\penalty 1\Theta\mid\Gamma\vdash M:t[X\mapsto\mu
X.t]$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=111.66173pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\mid\Gamma\vdash\textbf{intro}_{\mu X.t}(M):\mu
X.t$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 23.5625pt\hbox{$\displaystyle\penalty
1\Theta\mid\Gamma\vdash M:\mu X.t$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=121.20566pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\mid\Gamma\vdash\textbf{elim}(M):t[X\mapsto\mu
X.t]$}}}}$
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
35.5067pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=71.0134pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\mid\Gamma,x:t\vdash
x:t$}}}}\quad\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 5.59447pt\hbox{$\displaystyle\penalty
1\Theta\mid\Gamma,x:t\vdash M:u$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=89.39218pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\mid\Gamma\vdash\lambda x^{t}.M:t\to
u$}}}}\quad\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Theta\mid\Gamma\vdash M:t\to
u\quad\Theta\mid\Gamma^{\prime}\vdash N:t$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=133.56941pt\hbox{}}}\hbox{\kern
25.55534pt\hbox{$\displaystyle\Theta\mid\Gamma,\Gamma^{\prime}\vdash(M)N:u$}}}}$
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.83629pt\hbox{$\displaystyle\penalty 1\Theta\mid\Gamma\vdash
M:t\quad\Theta\vdash u$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=95.9384pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\mid\Gamma\vdash\textbf{inl}_{t,u}(M):t+u$}}}}\quad\quad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
3.40573pt\hbox{$\displaystyle\penalty 1\Theta\mid\Gamma\vdash
M:t\quad\Theta\vdash u$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=97.07729pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Theta\mid\Gamma\vdash\textbf{inr}_{t,u}(M):u+t$}}}}$
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Theta\mid\Gamma\vdash
M:t+u\quad\Theta\mid\Gamma^{\prime},x:t\vdash
N:v\quad\Theta\mid\Gamma^{\prime},y:u\vdash P:v$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=250.7257pt\hbox{}}}\hbox{\kern
56.36102pt\hbox{$\displaystyle\Theta\mid\Gamma,\Gamma^{\prime}\vdash\textbf{case}(M,x\cdot
N,y\cdot P):v$}}}}$

Now, we can define a program in FPC to be an expression $M$ such that the
judgement $\vdash M:t$ holds for some type $\vdash t$, that is: $M$ is a
closed term of closed type. A context with a hole is an expression $C[-]$ with
holes such that for every term $M$, $C[M]$ is the expression obtained by
replacing every hole by the term $M$. When the context $C[-]$ is of type $t$,
we write $C[-]:t$.

Secondly, the grammars of FPC are associated with the following operational
semantics, which describes how programs are executed. But first, let’s recall
what a reduction system is.

######  Definition A.1.

A reduction system is a pair $(\Lambda,\to)$ of a collection $\Lambda$ of
terms and a binary relation $\to\subseteq\Lambda\times\Lambda$ on terms, which
is called a reduction relation. The transitive reflexive closure of a
reduction relation $\to$ is denoted by $\to^{*}$. And therefore, if the
relation $M\to N$ means that the term $M$ reduces to the term $N$ in one step,
then the relation $M\to^{*}N^{\prime}$ means that the term $M$ reduces to the
term $N$ in finitely many steps. A term $M\in\Lambda$ is a normal form (or
value) if there is no term $N\in\Lambda$ such that $M\to^{*}N$. One says that
the term $M$ has a normal form if it reduces to a normal form in finitely many
steps.

A reduction relation is confluent when for every triplet $(M,N_{1},N_{2})$ of
terms, the following implication holds:

$M\to^{*}N_{1}\wedge M\to^{*}N_{2}\implies\exists
M^{\prime}.\,N_{1}\to^{*}M^{\prime}\wedge N_{2}\to^{*}M^{\prime}$

Additionally, a reduction relation is said to be strongly normalizing when
every reduction sequence $M_{0}\to M_{1}\to\cdots$ eventually terminates.

What follows is the operational semantics of the language FPC.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
48.81184pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=97.62369pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle(\lambda x^{\alpha}.M)N\to
M[N/x]$}}}}\quad\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 15.99304pt\hbox{$\displaystyle\penalty 1M\to
M^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=65.66483pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\lambda x.M\to\lambda
x.M^{\prime}$}}}}\quad\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1M\to M^{\prime},\,M\text{ not
abstract}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=107.33154pt\hbox{}}}\hbox{\kern
19.92363pt\hbox{$\displaystyle(M)N\to(M^{\prime})N$}}}}$

(where an abstract term is a term of the form $\lambda x.M$ for some variable
$x$ and some term $M$)

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
17.50009pt\hbox{$\displaystyle\penalty 1M\to N$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=65.47224pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\textbf{inl}(M)\to\textbf{inl}(N)$}}}}\quad\quad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.63898pt\hbox{$\displaystyle\penalty 1M\to N$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.75002pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\textbf{inr}(M)\to\textbf{inr}(N)$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
43.06978pt\hbox{$\displaystyle\penalty 1M\to\textbf{inl}(L)$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=130.40346pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\textbf{case}(M,x\cdot N,y\cdot P)\to N[x\mapsto
L]$}}}}$
${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1M\to\textbf{intro}_{\mu
X.\tau}(N)$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=68.47897pt\hbox{}}}\hbox{\kern
5.94788pt\hbox{$\displaystyle\textbf{elim}(M)\to N$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
41.33775pt\hbox{$\displaystyle\penalty 1M\to\textbf{inr}(R)$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=128.94287pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\textbf{case}(M,x\cdot N,y\cdot P)\to P[y\mapsto
R]$}}}}$