A model of stochastic memoization and name generation in probabilistic programming:
categorical semantics via monads on presheaf categories

Younesse Kaddar
and Sam Staton
Department of Computer Science, University of Oxford, UK

Stochastic memoization is a higher-order construct of probabilistic programming languages that is key in Bayesian nonparametrics, a modular approach that allows us to extend models beyond their parametric limitations and compose them in an elegant and principled manner. Stochastic memoization is simple and useful in practice, but semantically elusive, particularly regarding dataflow transformations. As the naive implementation resorts to the state monad, which is not commutative, it is not clear if stochastic memoization preserves the dataflow property – whether we can reorder the lines of a program without changing its semantics, provided the dataflow graph is preserved.
In this paper, we give an operational and categorical semantics to stochastic memoization and name generation in the context of a minimal probabilistic programming language, for a restricted class of functions.
Our contribution is a first model of stochastic memoization of constant Bernoulli functions with a non-enumerable type, which validates data flow transformations, bridging the gap between traditional probability theory and higher-order probability models. Our model uses a presheaf category and novel probability monad on it.

probabilistic programming, quasi-Borel spaces, synthetic measure theory, stochastic memoization, name generation, categorical semantics, commutative monads, nominal sets.

§ INTRODUCTION

Bayesian nonparametric models are a powerful approach to statistical learning. Unlike parametric models, which have a fixed number of parameters, nonparametric models can have an unbounded number of parameters that grows as needed to fit complex data. This flexibility allows them to capture subtle patterns in data that parametric models may miss, and it makes them more composable, because they are not arbitrarily truncated.

Prominent examples of nonparametric models include Dirichlet process models for clustering similar data points, and the Infinite Relational Model for automatically discovering latent groups and features, amongst others. These infinite-dimensional models can accommodate an unbounded number of components, clusters, or other features in order to fit observed data as accurately as possible.

Probabilistic programming is a powerful method for programming nonparametric models. Stochastic memoization <cit.>
has been identified as a particularly useful technique in this. This paper is about semantic foundations for stochastic memoization.

In deterministic memoization <cit.>, the idea is to compute a function the first time it is called with a particular argument, and store the result in a memo-table. When the function is called again with the same argument, the memo-table is used, resulting in performance improvement but no semantic difference. Stochastic memoization is this memoization applied to functions that involve random choices, and so a memoized function is semantically different from a non-memoized one, because the random choices will only be made once for each argument.

We illustrate this with a simple example; this is informal and we consider a precise language and semantics in Section <ref>. Consider a function $f$ that returns a random number $[0,1]$ for each argument. It might be written $f(x) = \mlstinline{uniform}$. One run of the program might call $f$ with various arguments, and example runs are as follows:

Calls to $f$ in a particular run of a program:   $f(0)$   $f(1)$   $f(0)$   $f(2)$   $f(1)$   $f(3)$   …

Results of calls in a run without memoization:   0.43   0.01   0.72   0.26   0.48   0.16   …

Results of calls in a run with memoization:   0.43   0.01   0.43   0.26   0.01   0.16   …

Thus in the memoized version, when the function is called again with the same value, the previous result is recalled, and the random choices are not made again. (Note that although this is called `stochastic memoization', the terminology is perhaps confusing: the memoization always happens, and it is not `randomly deciding whether or not to memoize'.)

From a semantic perspective, the role of stochastic memoization is clear when we use a monad-based interpretation with a probability monad |Prob|.
This might be thought of as the Giry monad <cit.> or a probabilistic powerdomain <cit.>, or a Haskell monad (e.g. <cit.>).

A distribution on a type |b| with parameters from |a| has type |a -> Prob(b)|. On the other hand, a random function is a probability distribution on the type of deterministic functions, having type |Prob(a -> b)|. Whereas parameterized distributions are a key idea in parametric statistics, random functions are a key idea in nonparametric statistics. And stochastic memoization is a higher-order function with probabilistic effects, of type
mem :: (a -> Prob b) -> Prob (a -> b)

that converts parameterized distributions into random functions, by making the random choice once for each argument.
This |mem| combinator plays a crucial role in Church <cit.> and WebPPL <cit.>, and appears with this type in our Haskell library LazyPPL <cit.>. Stochastic memoization also plays a role in Blog <cit.>, Hansei <cit.>, and many other languages (e.g. <cit.>). It is not difficult to implement stochastic memoization, by using a memo-table. Nonetheless, its semantic properties remain elusive and developers have noted bugs and complications (e.g. <cit.>). Moreover, the existing semantic models of probability (such as <cit.>) only support |mem| for very restricted domain types |a| (see <ref>). In particular our own Haskell library <cit.> supports stochastic memoization but the recent semantic analysis <cit.> only explains it at certain domain types. The point of this paper is to extend this semantic analysis of stochastic memoization to a broader class of domains.

First example: White noise in a non-parametric clustering model.
One common first example of stochastic memoization is as follows. Suppose we have a finite set of individuals, and we want to group them into an unknown number of clusters, and then assign attributes to the clusters. For example, we may want to form clusters and consider attributes on the clusters such as `Brexit-supporters', `mean geographic latitude/longitude', `geographic variance', `mean salary', and so on. A popular route is the `Dirichlet process with memoization', as follows, for which a generative model has the following pseudocode (see e.g. <cit.><cit.>):

* We randomly decide which proportion of individuals are in each cluster. We assign a unique identifier to each cluster, from some space $\Atoms$ of identifiers. One might use the Dirichlet process with a diffuse base measure on $\Atoms$, for example the normal distribution on the real numbers.

* Assign attributes to the cluster identifiers. For example, depending on whether that cluster supports Brexit, assign either true or false to the identifier. This particular assignment is a sample from a random function in $(\Atoms\to 2)$. This distribution might come from memoizing a constant Bernoulli distribution, assigning `true' to any cluster identifier with probability $0.5$.

* Steps (i)-(ii) are generative, and we could run them to get some synthetic data. The idea of Bayesian clustering is to start with steps (i)–(ii) as a reasonable prior distribution, in generative form, and to combine this with actual data to arrive at a posterior distribution.
In this example the actual data might come from a telephone survey, and we use conditional probability (aka Bayesian inversion) to arrive at a posterior distribution on the cluster proportions and their attributes. We can then use this to make predictions. The constant Bernoulli memoization is a reasonable prior for Brexit support, but the posterior will typically be much more complicated, with various correlations, etc.

In this paper, we focus on step (ii), stochastic memoization: steps (i) and (iii) are studied extensively elsewhere (e.g. see <cit.> in the statistics literature, or <cit.> in the semantics literature, and references therein).

This simple example of a memoized constant Bernoulli function is easy to implement using a memo-table, but already semantically complicated. If we put $\Atoms=\mathbb{R}$, the real numbers, for the base measure, as is common in statistical modelling, then the memoized constant Bernoulli distribution on $(\Atoms\to 2)$ is 1-dimensional white noise: intuitively, for every $x\in\mathbb{R}$ we toss a coin to pick true or false, making an uncountable number of independent random choices. (As an aside, we note that we could combine steps (i) and (ii), using a complicated base measure for the Dirichlet process that includes all the attributes. This model would not be compositional, and in any case, some kind of memoization would still be needed to implement the Dirichlet process.)

First example: White noise. For example, in our Haskell library LazyPPL <cit.>, suppose we start with a function which randomly picks a number in $[0,1]$ every time it is called:
[mathescape]|const (uniform 0 1) :: $\mathbb{R}$ -> Prob $\mathbb{R}$|. We can use stochastic memoization to create a memoized function that randomly assigns a number to every input number, sometimes referred to as “white noise" (<ref>):

[mathescape]|mem (const (uniform 0 1)) :: Prob ($\mathbb{R}$ -> $\mathbb{R}$)|.

This is an important basic example of stochastic memoization, which can serve as an essential building block for more complex models and practical implementations in probabilistic programming languages like Church <cit.>, WebPPL <cit.>, and (in this typed form) in LazyPPL <cit.>.

Two samples from a non-memoized function (pointwise) and the memoized white noise function.

The central issue addressed in this paper is that the straightforward implementation of stochastic memoization makes use of the state monad, which does not satisfy the dataflow property in general. The dataflow property permits reordering the lines of a program as long as the dataflow graph is preserved. This property is valuable for inference algorithms and program optimization. But most of all, it is essential to have a model of probability (see Section <ref>).

In this paper, we address the challenge of showing that the following items are consistent:

(1) a type $\Atoms$ with a diffuse probability distribution (Def <ref>);

(2) a type $\tbool$ of Booleans with Bernoulli probability distributions (i.e. tossing coins, including biased coins);

(3) a type of functions $[\Atoms\to \tbool]$, with function application (<ref>);

(4) stochastic memoization of the constant Bernoulli functions (<ref>);

(5) the language supports the dataflow property (Def. <ref>).

These items are together inconsistent with traditional measure theory, as we discuss in Section <ref>, where we also make the criteria precise. Nonetheless (1)-(4) are together easy to implement in a probabilistic programming language, and useful for Bayesian modelling. Item (5) is a very useful property for program reasoning and program optimization. Item (5) is also a fundamental conceptual aspect of axiomatic probability theory, since in the measure-theoretic setting it amounts to Fubini's theorem <cit.> and the fact that probability measures have mass $1$, and in the categorical abstraction of Markov categories <cit.> it amounts to the interchange law of affine monoidal categories.

There are measure-theoretic models where some of these items are relaxed (<ref>–<ref>). For example, if we drop the requirement of a diffuse distribution, then there are models using Kolmogorov extension (<ref>).

A grand challenge is to further generalize these items, for example to allow memoization of functions $A\to B$ for yet more general $A$ and $B$, and to allow memoization of all definable expressions. Since the above five items already represent a significant challenge, and our semantic model is already quite complicated, we chose to focus on a `minimal working example' for this paper.

To keep things simple and minimal, in this paper we side-step measure-theoretic issues by noticing that the equations satisfied by a diffuse probability distribution are exactly the equations satisfied by name generation (e.g. <cit.>). Because of this, we can use categorical models for name generation (following e.g. <cit.>, <cit.>) instead of traditional measure theory. Name generation can certainly be implemented using randomness, and there are no clashes of fresh names if and only if the names come from a diffuse distribution (see also e.g. <cit.>). On the other hand, if we keep things simple by regarding the generated names as pure names <cit.>, we avoid any other aspects of measure theory, such as complicated manipulations of the real numbers.

To address the challenge of the consistency of items (1)–(5) above, our main contributions are then as follows.

* We first provide an operational semantics for a minimal toy probabilistic programming language that supports stochastic memoization and name generation (<ref>).

* We then (<ref>) construct a cartesian closed (for function spaces) categorical model of this language endowed with an affine commutative monad (Theorem <ref>). In common with other work on local state (e.g. <cit.>), we use a functor category semantics, indexing sets by possible worlds. In this paper, those worlds are finite fragments of a memo-table.

* We prove that our denotational semantics is sound with respect to the operational semantics, ensuring the correctness of our approach and validating that lines can be reordered in the operational semantics (Theorem <ref>). The class of functions that can be memoized includes constant Bernoulli functions. We call these functions freshness-invariant (Definition <ref>).

The soundness theorem (<ref>) is not trivial because the timing of the random choices differs between the operational and denotational semantics. In the operational semantics, the memo-table is partial, and populated lazily as needed, when functions are called with arguments. This is what happens in all implementations. However, this timing is intensional, and so by contrast, in the denotational semantics, the memo-table is always totally populated as soon as the current world is extended with any functions or arguments.

* Finally, we present a practical Haskell implementation <cit.> which compares the small-step, big-step operational, and denotational semantics, demonstrating the applicability of our results (<ref>).

§ STOCHASTIC MEMOIZATION BY EXAMPLE

This section discusses the law of stochastic memoization and provides examples in finite, countable, and non-enumerable domain settings. We then address the challenges posed by the naive use of the state monad, and we clarify our objective: finding a model of probability that supports stochastic memoization over non-enumerable domains, satisfying the dataflow property, and that has function spaces.

In what follows, we use two calculi: (a) The internal metalanguage of a cartesian closed category with a strong monad |Prob|, for which we use Haskell notation, but which is roughly Moggi's monadic metalanguage <cit.>. (b) An ML-like programming language which is more useful for practical programming, but which would translate into language (a); this is roughly Moggi's `simple programming language' <cit.>. We assume passing familiarity with probability and monadic programming in this section, but the informal discussion here sets the context, and we move to more formal arguments in Section <ref>.

(Recall some Haskell notation: we write |-> t| for lambda abstraction; |>>=| for monadic bind, i.e. Kleisli composition; |return| for the unit; a |do| block allows a sequence of monadic bound instructions. We write |const x| for the constant |x| function, |const x = -> x|.)

Memoization law.

A strong monad supports stochastic memoization of type |a->b| if it is equipped with a morphism
|mem :: (a -> Prob b) -> Prob (a -> b)| that satisfies the following equation in the metalanguage, for every [mathescape]|x$\cb_0$ :: a| and
|f :: a -> Prob b|:

\begin{equation}\label{eqn:mem-monad}
\mlstinline{mem f     =    f x$_0\,$ >>= (\\y$_0\,$ -> mem f >>= (\\fMem -> return (\\x -> if x == x$_0\,$ then y$_0\,$ else fMem x) ) )}
\end{equation}

As noted at the beginning of this section, we will pass between an internal metalanguage for strong monads, and an ML-like programming language that would be interpreted using strong monads. In Section <ref> we introduce this programming language precisely, but for now we note that it has a special syntax $\lambdamem{x} u$, meaning [mathescape]|mem ($x$ -> $u$)|, since this is a common idiom\footnote{borrowing Melliès' use of the Hebrew letter $\mathsf{\mem}$ (``mem'')~\cite{melliesLocalStatesString2014}}. The law of Definition~\ref{def:mem} requires equations such as:
\vspace{-1em}
\begin{equation}\label{eqn:stochmem}\begin{minipage}[!htb]{.4\textwidth}
\begin{minipage}[!htb]{.3\textwidth}
\[\begin{aligned}&\iletin f {\lambdamem{{ x}}{{u}}\\&}{f@ n}\end{aligned}
\qquad{\large\overset{\mathclap{\text{1 sample}}}{=}}\qquad
\end{minipage}

\end{minipage}
\begin{minipage}[!htb]{.55\textwidth}
\begin{minipage}[!htb]{.3\textwidth}
\[\begin{aligned}
&\iletin f{\lambdamem{x}{u}}
{\\&\iletin {v_1} {f @ n }{
\\&\iletin {v_2}{f@ n}{
\\&\ireturn (v_1, v_2)}}}\end{aligned}
\qquad{\large \overset{\mathclap{\text{several samples}}}{=}}\qquad\quad
\begin{aligned}
&\iletin v {u[n/x]}{\\
&\ireturn (v, v)}\end{aligned}\]
\end{minipage}
\end{minipage}\end{equation}

\label{sec:examples}

The examples in the introduction use memoization of a constant Bernoulli function, i.e.
\begin{equation}\label{eqn:mem-const-bernoulli}
\mlstinline{mem (\\x ->bernoulli p)  =  mem (const (bernoulli p)) :: Prob(a -> Bool)}
\end{equation}
i.e.~$xbernoulli p$,
where \lstinline|bernoulli p :: Prob Bool| is a Bernoulli probability distribution (biased coin toss) with bias~\lstinline|p|. An intuition is that this is a binary white noise; every point in~\lstinline|a| has an independently chosen random Boolean value.

Notice that for the laws we have also needed function application
\begin{equation}\label{eqn:fn-app}
@ \quad\mlstinline{   :: ((a -> b) , a) -> b}
\end{equation}
In summary, memoized constant Bernoulli functions~\eqref{eqn:mem-const-bernoulli}, and function application~\eqref{eqn:fn-app}, are a bare minimum to discuss semantic issues around stochastic memoization.

We now consider interpretations where the domain \lstinline|a| is finite (\S\ref{sec:fin-mem}), countable (\S\ref{sec:countable}), and uncountable (\S\ref{sec:mem-nonatomic}).
%Stochastic memoization is, in practice, a convenient way to implement infinite sequences of random variables, point processes, clustering, and nonparametric Bayesian models in probabilistic programming. On the theoretical front, stochastic memoization may be crucial for obtaining general representation theorems for exchangeable data types, similar to de Finetti's theorem~\cite{finettiPrevisionSesLois1937} (for exchangeable sequences) or the Aldous-Hoover theorem~\cite{aldousRepresentationsPartiallyExchangeable1981,hooverRelationsProbabilitySpaces1979} (for exchangeable arrays).

\subsection{Memoization with finite domain}%\newcommand{\mlstinline}[1]{\mbox{\lstinline|#1|}}
\label{sec:fin-mem}

For finite domains \lstinline|a|, memoization is straightforward. It involves simply sampling a value of $f(x)$ for all inhabitants of $x ∈ X$ and returning the assignment as a finite mapping. For example, when $a = bool$, we can implement memoization in Haskell as follows:
\begin{lstlisting}[language=haskell]
mem f   =   do { fT <- f True ; fF <- f False ; return (\b -> if b then fT else fF)}
\end{lstlisting}
% (\fT fF -> \case {True -> fT; False -> fF}) <$> f True <*> f False
% \begin{lstlisting}[language=haskell]
% mem :: (Bool -> Prob b) -> Prob (Bool -> b)
% mem (f :: Bool -> Prob b) = do
% 	fTrue <- f True
% 	fFalse <- f False
% 	return (\case
% 		True -> fTrue
% 		False -> fFalse)
% \end{lstlisting}

\paragraph{Semantic interpretation with finite domain.} Memoization with finite domains is supported by a denotational semantics using any strong monad. For example, the category of sets and the monad of finitely supported probability distributions (e.g.~\cite{jacobs-probabilities}). For $a=bool$, this is nothing but the double-strength:
\[
\mlstinline{(bool -> Prob b)} \cong \mlstinline{(Prob b,Prob b)} \xrightarrow{\text{double-strength}} \mlstinline{Prob (b,b)}\text.
\]
For other finite $a$, it is defined using the double-strength by induction.

\subsection{Memoization with countable/enumerable domain}
\label{sec:countable}
When \lstinline|a| is enumerable, such as \lstinline|a=Int|, memoization is useful for defining point processes. Memoization can be regarded as providing an infinite stream of random choices, since the streams over \lstinline|b| are isomorphic with the functions
\lstinline|a -> b|.

Infinite streams of random choices are crucial examples of statistical processes~\cite{gv-bnp}. For an example of an application, recall the one-dimensional Poisson point process. This is a random sequence of real numbers in which the gaps between consecutive numbers are exponentially distributed. Assuming an exponential distribution with a given rate, \lstinline|exponential rate :: Prob RealNum|, we can sample a sequence of these exponential gaps from \lstinline|mem (const (exponential rate)) :: Prob (Int -> RealNum)|.
To get the corresponding list of points of the Poisson point process (with exponential interoccurence times), we simply keep a cumulative sum total of the points, starting from the \lstinline|lower| point:

\begin{lstlisting}[language=haskell]
poissonPP :: Double -> Double -> Prob [Double]
poissonPP lower rate = do { gaps <- mem (const (exponential rate)) ; return (scanl1 (+) lower (map gaps [1 .. ])) }
\end{lstlisting}

We implement memoization with enumerable \lstinline|a| in the Haskell LazyPPL library~\cite{lazyppl-popl} without using state, instead using Haskell's laziness and tries, following~\cite{hinzeGeneralizingGeneralizedTries2000} (see~\cite{lazyppl-popl}). We use the Poisson process extensively in the demonstrations for LazyPPL~\cite{LazyPPL}. %However, in this specific example where the domain of the memoized function is enumerable, we can take advantage of the host language's laziness to circumvent the issue of manipulating countably infinite sequences. For example, in LazyPPL, taking advantage of Haskell's laziness and recursion~\cite{lazyppl-popl}:

%poissonPP lower rate = exponential rate >>= \step -> let x = lower + step in (x :) <$> poissonPP x rate

%With laziness, we can also use tries (implemented in LazyPPL too), following~\cite{hinzeGeneralizingGeneralizedTries2000}.

\paragraph{Semantic interpretation with enumerable domains.} Memoization with enumerable domains is supported by a denotational semantics using the category of measurable spaces and the Giry monad~\cite{giry}. Although the category is not Cartesian closed, the function space $B^$ \emph{does} exist for all standard Borel $B$, and is given by the countable product of $B$ with itself, $∏_B$. Memoization amounts to using Kolmogorov's extension theorem to define a map $(G B)^→G(B^)$ (see \cite[\S4.8]{pollard-book} and~\cite[Thm.~2.5]{dirichlet-is-natural}).

\hide{\paragraph{Random graphs} Stochastic memoization is particularly useful for programming statistical models with random relational structures, such as graph social networks, the world wide web, or biochemical pathways. When modeling relational data, one typically represents observations of binary relationships between object collections with random arrays $(X_{i, j})_{i, j}$ of Boolean random variables, where $i$ and $j$ range over countable collections of potentially related objects.

When comparing a single countable object collection pairwise (i.e., $i$ and $j$ range over the same countable index), the array $(X_{i, j})_{i, j}$ can be viewed as the adjacency matrix of a random graph. These random adjacency matrices $(X{i, j})_{i, j}$ are considered \emph{exchangeable} if their joint distribution remains invariant under node relabeling in the corresponding graph. Assuming the random graph is simple (i.e., $(X{i, j})_{i, j}$ is symmetric with zero diagonal), the Aldous-Hoover theorem posits that every associated exchangeable adjacency matrix can be parameterized by a random measurable function $G: [0, 1]^2 ⟶ [0, 1]$ called as a \emph{graphon}. For two nodes $i$ and $j$ in the random simple graph, $G(u_i, u_j)$ is the edge probability between them, with $u_i$ and $u_j$ being independent and identically distributed (iid) random variables. Consequently, Bayesian models for exchangeable simple graphs are fully determined (in distribution) by a prior over graphons.

Consider, for instance, a Haskell typeclass \lstinline|RandomGraph|, corresponding to an abstract type whose interface enables generating a new random graph (with \lstinline|newGraph|) from a seed \lstinline|g|, drawing vertices at random (with \lstinline|newVertex|), and examining the presence of edges between vertices (with \lstinline|isEdge|). In line with the Aldous-Hoover theorem~\cite{aldousRepresentationsPartiallyExchangeable1981,hooverRelationsProbabilitySpaces1979,orbanz-roy}, every measurable function $\mlstinline{g}: [0, 1]^2 → [0, 1]$ (a \emph{graphon}) can serve as a seed, resulting in the following implementation in the LazyPPL library:

\begin{minipage}[!htb]{.51\textwidth}
\begin{lstlisting}[language=haskell]
class RandomGraph g where
type Graph g
data Vertex g
newGraph:: g -> Prob (Graph g)
newVertex:: Graph g -> Prob (Vertex g)
isEdge:: Graph g -> Vertex g -> Vertex g -> Bool
newtype Graphon = G ((*'$\mathbb{R}$'*, *'$\mathbb{R}$'*) -> *'$\mathbb{R}$'*)
\end{lstlisting}
\end{minipage}
\,
\begin{minipage}[!htb]{.49\textwidth}
\begin{lstlisting}[language=haskell]
instance RandomGraph Graphon where
type Graph Graphon = (*'$\mathbb{R}$'*, *'$\mathbb{R}$'*) -> Bool
data Vertex Graphon = V *'$\mathbb{R}$'*
-- return a random function '(*'$\color{gray}\mathbb{R}$'*, *'$\color{gray}\mathbb{R}$'*) -> Bool'
newGraph (G graphon) = mem $ bernoulli . graphon
newVertex _ = V <$> uniform
isEdge graph (V x) (V y) = graph (x, y)
\end{lstlisting}
\end{minipage}

The memoization function \lstinline[mathescape]|mem :: (($ℝ$, $ℝ$) -> Prob Bool) -> Prob (($ℝ$, $ℝ$) -> Bool)| ensures that once an edge between $x$ and $y$ is sampled (with probability \lstinline|graphon (x, y)|), its presence or absence remains constant throughout the rest of the program execution. For example, \lstinline|newGraph (G (const 0.5))| generates the Erdős-Rényi~\cite{erdosRandomGraphs1959,radoUniversalGraphsUniversal1964,ackermannWiderspruchsfreiheitAllgemeinenMengenlehre1937} random graph.}

\subsection{Memoization with non-enumerable/diffuse domain }
\label{sec:mem-nonatomic}
We now move beyond enumerable domains, to formalize the challenge from Section~\ref{sec:intro}.
In Section~\ref{sec:intro} we illustrated this with a clustering model. See~\cite{LazyPPL} for the full implementation in our Haskell library, LazyPPL, along with other models that also use memoization, including a feature extraction model that uses the Indian Buffet Process, and relational inference with the infinite relational model (following~\cite{probmods-non-parametric}).

Rather than axiomatizing uncountability, we consider diffuse distributions.
\begin{definition}[Diffuse distribution]\label{eqn:diffuse}
Let \lstinline|a| be an object with an equality predicate (\lstinline|(a,a)->bool|). A \emph{diffuse distribution}\footnote{Diffuse measures are often called `atomless' in probability theory. We will also want to regard names in name generation as atomic, so we avoid this clash of terminology.} is a term \lstinline|p| such that
\[\mlstinline{do \{x <- p ; y <- p ; return (x ==y)\}}
\qquad\text{is semantically equal to }\qquad
\mlstinline{return (false)}\text.
\]
\end{definition}
For example, in a probabilistic programming language over the real numbers, we can let \lstinline|a| be the type of real numbers and let \lstinline|p| be a uniform distribution on $[0,1]$, or a normal distribution, or an exponential distribution. These are all diffuse in the above sense. The Bernoulli distribution on the booleans is not diffuse, because there is always a chance that we may get the same result twice in succession.

For the reader familiar with traditional measure theory, we recall that if \lstinline|p| is diffuse then \lstinline|a| is necessarily an uncountable space. For any probability distribution on a countable discrete space must give non-zero measure to at least one singleton set.%\todo{Someone may complain that we didn't define trad measure theory.}

The implementation trick using tries from Section~\ref{sec:countable} will not work for diffuse measures, because we cannot enumerate the domain of a diffuse distribution. It is still possible to implement memoization using state and a memo-table (e.g.~\cite{LazyPPL}). Unlike a fully stateful effect, however, in this paper we argue that stochastic memoization is still compatible with commutativity/dataflow program transformations:

\begin{definition}[Dataflow property]\label{eqn:dataflow}
A programming language is said to have the \emph{dataflow property} if program lines can be reordered (commutativity) and discarded (discardability, or affineness) provided that the dataflow is preserved.
In other words, the language satisfies the following commutativity and discardability equations:

\begin{align}
%  &\hspace{-3mm}(\letin {x_1} {t_1} {\letin {x_2} {t_2} u}) = (\letin {x_2} {t_2} {\letin {x_1} {t_1} u})\label{eq:let-comm}\\
\hspace{-3mm}\mlstinline{do \{x1 <- t1 ; x2 <- t2 ; u\}}\ &=\ \mlstinline{do \{x2 <- t2 ; x1 <- t1 ; u\}}
%\letin {x_1} {t_1} {\letin {x_2} {t_2} u}) = (\letin {x_2} {t_2} {\letin {x_1} {t_1} u})
\label{eq:let-comm}\\
% &\hspace{-3mm} (\letin {x_1} {t_1} {t_2}) = t_2\label{eq:let-affine}\\
\mlstinline {do \{x1 <- t1 ; t2\}} & = \mlstinline{t2}
\label{eq:let-affine}
&\text{where $\mlstinline{x1} ∉ \fv(\mlstinline{t2})$ and $\mlstinline{x2} ∉ \fv(\mlstinline{t1})$.}
%  &\quad\text{where $x_1 ∉ \fv(t_2)$ and $x_2 ∉ \fv(t_1)$.}
\end{align}
\end{definition}
The dataflow property expresses the fact that, to give a meaning to programs, the only thing that matters is the topology of dataflow diagrams. %In other words, the semantics of programs is stable under symmetries of their dataflow diagrams.
These transformations are very useful for inference algorithms and program optimization. But above all, on the foundational side, dataflow is a fundamental concept that corresponds to monoidal categories and is crucial to have a model of probability. As for monoidal categories, a strong monad is commutative \eqref{eq:let-comm} if and only if its Kleisli category is monoidal (commutativity is the monoidal interchange law), and affine \eqref{eq:let-affine} if the monoidal unit is terminal. In synthetic probability theory, dataflow is regarded by various authors as a fundamental aspect of the abstract axiomatization of probability:
Kock~\cite{kock-comm-monad} argues that any monad that is strong commutative and affine can be abstractly viewed as a probability monad, and affine monoidal categories are used as a basic setting for synthetic probability by several authors~\cite{fritz,cho-jacobs,dario-thesis,dario}.
The reader familiar with measure-theoretic probability will recall that the proof that the Giry monad satisfies~(\ref{eq:let-comm}) amounts to Fubini's theorem for reordering integrals (e.g.~\cite{staton:sfinite}).

%	\item Kock~\cite{kock-comm-monad} argues that any monad that is strong commutative and affine can be abstractly viewed as a probability monad.
%	\item Affine (or semi-cartesian) monoidal categories (\ie monoidal categories where the tensorial unit is terminal), of which the category of probability kernels is an example, are used as a basic setting for synthetic probability by several authors~\cite{fritz,cho-jacobs,dario-thesis,dario,staton:sfinite}.

%More concretely, in the denotational semantics of a probabilistic programming language, the dataflow property corresponds to Fubini's theorem (\cref{eq:let-comm}) and the fact that probabilities have mass $1$ (\cref{eq:let-affine}). This leads to a more general definition of exchangeability for data types than the one of random arrays seen previously (Section~\ref{sec:countable}). An abstract data type for a random process expressed in a probabilistic programming language is said to be \emph{exchangeable} if adding it to the language does not break the dataflow property~\cite{xrp-data}.

\paragraph{Semantic interpretations for diffuse domains}\newcommand{\RR}{\mathbb{R}}
The point of this paper is to provide the first semantic interpretation for memoization of the constant Bernoulli functions~(\ref{eqn:mem-const-bernoulli}) with diffuse domain (Def.~\ref{eqn:diffuse}).
We emphasize that although other models can support some aspects of this, there is no prior work that supports everything.
\begin{itemize}
\item With countable domain, there is a model in measurable spaces, as discussed in Section~\ref{sec:countable}. But there can be no diffuse distribution on a countable space.
\item In measurable spaces, we can form the uncountable product space~$\prod_\RR 2$ of $\RR$-many copies of~$2$. We can then define a white noise probability measure on $\prod_\RR 2$ via Kolmogorov extension (e.g.~\cite[4.9(31)]{pollard-book}). Moreover, there are diffuse distributions on $\RR$, such as the uniform distribution on $[0,1]$. However, it is known that there is no measurable evaluation map $\RR\times (\prod_\RR 2)\to 2$ (see~\cite{aumann}), and so we cannot interpret function application~(\ref{eqn:fn-app}).
\item In quasi-Borel spaces~\cite{qbs}, there is a quasi-Borel space $[\RR\to 2]$ of measurable functions, and a measurable evaluation map $\RR\times ([\RR\to 2)\to 2$, but there is no white noise probability measure on $[\RR\to 2]$. The intuitive reason is that, in quasi-Borel spaces, a probability measure on $[\RR\to 2]$ is given by a random element, i.e.~a morphism $\Omega\to[\RR\to 2]$, which curries to a measurable function $\Omega\times\RR\to 2$. But there is no such measurable function representing white noise (e.g.~\cite[Ex~1.2.5]{kallianpur}).
% For another intuition, uncurrying this morphism gives a measurable function $[\RR\times \RR\to 2]$, which can be regarded as a `random-free graphon', whereas it is known that a gray graphon is needed to produce the white noise of the Erdos-Renyi graph.
%  One might consider moving to quasi-measurable spaces~\cite{QMS} to address this, but that still does not support a white noise measure on $[\RR\to 2]$~\cite{QMS-no-go}.
\item There are domain-theoretic treatments of probability theory that support Kolmogorov extension, uniform distributions on $\RR$, and function spaces~\cite{jia-monad,jgl-domain-probprog}. However, these treatments regard the real numbers $\RR$ as constructive, and hence there are no non-trivial continuous morphisms $\RR\to 2$, and there is no equality test on $\RR$, so that we cannot regard $\RR$ with a diffuse distribution as formalized equationally in Definition~\ref{eqn:diffuse}. The same concern seems to apply to recent approaches using metric monads\cite{mpp-wasserstein-alg}.
\item The semantic model of beta-bernoulli in~\cite{staton:betabernoulli} is a combinatorial model that includes aspects of the beta distribution, which is diffuse in measure theory. That model does not support stochastic memoization, but as a presheaf-based model it is a starting point for the model in this paper.
\item There is a straightforward implementation of stochastic memoization that uses local state, as long as the domain supports equality testing \cite{LazyPPL}. The informal idea is to make the random choices as they are needed, and remember them in a memo-table, and keep this memo-table in a local state associated with the function. Therefore one could use a semantic treatment of local state to analyze memoization. For example, one could build a state monad in quasi-Borel spaces. However, state effects in general do not support the dataflow property (Def.~\ref{eqn:dataflow}), since we cannot reorder memory assignments in general. Ideally, one could use a program logic to prove that this particular use of state does support the dataflow property. Although there are powerful program logics for local state and probability (e.g.~\cite{bizjak-birkedal}), we have not been able to use them to prove this.
\end{itemize}
There are other models of higher-order probability (e.g.~\cite{measurable-cones,crubille-cones,cp-games-prob}). These do not necessarily fit into the monad-based paradigm, but there may be other ways to use them to address the core challenge in Section~\ref{sec:intro}.

% \begin{example}[Commutativity is Fubini's theorem and discardability marginalization]
% 	The quasi-Borel spaces (QBS) categorical model~\cite{qbs} satifies the dataflow property.
% 	In this model, the meaning of a probabilistic program \lstinline|p| returning random values of type $X$ is a QBS probability measure, which can be seen as an expectation calculator of the form
% 	$$\den{\mlstinline{p}} ≝ X \xto k Ω ⟼ \int_{Ω} k(α(ω)) \,\d ω ∈ P(X) ⊆ ((X → Ω) → Ω)$$
% 	where $k：X → Ω$ a QBS morphism and $M_X ∋ α：Ω → X$ is the admissible random element corresponding to the interpretation of the program as a measure on the QBS $X$ (the monad of probability measures is a submonad of the continuation monad generated by admissible random elements). Then, if the program makes, say, $n$ consecutive samples and $ω ≝ (ω_1, …, ω_n)$, the denotation of the program \lstinline[mathescape]|p$\cb^{σ}$| where the sample statements are shuffled by a permutation $σ$ is $$\den{\mlstinline{p}{\cb^{σ}}}(k) ≝ \int_{Ω} k(α(ω_1, …, ω_n)) \,\d(ω_{σ(n)}, …, ω_{σ(1)}) = \int_{Ω} k(α(ω_1, …, ω_n)) \,\d(ω_n, …, ω_1) = \den{\mlstinline{p}}(k)$$
% 	This is Fubini's theorem (integrals over probability spaces can be reordered).
% 	In a similar vein, discardability corresponds to marginalizing unused variables.
% \end{example}

%\subsection{Challenges for probability theory}

%On the semantic side, the dataflow property is not trivial. Informally, stochastic memoization appears related to Kolmogorov's extension theorem, which relates probability measures on infinite product spaces to probability measures on the projections from the product. Arguably, then, stochastic memoization validates dataflow transformations because it is not \emph{intrinsically} stateful, rather, it is linked to a fundamental part of pure probability theory. However, traditional probability theory does not actually support higher-order functions~\cite{aumann}, and higher-order probability is a burgeoning field~\cite{fritz,cho-jacobs,kock,qbs,dario-thesis}. Existing models of higher-order probability, such as quasi-Borel spaces~\cite{qbs}, do not support stochastic memoization in full generality, and this is the contribution of our work: a first model of stochastic memoization with a non-enumerable type and validating the dataflow transformations~\eqref{def:dataflow-property}.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
%%% End:

\section{A language for stochastic memoization and name generation}
\label{sec:syntax}

Our probabilistic programming language has a minimal syntax, emphasizing the following key features:
\begin{itemize}
\item \textbf{name generation}: we can generate fresh names (referred to as \emph{atomic} names or \emph{atoms}, in the sense of Pitts' nominal set theory~\cite{pittsNominalSetsNames2013}) with constructs such as $\letin{x}{\ifresh}{⋯}$. In the terminology of Def.~\ref{eqn:diffuse}, this is like a generic diffuse probability measure, since fresh names are distinct.
\item basic \textbf{probabilistic effects}: for illustrative purposes, the only distribution we consider, as a first step, is the Bernoulli distribution (but it can easily be extended to other discrete distributions). Constructs like $\letin{b}{\iflip}{⋯}$ amount to flipping a coin with bias $θ$ and storing its result in a variable $b$.
\item \textbf{stochastic memoization}: if a probabilistic function $f$ -- defined with the new $\lambdamem{}{}$ operator -- is called twice on the same argument, it should return the same result (\cref{eqn:stochmem}).
\end{itemize}

We have the following base types: $$ (booleans), $$ (atomic names), and $$ (which can be thought of as the type of memoized functions $→$). For the sake of simplicity, we do not have arbitrary function types. In fine-grained call-by-value fashion~\cite{levy:cbpv}, there are two kinds of judgments: typed values, and typed computations. The grammar and typing rules of our language are given in Figure~\ref{fig:language}. The typing rules are standard, except for the $$ operator, which is the key novelty of our language. The typing rule for $$ is given in Figure~\ref{fig:language} and is explained in the next section. (Also, equality $v = w$ and memoized function application $v @ w$ are pure computations, \ie in the categorical semantics (\cref{sec:cat-semantics}), they will be composed by the unit of the monad.)

% \begin{figure*}[t]
%     \setlength{\tabcolsep}{1em}
%     % \setlength{\extrarowheight}{1pt}
%     \centering
%     \begin{tabular}{|l c l|c|}
%     \hline
%     \multicolumn{3}{|c|}{\textbf{Construct}} & \multicolumn{1}{c|}{\textbf{Description}} \\\hline \hline
%     \multicolumn{3}{|c|}{\textbf{Types}} & \\ \cline{1-3}
%     %A,B\ ::=\ \tbool~|~\Atoms~|~\Fns~|~A× B
%     $A, B$ & \mbox{::=} & \; $\tbool$ \mmid $\Atoms$ \mmid $\Fns$ & \grammarcomment{Base Types} \\
%     & & \mmid $A × B$ & \grammarcomment{Product types} \\[1em] \hline \hline

%     \multicolumn{3}{|c|}{\textbf{Expressions}} & \\ \cline{1-3}
%     \multicolumn{3}{|l|}{\textbf{Values:}} & \\
%     $v, w$ & \mbox{::=} & \; $\itrue$ \mmid $\ifalse$ \mmid $x$& \grammarcomment{Booleans and Variables} \\
%     & & \mmid $(v,w)$ & \grammarcomment{Product} \\
%     \multicolumn{3}{|l|}{\textbf{Computations:}} & \\
%     $u, t$ & \mbox{::=} & \; $\ireturn(v)$ \mmid $\iletin x u t$ & \grammarcomment{Return and Let} \\
%     & & \mmid $\ite v u t$ \mmid $\imatch v {(x,y)} t$ & \grammarcomment{Eliminators} \\
%     & & \mmid $\iflip$ & \grammarcomment{Bernoulli trial with bias $θ$} \\
%     & & \mmid $\ifresh$ \mmid $v=w$ & \grammarcomment{Atoms: Fresh generation and Equality test} \\
%     & & \mmid $\lambdamem x u$ \mmid $v@w$ & \grammarcomment{Memoized functions: Abstraction and Application} \\[1em] \hline \hline

%     \multicolumn{4}{|c|}{\textbf{Typing judgements}} \\ \hline
%     \multicolumn{4}{|l|}{\textbf{Typed values:}} \\
%     \multicolumn{4}{|c|}{
%       \begin{prooftree}
%         \hypo{-}
%         \infer1{\vj{Γ}\itrue \tbool}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{-}
%         \infer1{\vj{Γ}\ifalse \tbool}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{-}
%         \infer1{\vj{Γ,x:A}x A}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{\vj{Γ}v A}
%         \hypo{\vj{Γ}w B}
%         \infer2{\vj{Γ}{(v,w)} {A× B}}
%       \end{prooftree}}
%     \\[2em]
% \multicolumn{4}{|l|}{\textbf
%     {Typed computations:}} \\[1em]
%     \multicolumn{4}{|c|}{
%       \begin{prooftree}
%         \hypo{\vj{Γ}v A}
%         \infer1{\cj{Γ}{\ireturn(v)} A}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{\cj{Γ}u A}
%         \hypo{\cj{Γ,x:A}t B}
%         \infer2{\cj{Γ}{\iletin x u t} B}
%       \end{prooftree}
%     }\\[1.5em]
%     \multicolumn{4}{|c|}{
%       \begin{prooftree}
%         \hypo{\vj{Γ}v \tbool}
%         \hypo{\cj{Γ}u A}
%         \hypo{\cj{Γ}t A}
%         \infer3{\cj{Γ}{\ite v u t} A}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{\vj{Γ}v {A× B}}
%         \hypo{\cj{Γ,x:A,y:B}t C}
%         \infer2{\cj{Γ}{\imatch v {(x,y)} t} C}
%       \end{prooftree}
%     }\\[1.5em]
%     \multicolumn{4}{|c|}{
%       \begin{prooftree}
%         \hypo{-}
%         \infer1{\cj{Γ}{\iflip} \tbool}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{-}
%         \infer1{\cj{Γ}{\ifresh} \Atoms}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{\vj{Γ}v \Atoms}
%         \hypo{\vj{Γ}w \Atoms}
%         \infer2{\cj{Γ}{(v=w)} \tbool}
%       \end{prooftree}
%     }\\[1.5em]
%     \multicolumn{4}{|c|}{
%       \begin{prooftree}
%         \hypo{\cj{Γ,x:\Atoms}u \tbool}
%         \infer1{\cj{Γ}{\lambdamem x u} \Fns}
%       \end{prooftree}
%       \qquad
%       \begin{prooftree}
%         \hypo{\vj{Γ}v \Fns}
%         \hypo{\vj{Γ}w \Atoms}
%         \infer2{\cj{Γ}{(v@w)} \tbool}
%       \end{prooftree}
%     }\\[1.5em]
%   \hline
%   \end{tabular}

%     \caption{Grammar and a typing rules of the language}
%     \label{fig:language}
% \end{figure*}

\begin{longtable}{|l c l|}
\caption{Grammar and typing rules of the language} \label{fig:language}\\
\hline
\multicolumn{3}{|c|}{\textbf{Types}} \\

% \hline
% \endfirsthead
% \hline
% \multicolumn{3}{|c|}{} \\[-2ex]
% \endhead
% \multicolumn{3}{|c|}{} \\[-2ex]
% \hline
% \multicolumn{3}{|c|}{\textit{Continued on next page}}\\
% \hline
% \endfoot
% \hline
% \endlastfoot
% \hline

\hline
\endfirsthead
\hline
\endhead
\hline
\endfoot
\endlastfoot

$A, B$ & \mbox{::=} & \; $\tbool$ \mmid $\Atoms$ \mmid $\Fns$ \mmid $A × B$ \\ \hline \hline
\multicolumn{3}{|c|}{\textbf{Expressions}} \\
\hline
\multicolumn{3}{|l|}{\textbf{Values:}} \\[-.5em]
$v, w$ & \mbox{::=} & \; $\itrue$ \mmid $\ifalse$ \mmid $x$ \mmid $(v,w)$ \\
\multicolumn{3}{|l|}{\textbf{Computations:}} \\[-.5em]
$u, t$ & \mbox{::=} & \; $\ireturn(v)$ \mmid $\iletin x u t$ \mmid $\ite v u t$ \mmid $\imatch v {(x,y)} t$ \\
& & \mmid $\iflip$ \mmid $\ifresh$ \mmid $v=w$ \mmid $\lambdamem x u$ \mmid $v@w$ \\[.5em] \hline \hline

\multicolumn{3}{|c|}{\textbf{Typing judgements}} \\ \hline
\multicolumn{3}{|l|}{\textbf{Typed values:}} \\
\multicolumn{3}{|c|}{
\begin{prooftree}
\hypo{-}
\infer1{\vj{Γ}\itrue \tbool}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{-}
\infer1{\vj{Γ}\ifalse \tbool}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{-}
\infer1{\vj{Γ,x:A, Γ'}x A}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\vj{Γ}v A}
\hypo{\vj{Γ}w B}
\infer2{\vj{Γ}{(v,w)} {A× B}}
\end{prooftree}}\\[1em]
\multicolumn{3}{|l|}{\textbf
{Typed computations:}} \\[.5em]
\multicolumn{3}{|c|}{
\begin{prooftree}
\hypo{\vj{Γ}v A}
\infer1{\cj{Γ}{\ireturn(v)} A}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\cj{Γ}u A}
\hypo{\cj{Γ,x:A}t B}
\infer2{\cj{Γ}{\iletin x u t} B}
\end{prooftree}
\multicolumn{3}{|c|}{
\begin{prooftree}
\hypo{\vj{Γ}v \tbool}
\hypo{\cj{Γ}u A}
\hypo{\cj{Γ}t A}
\infer3{\cj{Γ}{\ite v u t} A}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\vj{Γ}v {A× B}}
\hypo{\cj{Γ,x:A,y:B}t C}
\infer2{\cj{Γ}{\imatch v {(x,y)} t} C}
\end{prooftree}
\multicolumn{3}{|c|}{
\begin{prooftree}
\hypo{-}
\infer1{\cj{Γ}{\iflip} \tbool}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{-}
\infer1{\cj{Γ}{\ifresh} \Atoms}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\vj{Γ}v \Atoms}
\hypo{\vj{Γ}w \Atoms}
\infer2{\cj{Γ}{(v=w)} \tbool}
\end{prooftree}
\multicolumn{3}{|c|}{
\begin{prooftree}
\hypo{\cj{Γ,x:\Atoms}u \tbool}
\infer1{\cj{Γ}{\lambdamem x u} \Fns}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\vj{Γ}v \Fns}
\hypo{\vj{Γ}w \Atoms}
\infer2{\cj{Γ}{(v@w)} \tbool}
\end{prooftree}
\hline
\end{longtable}

\section{Operational Semantics}
\label{sec:operational}

We now present a small-step operational semantics for our language.  The operational semantics defines the rules for reducing program expressions, which form the basis for understanding the behavior of programs written in the language. Henceforth, we fix a countable set of variables $x, y, z, … ∈ $, and consider the terms up to $α$-equivalence for the $$ operator. Since we focus on functions with boolean codomain, our partial memo-tables are represented as partial bigraphs (bipartite graphs).

\begin{definition}[Partial bigraph]\label{def:bigraph}
A partial bigraph $𝖌 ≝ (𝖌_L, 𝖌_R, E)$ is a finite bipartite graph where the edge relation $E：𝖌_L × 𝖌_R → \{\itrue, \ifalse, ⊥\}$ is either true, false or undefined ($⊥$) on each pair of left and right nodes $(ƒ, a) ∈ 𝖌_L × 𝖌_R$. In the following, left nodes will be thought of as function labels and right nodes as atom labels.
By abuse of notation, syntactic truth values will be conflated with semantic ones. For a partial graph $𝖌$, $E(ƒ, a) = β ∈ \{\itrue, \ifalse, ⊥\}$ will be written $ƒ \xto {β} a$ when $𝖌$ is clear from the context.
\end{definition}

\subsection{Extended expressions}

We introduce extended expressions $e$, by extending the grammar of computations (\ref{fig:language}) with an extra construct $u$, where $u$ is a computation,$(ƒ, a)$ is a pair of function and atom labels to memoize, and $γ$ is the environment to restore after the result of $ƒ$ at $a$ has been computed and stored.
Intuitively, the decoration $-$ is thought of as a memoization context, indicating expressions where memoization should happen: $u$ is a computation that memoizes the result of $u$, and then restores the environment to the state it was in before the computation $u$ was evaluated.
In the following, $Δ ∈ ⋃_n ≥ 0 (𝖌_L × 𝖌_R)^n$ is a finite stack of function--atom label pairs, indicating that we are in the process of computing the result of these functions at these atoms for the first time. Each newly introduced function--atom label pair is assumed not to already belong to the memoization stack.

% \setlength{\tabcolsep}{1em}
% \setlength{\extrarowheight}{2pt}
% \centering
\begin{longtable}{|c c|}
\caption{Extended expression typing rules. }\label{fig:extended_expressions}\\
\hline
\multicolumn{2}{|c|}{\textbf{Extended expression typing judgements.} Here, $(ƒ, a) ∉ Δ ∪ Δ_1 ∪ Δ_2$.}\\

\hline
\multicolumn{2}{|c|}{} \\[-2ex]
\endfirsthead
\hline
\multicolumn{2}{|c|}{} \\[-2ex]
\endhead
\hline
\endfoot
\hline
\endlastfoot

\begin{prooftree}
\hypo{\cj{Γ} u A}
\infer1{\cje{Γ} {∅} u A}
\end{prooftree}
\qquad
\begin{prooftree}
\hypo{\cje{Γ} {Δ} u A}
\infer1{\cje{Γ} {(ƒ, a), Δ} {\memobraces{u}} A}
\end{prooftree}
\begin{prooftree}
\hypo{\cje {Γ} {Δ_1} u A}
\hypo{\cje {Γ,x:A} {Δ_2} t B}
\infer2{\cje {Γ} {Δ_1, Δ_2} {\iletin x u t} B}
\end{prooftree}
\\[1.5em]
\begin{prooftree}
\hypo{\cje {Γ} {Δ_1} u A}
\hypo{\cje {Γ,x:A} {Δ_2} t B}
\infer2{\cje {Γ} {(ƒ, a), Δ_1, Δ_2} {\iletin x {\memobraces{u}} t} B}
\end{prooftree}
\begin{prooftree}
\hypo{\cje {Γ} {Δ_1} u A}
\hypo{\cje {Γ,x:A} {Δ_2} t B}
\infer2{\cje {Γ} {(ƒ, a), Δ_1, Δ_2} {\iletin x u {\memobraces{t}}} B}
\end{prooftree}\\[1.5em]
\multicolumn{2}{|c|}{
\begin{prooftree}
\hypo{\vj{Γ}{v}{\tbool}}
\hypo{\cje{Γ}{Δ_1}{u}{A}}
\hypo{\cje{Γ}{Δ_2}{t}{A}}
\infer3{\cje{Γ}{Δ_1,Δ_2}{\ite v u t} A}
\end{prooftree}}\\[1.5em]
\begin{prooftree}
\hypo{\vj{Γ}{v}{\tbool}}
\hypo{\cje{Γ}{Δ_1}{u}{A}}
\hypo{\cje{Γ}{Δ_2}{t}{A}}
\infer3{\cje{Γ}{(ƒ, a),Δ_1,Δ_2}{\ite v {\memobraces{u}} t} A}
\end{prooftree}
\begin{prooftree}
\hypo{\vj{Γ}{v}{\tbool}}
\hypo{\cje{Γ}{Δ_1}{u}{A}}
\hypo{\cje{Γ}{Δ_2}{t}{A}}
\infer3{\cje{Γ}{(ƒ, a),Δ_1,Δ_2}{\ite v u {\memobraces{t}}} A}
\end{prooftree}\\[1.5em]
\begin{prooftree}
\hypo{\vj{Γ}{v}{A × B}}
\hypo{\cje{Γ,x:A,y:B}{Δ}{t}{C}}
\infer2{\cje{Γ}{Δ}{\imatch v {(x,y)} t} C}
\end{prooftree}
\begin{prooftree}
\hypo{\vj{Γ}{v}{A × B}}
\hypo{\cje{Γ,x:A,y:B}{Δ}{t}{C}}
\infer2{\cje{Γ}{(ƒ, a), Δ}{\imatch v {(x,y)} {\memobraces{t}}} C}
\end{prooftree}\\[1.5em]
%  \multicolumn{2}{|c|}{where $(ƒ, a) ∉ Δ ∪ Δ_1 ∪ Δ_2$}\\[.5em] \hline
\end{longtable}

% \begingroup
% \allowdisplaybreaks
% \begin{alignat*}{2}
%   &\begin{prooftree}
%     \hypo{\cj{Γ} u A}
%     \infer1{\cje{Γ} {∅} u A}
%   \end{prooftree} \qquad \qquad &&
%   \begin{prooftree}
%     \hypo{\cje{Γ} {Δ} u A}
%     \infer1[$(ƒ, a) ∉ Δ$]{\cje{Γ} {(ƒ, a), Δ} {\memobraces{u}} A}
%   \end{prooftree}\\[2.5em]
%   &\begin{prooftree}
%     \hypo{\cje {Γ} {Δ_1} u A}
%     \hypo{\cje {Γ,x:A} {Δ_2} t B}
%   \infer2{\cje {Γ} {Δ_1, Δ_2} {\iletin x u t} B}
%   \end{prooftree} \span\span\\[1.5em]
%   & &&\begin{prooftree}
%     \hypo{\cje {Γ} {Δ_1} u A}
%     \hypo{\cje {Γ,x:A} {Δ_2} t B}
%     \infer2[$(ƒ, a) ∉ Δ_1 ∪ Δ_2$]{\cje {Γ} {(ƒ, a), Δ_1, Δ_2} {\iletin x {\memobraces{u}} t} B}
%   \end{prooftree} \\[1.5em]
%   & &&
%   \begin{prooftree}
%   \hypo{\cje {Γ} {Δ_1} u A}
%   \hypo{\cje {Γ,x:A} {Δ_2} t B}
%   \infer2[$(ƒ, a) ∉ Δ_1 ∪ Δ_2$]{\cje {Γ} {(ƒ, a), Δ_1, Δ_2} {\iletin x u {\memobraces{t}}} B}
%   \end{prooftree}\\[2.5em]
%   & \begin{prooftree}
%   \hypo{\vj{Γ}{v}{\tbool}}
%   \hypo{\cje{Γ}{Δ_1}{u}{A}}
%   \hypo{\cje{Γ}{Δ_2}{t}{A}}
%   \infer3{\cje{Γ}{Δ_1,Δ_2}{\ite v u t} A}
%   \end{prooftree}\span\span\\[1.5em]
%   & &&
%   \begin{prooftree}
%     \hypo{\vj{Γ}{v}{\tbool}}
%     \hypo{\cje{Γ}{Δ_1}{u}{A}}
%     \hypo{\cje{Γ}{Δ_2}{t}{A}}
%     \infer3[$(ƒ, a) ∉ Δ_1 ∪ Δ_2$]{\cje{Γ}{(ƒ, a),Δ_1,Δ_2}{\ite v {\memobraces{u}} t} A}
%   \end{prooftree}\\[2.5em]
%   & &&
%   \begin{prooftree}
%     \hypo{\vj{Γ}{v}{\tbool}}
%     \hypo{\cje{Γ}{Δ_1}{u}{A}}
%     \hypo{\cje{Γ}{Δ_2}{t}{A}}
%     \infer3[$(ƒ, a) ∉ Δ_1 ∪ Δ_2$]{\cje{Γ}{(ƒ, a),Δ_1,Δ_2}{\ite v u {\memobraces{t}}} A}
%   \end{prooftree}\\[2.5em]
%   &\begin{prooftree}
%     \hypo{\vj{Γ}{v}{A × B}}
%     \hypo{\cje{Γ,x:A,y:B}{Δ}{t}{C}}
%     \infer2{\cje{Γ}{Δ}{\imatch v {(x,y)} t} C}
%   \end{prooftree}\span\span\\[1.5em]
%   & &&
%   \begin{prooftree}
%     \hypo{\vj{Γ}{v}{A × B}}
%     \hypo{\cje{Γ,x:A,y:B}{Δ}{t}{C}}
%     \infer2[$(ƒ, a) ∉ Δ$]{\cje{Γ}{(ƒ, a), Δ}{\imatch v {(x,y)} {\memobraces{t}}} C}
%   \end{prooftree}
% \end{alignat*}
% \endgroup

\subsection{Configurations}

We now define the set-theoretic interpretation of contexts. Context values are built by combining booleans, atomic names and functions using pairing. Thus a context value is a tree, where the branches are understood as pairing.

\begin{definition}
If $S$ is a finite set, $\Tree[S] ≅ \biguplus_{ n ≥ 0} C_n \, S^{n+1}$ (where $C_n$ is the $n$-th Catalan number, and $C_n \, S^{n+1}$ is a coproduct of $n$ copies of $S^{n+1}$, one for each possible bracketing) denotes the set of all possible non-empty trees with internal nodes the cartesian product and leaf nodes taken in $S$.
\begin{example}
If $S ≝ \{s_1, s_2\}$, then $s_1 ∈ \Tree[S], (s_2, s_1) ∈ \Tree[S], (s_1, (s_1, s_2)) ∈ \Tree[S], …$
\end{example}
\end{definition}

\begin{definition}[Set-theoretic denotation of contexts.]
Let $𝖌$ be a partial bigraph. The set-theoretic denotation $\denpar { - }$ of a context $Γ$
is defined as $\denpar {\tbool} ≝ 2 ≅ \{ \itrue, \, \ifalse\}, \, \denpar {\Fns} ≝ 𝖌_L, \, \denpar {\Atoms} ≝ 𝖌_R$ and $\denpar {-}$ is readily extended to every context $Γ$. Moreover, in the following, $γ ∈ \denpar {Γ} ⊆ \Tree^{\Var}$ denotes a context value.
\end{definition}

\begin{example} If $Γ ≝ (x: \tbool, y: \Fns, z: ((\Fns × 2) × \Atoms))$, then $\denpar {Γ} ≝ \{ x ↦ 2, y ↦ 𝖌_L, z ↦ ((𝖌_L × 2) × 𝖌_R)$ and an example of a context value is $γ ≝ \{ x ↦ \itrue, y ↦ ƒ_0, z ↦ ((ƒ_1, \itrue), a_0)\}$.
\end{example}

We now present terminal computations, redexes, reduction contexts, and configurations (\cref{fig:configurations}). Configurations encapsulate the computation state (a context value, an extended expression, a partial graph, and a map from the partial graph to closures), which helps keep track of different parts of the program as the computation proceeds.

% Let us now introduce terminal computations, redexes, reduction contexts, and configurations (\cref{fig:configurations}). Configurations provide a complete description of the state of the computation, including the context value, extended expression, partial graph, and a mapping from the partial graph to closures. These components help keep track of different parts of the program as the computation proceeds.

% \setlength{\tabcolsep}{1em}
% % \setlength{\extrarowheight}{2pt}
% \centering
% \vspace{-.12em}
\begin{longtable}{|l c l|}
\caption{Terminal computations, redexes, reduction contexts, and configurations.}
\label{fig:configurations}\\
\hline
\multicolumn{3}{|c|}{\textbf{Terminal computations $r$, Redexes $ρ$, and Reduction contexts $\C[-]$}} \\

\hline
\endfirsthead
\hline
\multicolumn{3}{|c|}{} \\[-2ex]
\endhead
\hline
\endfoot
\endlastfoot

$r$ & \mbox{::=} & \; $\ireturn(v)$ \mmid $\lambdamem x u$ \mmid $\ifresh$ \\
% \hline \hline

% \multicolumn{3}{|c|}{\textbf{Redexes $ρ$}} \\ \cline{1-3}
$ρ$ & \mbox{::=} & \; $\iletin x r u$  \mmid $\memobraces{\ireturn (v)}$ \qquad where $ƒ ∈ 𝖌_L,\; a ∈ 𝖌_R,\; γ ∈ \Tree^{\Var}$\\
& & \mmid $\imatch v {(x,y)} t$ \mmid $\ite v t u$  %\\
%& &
\mmid $\iflip$ \mmid $(v=w)$ \mmid $(v@w)$ \\
%&\multicolumn{2}{l|}{where $ƒ ∈ 𝖌_L,\; a ∈ 𝖌_R,\; γ ∈ \Tree^{\Var}$}\\
% \hline \hline

% \multicolumn{3}{|c|}{\textbf{Reduction contexts $\C[-]$}} \\ \cline{1-3}
$\C[-]$ & \mbox{::=} & \; $[-]$ \mmid $\iletin x {\C[-]} u$ \mmid $\memobraces{\C[-]}$ \\[.3em]
\hline

\multicolumn{3}{|c|}{\textbf{Configurations $(γ, u, 𝖌, λ)$}} \\
\cline{1-3}
% % \multicolumn{3}{|c|}{$(γ, u, 𝖌, λ)$}\\
&\multicolumn{2}{l|}{$γ ∈ \Tree^\Var$ is a context value.} \\
&\multicolumn{2}{l|}{$u$ is an extended expression $\cje{Γ}{Δ}{u}{A}$.} \\
&\multicolumn{2}{l|}{$𝖌 ≝ (𝖌_L, 𝖌_R, E)$ is a partial graph.} \\
&\multicolumn{2}{l|}{$λ：𝖌_L → \Closures$, where $\Closures ≝ \big\{ (\lambdamem x u, γ) \;\mid\; \cj{Γ}{\lambdamem x u}{\Fns} \text{ and } γ ∈ \denpar{Γ}\big\}$}\\\hline
\end{longtable}

\subsection{Reduction rules}

Let $[γ]-$ be the function evaluating an expression value in a context value $γ$ (\eg $[γ]x = γ(x), [γ] = $, etc). %and $\Ty$ be the one returning the type of such evaluations (\eg $\Ty(\denpar[γ]{\itrue}) = \tbool, \Ty(\denpar[γ]{(\itrue, \ifalse)}) = \tbool × \tbool$, etc). We also define a function $\Ctxt：\Tree^\Var ⟶ \Contexts$ associating to every context value $γ$ its corresponding context: $\Ctxt(γ)≝ \big(x: \Ty(\denpar[γ]{x})\big)_{x \,∈\, \supp(γ)}$, where $\supp(γ)$ is the support of $γ$.

We can define the operational semantics of the language using reduction rules. They provide a step-by-step description of how expressions are evaluated and transformed during execution, following a left-most outer-most strategy, with lexical binding. Given a configuration $(γ, u, 𝖌, λ)$ (note that if $u$ is of the form $u'[(ƒ, a)][γ]$, then it is assumed that the function--atom label pair $(ƒ, a) ∈ 𝖌_L × 𝖌_R$), we will apply the following reduction rules:

% \setlength{\extrarowheight}{2pt}
% \renewcommand{\arraystretch}{1.8}
\begin{longtable}{|l c l|}
\caption{Reduction rules.} \\
\hline
\multicolumn{3}{|c|}{\textbf{Reduction Rules}}\\
\hline
\endfirsthead
\hline
\multicolumn{3}{|c|}{} \\[-1.5ex]
% \multicolumn{3}{|c|}{\textbf{Reduction Rules (Continued)}}\\
% \hline
\endhead
\multicolumn{3}{|c|}{} \\[-1.5ex]
\hline
\multicolumn{3}{|c|}{\textit{Continued on next page}}\\
\hline
\endfoot
\hline
\endlastfoot
\hline
\multicolumn{3}{|c|}{} \\[-1.5ex]
$(γ, \iletin{x}{\ireturn(v)}{u}, 𝖌, λ)$ & $⟶$ & $(γ ⨆ \{ x ↦ \denpar[γ]{v}\}, u, 𝖌, λ)$ \\
$(γ, \memobraces{\ireturn(v)}[(ƒ, a)][γ'], 𝖌, λ)$ & $⟶$ & $\begin{cases}
(γ', \ireturn(\denpar[γ]{v}), (𝖌_L, 𝖌_R, E ∪ \{ ƒ \xto{\denpar[γ]{v}} a \}), λ)\\
\hspace{7em} \quad\text{ if } \denpar[γ]{v} ∈ \{\itrue, \ifalse\}\\
\text{ else, failure (cannot memoize a non-boolean function)}\\
\end{cases}$ \\
$(γ, \iletin{x}{\lambdamem y u}{t}, 𝖌, λ)$ & $⟶$ & $\big(γ ⨆ \{ x ↦ ƒ\}, t, (𝖌_L ⨆ \{ ƒ\}, 𝖌_R, E ⨆ \{ f \xto {⊥} a \}_{a ∈ 𝖌_R}),$ \\
&& \hphantom{$\big(γ ⨆ \{ x ↦ ƒ\}, t, $} $λ ⨆ \{ ƒ ↦ (\lambdamem y u, γ)\}\big)$ \\
$(γ, \iletin{x}{\ifresh}{t}, 𝖌, λ)$ & $⟶$ & $\big(γ ⨆ \{ x ↦ a\}, t,$ \\
&& \hphantom{$\big(γ ⨆ \{ x ↦ $} $(𝖌_L, 𝖌_R ⨆ \{ a\}, 𝖌_R, E ⨆ \{ ƒ \xto {⊥} a \}_{ƒ ∈ 𝖌_L}), λ\big)$ \\
$(γ, (v@w), 𝖌, λ)$ & $⟶$ & $\begin{cases}
(γ, \ireturn(β), 𝖌, λ) \quad\text{ if } β ≝ E(\denpar[γ]{v}, \denpar[γ]{w}) ≠ ⊥\\
(γ_0 ⨆ \{ y ↦ \denpar[γ]{w}\}, \memobraces{u}, 𝖌, λ) \quad\text{ else,}\\
\hspace{7em}\text{where } λ(\denpar[γ]{v}) ≝ (\lambdamem y u, γ_0)
\end{cases}$ \\
$(γ, v = w, 𝖌, λ)$ & $⟶$ & $(γ, \ireturn(β), 𝖌, λ) \text{ where } β ≝ (\denpar[γ]{v} = \denpar[γ]{w})$ \\
$(γ, \iflip, 𝖌, λ)$ &$\overset{\text{\tiny with proba. } θ}{⟶}$& $(γ, \ireturn(β), 𝖌, λ) \quad\text{ where } β ∈ \{ \itrue, \ifalse\}$ \\
$(γ, \imatch v {(x,y)} t, 𝖌, λ)$ & $⟶$ & $(γ ⨆ \{ x ↦ \denpar[γ]{v}, y ↦ \denpar[γ]{w}\}, t, 𝖌, λ)$ \\
$(γ, \ite v t u)$ & $⟶$ & $\begin{cases}
(γ, t, 𝖌, λ) \qquad\text{ if } v = \itrue\\
(γ, u, 𝖌, λ) \qquad\text{else, if } v = \ifalse
\end{cases}$ \\
\multicolumn{3}{|c|}{} \\
\multicolumn{3}{|c|}{$\dfrac{(γ, e, 𝖌, λ) ⟶ (γ', e', 𝖌', λ')}{(γ, \C[e], 𝖌, λ) ⟶ (γ', \C[e'], 𝖌', λ')}$} \\[1.5em]
\hline
\end{longtable}

% \paragraph*{Reduction rules:}
% \begingroup
% \addtolength{\jot}{0.8em}
% \allowdisplaybreaks
% \begin{alignat*}{2}
%   &(γ, \iletin{x}{\ireturn(v)}{u}, 𝖌, λ) &&⟶ (γ ⨆ \{ x ↦ \denpar[γ]{v}\}, u, 𝖌, λ) \\
%   &(γ, \memobraces{\ireturn(v)}[(ƒ, a)][γ'], 𝖌, λ) &&⟶ (γ', \ireturn(\denpar[γ]{v}), (𝖌_L, 𝖌_R, E ∪ \{ ƒ \xto{\denpar[γ]{v}} a \}), λ) \\
%   &(γ, \iletin{x}{\lambdamem y u}{t}, 𝖌, λ) &&⟶ \big(γ ⨆ \{ x ↦ ƒ\}, t, (𝖌_L ⨆ \{ ƒ\}, 𝖌_R, E ⨆ \{ f \xto {⊥} a \}_{a ∈ 𝖌_R}), \\[-.8em]
%   & && \hphantom{⟶} \quad λ ⨆ \{ ƒ ↦ (\lambdamem y u, γ)\}\big) \\
%   &(γ, \iletin{x}{\ifresh}{t}, 𝖌, λ) &&⟶ \big(γ ⨆ \{ x ↦ a\}, t, \\[-.8em]
%     & && \hphantom{⟶} \quad (𝖌_L, 𝖌_R ⨆ \{ a\}, 𝖌_R, E ⨆ \{ ƒ \xto {⊥} a \}_{ƒ ∈ 𝖌_L}), λ\big)\\
%   &(γ, (v@w), 𝖌, λ) &&⟶ \begin{cases}
%     (γ, \ireturn(β), 𝖌, λ) \quad\text{ if } β ≝ E(\denpar[γ]{v}, \denpar[γ]{w}) ≠ ⊥\\
%     (γ_0 ⨆ \{ y ↦ \denpar[γ]{w}\}, \memobraces{u}, 𝖌, λ) \quad\text{ else,}\\
%     \smash{\hspace{7em}\text{where } λ(\denpar[γ]{v}) ≝ (\lambdamem y u, γ_0)}
%   \end{cases}\\
%   &(γ, v = w, 𝖌, λ) &&⟶ (γ, \ireturn(β), 𝖌, λ) \text{ where } β ≝ (\denpar[γ]{v} = \denpar[γ]{w})\\
%   &(γ, \iflip, 𝖌, λ) \quad&&\hspace{-1em}\overset{\text{\tiny with proba $θ$}}{⟶} (γ, \ireturn(β), 𝖌, λ) \quad\text{ where } β ∈ \{ \itrue, \ifalse\}\\
%   &(γ, \imatch v {(x,y)} t, 𝖌, λ) &&⟶ (γ ⨆ \{ x ↦ \denpar[γ]{v}, y ↦ \denpar[γ]{w}\}, t, 𝖌, λ)\\
%   &(γ, \ite v t u) &&⟶ \begin{cases}
%     (γ, t, 𝖌, λ) \qquad\text{ if } v = \itrue\\
%     (γ, u, 𝖌, λ) \qquad\text{else, if } v = \ifalse
%     \end{cases}\\
%   &\hspace{1em}\cfrac{(γ, e, 𝖌, λ) ⟶ (γ', e', 𝖌', λ')}{(γ, \C[e], 𝖌, λ) ⟶ (γ', \C[e'], 𝖌', λ')}\span\span
% \end{alignat*}
% \endgroup

%%%%% EXAMPLE
% \begingroup
% \allowdisplaybreaks
% \begin{example}\begin{align*}
%   &\Big(∅, \quad \iletin{x_0}{\ifresh}{\\
%   & \qquad \;\; \iletin{f_1}{\lambdamem{x}{(\iletin{b}{(x = x_0)}{\ireturn(b)})}}{\\
%   & \qquad \;\; \iletin{f_2}{\lambdamem{y}{f_1 @ y}}{f_2 @ x_0}}},\\
%   & \quad (∅, ∅, ∅),\; ∅\Big)  \\[1em]
%   ⟶ &\Big(\{x_0 ↦ a_0\}, \quad \iletin{f_1}{\lambdamem{x}{(\iletin{b}{(x = x_0)}{\ireturn(b)})}}{\\
%   & \qquad \qquad \qquad \;\; \iletin{f_2}{\lambdamem{y}{f_1 @ y}}{f_2 @ x_0}},\\
%   & \quad (∅, \{a_0\}, ∅),\; ∅\Big)  \\[1em]
%   ⟶^2  & \Big(\overbrace{\{x_0 ↦ a_0,\, f_1 ↦ ƒ_1,\, f_2 ↦ ƒ_2\}}^{≝ \, γ_0},\quad f_2 @ x_0, \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\[1em]
%   & \quad \big\{ƒ_1 ↦ (\lambdamem{x}{(\iletin{b}{(x = x_0)}{\ireturn(b)})}, \{x_0 ↦ a_0\}),\\
%   & \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)\\[1em]
%   ⟶  & \Big(\overbrace{\{x_0 ↦ a_0,\, f_1 ↦ ƒ_1, \, y ↦ a_0\}}^{≝ \, γ_1},\quad \memobraces{f_1 @ y}[ƒ_2, a_0][γ_0], \\
%   & \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
%   & \quad \big\{ƒ_1 ↦ (\lambdamem{x}{(\iletin{b}{(x = x_0)}{\ireturn(b)})}, \{x_0 ↦ a_0\}), \\
%   & \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)\\[1em]
%   ⟶  & \Big(\{x_0 ↦ a_0,\, x ↦ a_0\},\quad \memobraces{\memobraces{\iletin{b}{(x = x_0)}{\ireturn(b)}}[ƒ_1, a_0][γ_1]}[ƒ_2, a_0][γ_0], \\
%   & \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
%   & \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{\ireturn(b)}}, \{x_0 ↦ a_0\}), \\
%   & \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)\\[1em]
%   ⟶^2  & \Big(\{x_0 ↦ a_0,\, x ↦ a_0, \, b ↦ \itrue\},\quad \memobraces{\memobraces{\ireturn(b)}[ƒ_1, a_0][γ_1]}[ƒ_2, a_0][γ_0], \\
%   & \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
%   & \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{\ireturn(b)}}, \{x_0 ↦ a_0\}), \\
%   & \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)\\[1em]
%   ⟶^2  & \Big(\overbrace{\{x_0 ↦ a_0,\, f_1 ↦ ƒ_1,\, f_2 ↦ ƒ_2\}}^{≝ \, γ_0},\quad \ireturn(\itrue), \\
%   & \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {\itrue} a_0, \,ƒ_2 \xto {\itrue} a_0\}), \\
%   & \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{\ireturn(b)}}, \{x_0 ↦ a_0\}), \\
%   & \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
% \end{align*}
% \end{example}
% \endgroup

\begin{example} We now give an example showcasing how these reduction rules apply on a program combining name generation, a coin flip, function abstraction, and stochastic memoization. An atom $x_0$ is generated and used as an argument for a function $f_1$, which performs a coin flip if the argument matches $x_0$. The outcome is then memoized and the result is returned in the second application. There are two execution traces, depending on the outcome of the coin flip ($β ∈ {\itrue, \ifalse}$).
\begingroup
\allowdisplaybreaks
\begin{longtable}{p{0.4\textwidth}p{0.1\textwidth}p{0.4\textwidth}}
&\Big(∅, \quad \iletin{x_0}{\ifresh}{\\
& \hspace{2.6em} \iletin{f_1}{\lambdamem{x}{(\iletin{b}{(x = x_0)}{}\\
& \hspace{8.5em} \ite b {\iflip[\tfrac 1 2]} {\ifalse})}}{\\
& \hspace{2.6em} \iletin{f_2}{\lambdamem{y}{f_1 @ y}}{f_2 @ x_0}}},\\
& \quad (∅, ∅, ∅),\; ∅\Big)
\end{aligned}$
& $\hspace{3em} ⟶$ &
&\Big(\{x_0 ↦ a_0\}, \\
& \hspace{1em}  \iletin{f_1}{\lambdamem{x}{(\iletin{b}{(x = x_0)}{}\\
& \hspace{6.9em} \ite b {\iflip[\tfrac 1 2]} {\ifalse})}}{}\\
& \hspace{1em} \iletin{f_2}{\lambdamem{y}{f_1 @ y}}{f_2 @ x_0},\\
& \quad (∅, \{a_0\}, ∅),\; ∅\Big)
\end{aligned}$ \\[1em]
⟶^2  & \Big(\overbrace{\{x_0 ↦ a_0,\, f_1 ↦ ƒ_1,\, f_2 ↦ ƒ_2\}}^{≝ \, γ_0},\quad f_2 @ x_0,\\
&\hspace{1em} (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\[1em]
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\\
& \hspace{4.4em} \ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}),\\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$
& $\hspace{3em} ⟶$ &
& \Big(\overbrace{\{x_0 ↦ a_0,\, f_1 ↦ ƒ_1, \, y ↦ a_0\}}^{≝ \, γ_1},\quad \memobraces{f_1 @ y}[ƒ_2, a_0][γ_0], \\
& \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\\
& \hspace{4.4em}\ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}), \\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$ \\[1em]
⟶  & \Big(\{x_0 ↦ a_0,\, x ↦ a_0\},\\
& \hspace{.5em} \Bigmemobraces{\bigmemobraces{\iletin{b}{(x = x_0)}{}\\[-.5em]
& \hspace{4.4em} \ite b {\iflip[\tfrac 1 2]} {\ifalse}}[ƒ_1, a_0][γ_1]}[ƒ_2, a_0][γ_0]\!\!\!, \\
& \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\\
&\hspace{4.4em}\ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}), \\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$
& $\hspace{3em} ⟶$ &
& \Big(\{x_0 ↦ a_0,\, x ↦ a_0, \, b ↦ \itrue\},\\
&\hspace{.5em}\memobraces{\memobraces{\ite b {\iflip[\tfrac 1 2]} {\ifalse}}[ƒ_1, a_0][γ_1]}[ƒ_2, a_0][γ_0]\!\!\!, \\
& \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\\
&\hspace{4.4em}\ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}), \\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$ \\[1em]
⟶  & \Big(\{x_0 ↦ a_0,\, x ↦ a_0, \, b ↦ \itrue\},\\
&\hspace{.5em}\memobraces{\memobraces{\iflip[\tfrac 1 2]}[ƒ_1, a_0][γ_1]}[ƒ_2, a_0][γ_0]\!\!\!, \\
& \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\\
&\hspace{4.4em}\ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}), \\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$
& $\hspace{2.3em} \overset{\text{\tiny proba. } \tfrac 1 2}{⟶}$ &
& \Big(\{x_0 ↦ a_0,\, x ↦ a_0, \, b ↦ \itrue\},\\
&\hspace{.5em}\memobraces{\memobraces{\ireturn(β)}[ƒ_1, a_0][γ_1]}[ƒ_2, a_0][γ_0]\!\!\!, \\
& \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {⊥} a_0, \,ƒ_2 \xto {⊥} a_0\}), \\
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\\
&\hspace{4.4em}\ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}), \\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$
\\[1em]
⟶^2  & \Big(\overbrace{\{x_0 ↦ a_0,\, f_1 ↦ ƒ_1,\, f_2 ↦ ƒ_2\}}^{≝ \, γ_0},\quad \ireturn(β), \quad (\{ƒ_1, ƒ_2\}, \;\{a_0\}, \{ƒ_1 \xto {β} a_0, \,ƒ_2 \xto {β} a_0\}), \\
& \quad \big\{ƒ_1 ↦ (\lambdamem{x}{\iletin{b}{(x = x_0)}{}\ite b {\iflip[\tfrac 1 2]} {\ifalse}}), \{x_0 ↦ a_0\}), \\
& \quad \, ƒ_2 ↦ (\lambdamem{y}{f_1 @ y}, \{x_0 ↦ a_0, f_1 ↦ ƒ_1\})\big\}\Big)
\end{aligned}$
\end{longtable}
\endgroup
\end{example}

\paragraph*{Configuration judgements.} We now show that the operational semantics satisfies the memoization equations \cref{eqn:stochmem}. Initial configurations are of the form $(∅, e, ∅, ∅)$, where $e$ is a non-extended expression. One can associate a \emph{configuration judgment} $(∅, e, ∅, ∅) ≝ ∅∅eA$ to every initial configuration. A configuration $(γ, e, 𝖌, λ)$ is said to be \emph{accessible} (from $(∅, e_0, ∅, ∅)$) if there exists a reduction trace $s = (∅, e_0, ∅, ∅) ⟶^∗(γ, e, 𝖌, λ)$ with probability $> 0$. The big-step operational semantics of an initial configuration is defined in a standard way as the resulting probability distribution over the set of configurations accessible from it. We can then prove that a configuration is accessible only if it has a corresponding configuration judgment that is derivable:

\begin{lemma}
If a configuration $(γ, e, 𝖌, λ)$ is accessible, there exists a corresponding \emph{configuration judgement} $\J(γ, e, 𝖌, λ) ≝ \cje{Γ}{Δ}{e}{A}$ where $γ ∈ \denpar{Γ}$ and such that $\J(γ, e, 𝖌, λ)$ is derivable (with \cref{fig:language,fig:extended_expressions}).
\end{lemma}

Due to the fact that we have at most one redex per (extended) expression and we do not have recursion (so the dataflow graph does not have self-loops and is acyclic), we can prove that:

\begin{lemma}
If a configuration of the form $(γ, \C[v@w], 𝖌, λ)$ is accessible and $E(\denpar[γ]{v}, \denpar[γ]{w}) = ⊥$, then $J(γ, \C[v@w], 𝖌, λ) ≝ \cje{Γ}{Δ}{\C[v@w]}{A}$ is such that the memoization stack $Δ$ does not contain a function--atom label pair with $\denpar[γ]{v}$ as first component.
\end{lemma}

As a corollary, we can then prove that a configuration is accessible only if its memoization stack has no duplicates:

\begin{lemma}
If a configuration $(γ, e, 𝖌, λ)$ is accessible and $\J(γ, e, 𝖌, λ) ≝ \cje{Γ}{Δ}{e}{A}$ is its corresponding configuration judgment, there is no duplicate in $Δ$.
\end{lemma}

This in turn enables us to ensure that the operational semantics satisfies the memoization equations:

\begin{proposition}
If $e_1$ and $e_2$ are programs of the form
\begin{align*}
e_1 &≝ \iletin x {\ifresh} {\iletin{f}{\lambdamem{y}{e}}{\iletin {v_1} {f @ x}{\iletin {v_2} {f @ x}{ \ireturn (v_1, v_2)}}}}\\
e_2 &≝ \iletin x {\ifresh} {\iletin{f}{\lambdamem{y}{e}}{\iletin {v_1} {f @ x}{\ireturn (v_1, v_1)}}}
\end{align*}
the configurations $(∅, e_1, ∅, ∅)$ and $(∅, e_2, ∅, ∅)$ have the same big-step operational semantics.
\end{proposition}

% $\begin{aligned}
%   &\iletin f{\lambdamem{y}{u}}{}\\
%   &\iletin {v_1} {f @ x }{}\\
%   &\iletin {v_2}{f@ x}{}\\
%   &\ireturn (v_1, v_2)\end{aligned}$ and
% $\begin{aligned}
%   &\iletin f{\lambdamem{y}{u}}{}\\
%   &\iletin {v_1} {f @ x }{}\\
%   &\ireturn (v_1, v_1)
% \end{aligned}$

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
%%% End:

\section{Denotational Semantics}
\label{sec:denotational-semantics}

In this section we propose a denotational model that verifies the dataflow property (Def.~\ref{eqn:dataflow}, Theorem~\ref{thm:probabilistic-local-state-monad-commutative-affine}) and which supports memoization of constant Bernoulli functions (Theorem~\ref{thm:T-mem}) and is sound with respect to the operational semantics of Section~\ref{sec:operational} (Theorem~\ref{thm:soundness}). Thus we show that criteria (1)--(5) of Section~\ref{sec:intro} are consistent.

The memo-tables in memoization are a kind of hidden or local state, and our semantic domain is similar to other models of local state \cite{plotkinNotionsComputationDetermine2002,poy-bi,melliesLocalStatesString2014,klms-ground-state-monad} in that it uses a possible worlds semantics in the guise of a functor category.

\begin{definition}
A \emph{total bigraph} is a partial bigraph (Def.~\ref{def:bigraph}) that does not have any undefined ($\bot$) elements. This represents a fully populated memo-table. We notate this $g=(g_L,g_R,E^g)$, omitting the superscript when it is clear.
An \emph{embedding} between total bigraphs $\iota\colon g\to g'$ is a pair of injections $(\iota_L: g_L\to g_L',\iota_R: g_R\to g_R'$) that do not add or remove edges ($E^g(ƒ, a)=E^{g'}(\iota_L(ƒ),\iota_R( a))$).
These can be thought of as conservative extensions of the memo-table.
We let $\BiG$ be the category where the objects are total finite bigraphs and graph embeddings.
\end{definition}

We will interpret our types as covariant presheaves, i.e.~functors in $[,]$, and programs will be interpreted as natural transformations. We discuss this category in Section~\ref{sec:presheaf-cat}, before defining a monad (\S\ref{sec:prob-loc-monad}) and giving a denotational semantics (\S\ref{sec:cat-semantics}) and proving a soundness theorem (\S\ref{sec:soundness}).

%One way to prove that stochastic memoization satisfies the dataflow property \hl{ref} is to exhibit a denotational model, which is what we do in this section, in a restricted setting. We develop the denotational semantics for our language based on memo-nominal sets. We also state the soundness of our denotational semantics with respect to the operational semantics.

\hide{Stochastic functions are usually interpreted as probabilistic kernels $f： X → PY$, where $P$ is a probability monad on a suitable category~\cite{fritz,kock}. A semantic model for stochastic memoization should then admit a cartesian closed structure (to model higher-order functions) and a morphism ${\mathop{\rm mem}}_{X, Y}：(PY)^X ⟶ P(Y^X)$.\todo{This was already said}
To prove that equations~(\ref{eqn:stochmem}) are consistent with the dataflow property~(\ref{eqn:dataflow}), we give a denotational model. For simplicity, we focus on Boolean-valued functions over a non-enumerable type of atoms~\cite{pittsNominalSetsNames2013}.\todo{This was already said} Our model is based on functors over finite bipartite graphs (\emph{bigraphs}, for short\todo{already said. but emphasise total}), see~\cite{kaddarModelStochasticMemoization2022,kaddarTransferReportExchangeability2022}\todo{Do we need to cite these?} %They might complain that they want the details here, not in a student report
for details. At a lower level, we have the following interface:

\begin{lstlisting}
new_atom :: *'$\mathbb{A}$'* -- Atoms (randomly generated fresh names)
new_function :: *'$\mathbb{F}$'* -- Function labels: type to be thought of as *'$\color{mygray}{\mathbb{A}}$'* -> Bool
(@) :: (*'$\mathbb{F}$'*, *'$\mathbb{A}$'*) -> Bool -- Application operator making every function memoized: type of a bigraph
\end{lstlisting}

where every function from a set of atoms $𝔸$ to \lstinline|Bool| is viewed as an inhabitant of type $𝔽$ (thought of as $𝔸 → \mlstinline{Bool}$). Applying a function to an argument and memoizing the result amounts to the explicit `apply' operator $\mlstinline{(@)}:: 𝔽 × 𝔸 → \mlstinline{Bool}$. But requiring that the results be memoized is precisely saying that $\mlstinline{@}$ ought to be seen as the `edge' relation of a bigraph with set $𝔽$ of left nodes and $𝔸$ of right nodes, the edges of which are such that their presence (or absence) remains unchanged after being sampled.\todo{Some of this has already been said} Inspired by the local state monad~\cite{plotkinNotionsComputationDetermine2002}, we model probabilistic and name generation effects by a new monad $T$ on $[\BiG, \Sets]$, where $\BiG$ is the category of finite bigraphs and embeddings. We then use it to give a categorical semantics to our language, and we show that $T$ is commutative and affine, and hence satisfies the dataflow property~(\ref{eqn:dataflow}).}
% like \lstinline|isEdge| in \lstinline|RandomGraph|.

% Similarly to the Rado topos setting~\hl{LICS paper ref}, this suggests that we are looking for a topos where a random countable bigraph would play the role of the Rado graph.

\subsection{Base category}\label{sec:presheaf-cat}

We work in the category $[, ]$ of covariant presheaves on the category $$ of finite bigraphs. The types of the language $A$ are interpreted as presheaves~$A$. The idea is that once some functions and atomic names are fixed, and a memo-table $g$ for them is given, then we can say what the values or expressions are, $A(g)$. The values can be renamed by permuting functions and atomic names, and are monotonic in that they remain unchanged when we conservatively extend the memo-table. This is the functorial action, $Aι: A(g)→A (g')$.
Programs will be interpreted as natural transformations: the naturality ensures that they are invariant under permuting the functions and atomic names, or extending the memo-table.

We write $∘$ and $∙$ for the one-vertex left and right graphs respectively. The denotation of basic types is given by:
\[
\den\Fns ≝ \BiG(\circ,-)\quad
\den\Atoms ≝ \BiG(\bullet,-)
\quad\text{so that }
\den\Fns(g) \cong g_L\text,\
\den\Atoms(g) \cong g_R\text.
\]
The presheaf category $[,]$ has products and coproducts, given pointwise~\cite{cwm}.
In particular, the denotation of the type of booleans is the constant presheaf $2 ≅ 1+1$.
%For a bigraph $g$ and a presheaf $X = \den{\mathcal{X}}$, $X(g)$ is thought of as the set of programs of type $\mathcal{X}$ that may use the bigraph $g$, in the following sense: probabilistic functions (that we want to memoize) and atom labels are stored as left and right nodes respectively. The presence (resp. absence) of an edge between a given left and right node memoizes the fact that a probabilistic call of the corresponding function on the corresponding atom has resulted in $\itrue$ (resp. $\ifalse$). For every embedding $ι：g ↪ g'$, the function $Xι：X(g) → X(g')$ models substitution in the programs in $X(g)$ according to $ι$.

The edge relations collect to form a natural transformation $ℰ:×→2$ given by $ℰ_g(ƒ, a) = E^g(ƒ, a)$.

The category $[,]$ is cartesian closed, as is any presheaf category. By currying $ℰ$,
we have an embedding of $$ in the function space $2^$, i.e.~$→2^$. In fact, in this development to keep things simpler, we will focus on $$ rather than the full function space $2^$.

%   The model will soon be refined to the subtopos of sheaves over $\BiG$ for the atomic Grothendieck topology, as discussed in \cref{sec:bipartite-random-graph-topos}. The sheaf condition expresses the fact that if two bigraphs $g_1, g_2$ have a common intersection $g$ and $x ∈ X(g_1) ∩ X(g_2)$, then the program $x$ can be regarded as only using $g$, so that $x ∈ X(g)$~\cite{statonNamepassingProcessCalculi}.

\subsection{Probabilistic local state monad}
\label{sec:prob-loc-monad}
In the following, $X, Y, Z：→ $ denote presheaves, $g = (g_L, g_R, E^g), g', h, h' ∈ $ bigraphs, and $ι, ι'：g ↪ g'$ bigraph embeddings. We will omit subscripts when they are clear from the context.

Let $$ be the finite distribution monad:
$(X)(g)= {p:X(g) → [0,1] |  𝗌𝗎𝗉𝗉(p) finite and ∑_x p(x)=1}$.
By considering the following `node-generation' monad $N(X)(g) ≝ _g  ↪  h X(h)$ on $[, ]$, one could be tempted to think that modeling name generation and stochastic memoization is a matter of composing these two monads. But this is not quite enough. We also need to remember, in the monadic computations, the probability of a function returning $$ for a fresh, unseen atom. To do so, inspired from Plotkin and Power's local state monad~\cite{plotkinNotionsComputationDetermine2002} (which was defined on the covariant presheaf category $[, ]$, where $$ is the category of ﬁnite sets and injections), we model probabilistic and name generation effects by the following monad, defined using a coend~\cite{cwm}, that we name `probabilistic local state monad':

\begin{definition}[Probabilistic local state monad]\label{def:probabilistic-local-state-monad}
For all covariant presheaves $X：\BiG → \Sets$ and bigraphs $g ∈ \BiG$:
\[
T(X)(g) \,≝\, \bigg(\Prfin \int^{g ↪ h} \Big( X(h)\times [0, 1]^{(h-g)_L}\Big)\bigg)^{[0,1]^{g_L}}
\]
\end{definition}

The monad $T$ is similar to the read-only local state monad, except that any fresh node can be initialized. Every $λ ∈ [0, 1]^g_L$ is thought of as the probability of the corresponding function/left node yielding true on a new fresh atom. We will refer to such a $λ$ as a \emph{state of biases}. The coend `glues together' the extensions of the memo-table that are compatible with the constraints imposed by the current computation. The monad allows manipulating probability distributions over such extensions, while keeping track of the probability of new nodes.

Equivalence classes in $∫^g ↪ h X(h)×[0, 1]^(h-g)_L$ are written $[x_h, λ^h]_g$. In the coend, the quotient can be thought of as taking care of garbage collection: nodes that are not used in the bigraph environment can be discarded. We use Dirac's bra-ket notation\footnote{popularized by Bart Jacobs for finite probability distributions~\cite{jacobs-new-directions}} $[x_h, λ^h]_g_h$ to denote a formal column vector of equivalence classes ranging over a finite set of $h$'s. As such, a formal convex sum $∑_i p_i [x_h_i, λ^h_i]_g ∈ ∫^g ↪ h X(h)×[0, 1]^(h-g)_L$ will be concisely denoted by $p⃗ | [x_h, λ^h]_g_h$.

\begin{definition}[Action of $T(X)$ on morphisms]
\[
T(X)(g \xinjto {ι} g')：\\
\begin{cases}
\displaystyle\Big(\Prfin \int^{g ↪ h} \mkern-30mu X(h)\times [0, 1]^{(h-g)_L}\Big)^{[0,1]^{g_L}}
⟶ \Big(\Prfin \int^{g' ↪ h'} \mkern-35mu X(h')\times [0, 1]^{(h'-g')_L}\Big)^{[0,1]^{g'_L}} \span\\
ϑ ↦ [0,1]^{g'_L} \xto {- \circ ι_L} [0,1]^{g_L} &\xto {ϑ} \Prfin \displaystyle\int^{g ↪ h} X(h)\times [0, 1]^{(h-g)_L} \\
&\xto{\Prfin ψ_{g, g'}} \Prfin \displaystyle\int^{g' ↪ h'} X(h')\times [0, 1]^{(h'-g')_L}
\end{cases}
\]

\begin{itemize}
\item $ι_L：g_L ↪ g_L'$ is the embedding restricted to left nodes, the maps $ψ_{g, g'}$ are given by:\,\\[1em]
\begin{prooftree}
\hypo{\begin{cases}
X(h)\times [0, 1]^{(h-g)_L} → X(h \pushout_g g')\times [0, 1]^{(h \pushout_g g' - g')_L} → \mathrlap{\int^{g' ↪ h'} X(h')\times [0, 1]^{(h'-g')_L}}\\
(x_h, \, λ^h) ⟼ (X(h ↪ h \pushout_g g')(x_h), \, λ^h) ⟼ \mathrlap{[X(h ↪ h \pushout_g g')(x_h), \, λ^h]_{g'}}\vphantom{\bigg|}
\end{cases}}
\infer1[extranatural in $h$]{\int^{g ↪ h} X(h)\times [0, 1]^{(h-g)_L} \xto{ψ_{g, g'}} \int^{g' ↪ h'} X(h')\times [0, 1]^{(h'-g')_L}}
\end{prooftree}\\[1em]
\item  and $h \pushout_g g'$ is the pushout in the category of graphs regarded as an object of $\BiG$.
\end{itemize}

More concretely, with Dirac's bra-ket notation, $T(X)(g \xinjto {ι} g')$ can be written as:
\[
T(X)(ι) =
\begin{cases}
\Big(\Prfin \int^{g ↪ h} X(h)\times [0, 1]^{(h-g)_L}\Big)^{[0,1]^{g_L}}
⟶ \Big(\Prfin \int^{g' ↪ h'} X(h')\times [0, 1]^{(h'-g')_L}\Big)^{[0,1]^{g'_L}} \\
ϑ ⟼ λ' ↦ \letin{ϑ(λ'ι_L)}{\Braket {\vec p | [x_h, λ^h]_g}_h}{\Braket {\vec p | [X(h ↪ h \pushout_g g')(x_h), λ^h]_{g'}}_h}
\end{cases}
\]
\end{definition}

$T$ can be endowed with the structure of a $[, ]$-enriched monad, that is, since $[, ]$ is a (cartesian) monoidal closed category, a strong monad. Its enriched unit $η_X：1 → TX^X$ and bind $(-)^∗：TY^X → TY^TX$ are as follows\footnote{following Fosco Loregiàn~\cite{loregian-coend}, $よ：\BiG → [\BiG, \Sets]\op$ denotes the (contravariant) Yoneda embedding.}.

\begingroup
\allowdisplaybreaks
\begin{longtable}{p{0.63\textwidth}p{0.37\textwidth}}
\{*\} ⟶ [X × よ(g), TX]\\
* ⟼  ŋg'：
\begin{cases}
X(g') × よ(g)(g') ⟶ TX(g') \\
x_{g'}, \; \text{\textunderscore} ⟼ \Big([0, 1]^{g'_L} ∋ λ ↦ 1 ⋅ \Ket{[x_{g'}, !]_{g'}}\Big)
\end{cases}
\end{cases}
\end{aligned}$ &\hspace{-2
TY^X(g) ⟶ \big[TX × よ(g), TY\big]
% \hphantom{\Big(\Prfin \int^{g' ↪ h} X(h)\times [0, 1]^{(h-g')_L}\Big)^{[0,1]^{g_L'}} \!\!\!\!\!\!\!× よ(g)(g') \xto {φ^\ast_{g'}} \Big(\Prfin \int^{g' ↪ h'} Y(h')\times [0, 1]^{(h'-g')_L}\Big)^{[0,1]^{g_L'}}}
% \span\\
\\
φ ⟼ φ^\ast
\end{cases}
\end{aligned}$\\
\text{where } \\[-.2em]
\multicolumn{2}{l}{
φ^\ast_{g'}： \begin{cases}
\displaystyle\Big(\Prfin \int^{g' ↪ h} \mkern-35mu X(h)\times [0, 1]^{(h-g')_L}\Big)^{[0,1]^{g_L'}} \mkern-15mu × よ(g)(g') \xto {φ^\ast_{g'}} \Big(\Prfin \int^{g' ↪ h'} \mkern-35mu Y(h')\times [0, 1]^{(h'-g')_L}\Big)^{[0,1]^{g_L'}}
\span\\
(ϑ, \; g \xinjto {ι} g') \xmapsto {φ^\ast_{g'}} λ' ↦& \letin {ϑ(λ')} {\Braket {\vec p | [x_h, λ^h]_{g'}}_{h ∈ H_{g'}}}{\\
&\for{h ∈ H_{g'}}\\
& \;\; \letin{φ_h(x_h, g \xinjto {ι} g' ↪ h)(λ^h ⨆ λ')}{\Braket {\vec {q_h} | [y_h', γ^{h'}]_{h}}_{h' ∈ H_{h}}}{\\
& \Braket {\vec p | Q | [y_{h'}, γ^{h'} ⨆ λ^h]_{g'}}_{h' ∈ \bigcup\limits_{h ∈ H_{g'}} \mkern-15mu H_h}}}\\
\end{cases}
\end{aligned}$}\\
% \multicolumn{2}{l}{
\text{and }
$Q \,≝\, \begin{pmatrix}
\vec {q_{h_1}} \\
\vdots \\
\vec {q_{h_n}}
\end{pmatrix}_{{\smash h_i ∈ H_{g'}}}
\hspace{-1em}=\hspace{1em}
\begin{pmatrix}
q_{h_1, h_1'}   & \rvline &   & \rvline &  q_{h_1, h_m'} \\
\vdots          & \rvline & ⋯ & \rvline & \vdots \\
q_{h_n, h_1'}   & \rvline &   & \rvline &  q_{h_n, h_m'}
\end{pmatrix}_{\substack{h_i ∈ H_{g'} \\ h_j' ∈ \bigcup\limits_{h ∈ H_{g'}} \mkern-15mu H_h}}$ & \hspace{-4.5em}\text{(where each $\vec {q_h}$ has been $0$-padded accordingly)}\\
\end{longtable}
\endgroup

% \begingroup
% \allowdisplaybreaks
% \begin{gather*}
%   η_X(g)：
%   \begin{cases}
%       \{*\} ⟶ [X × よ(g), TX]\\
%       * ⟼  ŋg'： \begin{cases}
%       X(g') × よ(g)(g') ⟶ TX(g') \\
%       x_{g'}, \; \text{\textunderscore} ⟼ \Big([0, 1]^{g'_L} ∋ λ ↦ 1 ⋅ \Ket{[x_{g'}, !]_{g'}}\Big)
%       \end{cases}
%   \end{cases}\\
%   (-)^\ast_g：
%   \begin{cases}
%   TY^X(g) ⟶ \big[TX × よ(g), \; TY\big]
%   \hphantom{\Big(\Prfin \int^{g' ↪ h} X(h)\times [0, 1]^{(h-g')_L}\Big)^{[0,1]^{g_L'}} \!\!\!\!\!\!\!× よ(g)(g') \xto {φ^\ast_{g'}} \Big(\Prfin \int^{g' ↪ h'} Y(h')\times [0, 1]^{(h'-g')_L}\Big)^{[0,1]^{g_L'}}}
%   \span\\
%   φ ⟼ φ^\ast
%   \end{cases}\\
% \text{where } \\[.8em]
% φ^\ast_{g'}：\begin{cases}
%     \displaystyle\Big(\Prfin \int^{g' ↪ h} \mkern-35mu X(h)\times [0, 1]^{(h-g')_L}\Big)^{[0,1]^{g_L'}} \mkern-15mu × よ(g)(g') \xto {φ^\ast_{g'}} \Big(\Prfin \int^{g' ↪ h'} \mkern-35mu Y(h')\times [0, 1]^{(h'-g')_L}\Big)^{[0,1]^{g_L'}}
%     \span\\
%     (ϑ, \; g \xinjto {ι} g') \xmapsto {φ^\ast_{g'}} λ' ↦& \letin {ϑ(λ')} {\Braket {\vec p | [x_h, λ^h]_{g'}}_{h ∈ H_{g'}}}{\\
%     &\for{h ∈ H_{g'}}\\
%     & \;\; \letin{φ_h(x_h, g \xinjto {ι} g' ↪ h)(λ^h ⨆ λ')}{\Braket {\vec {q_h} | [y_h', γ^{h'}]_{h}}_{h' ∈ H_{h}}}{\\
%     & \Braket {\vec p | Q | [y_{h'}, γ^{h'} ⨆ λ^h]_{g'}}_{h' ∈ \bigcup\limits_{h ∈ H_{g'}} \mkern-15mu H_h}}}\\
% \end{cases}\\
% \text{and } \\[.8em]
% Q \,≝\,
%     \begin{pmatrix}
%         \vec {q_{h_1}} \\
%         \vdots \\
%         \vec {q_{h_n}}
%     \end{pmatrix}_{h_i ∈ H_{g'}}
%     =
%     \begin{pmatrix}
%     q_{h_1, h_1'}   & \rvline &   & \rvline &  q_{h_1, h_m'} \\
%     \vdots          & \rvline & ⋯ & \rvline & \vdots \\
%     q_{h_n, h_1'}   & \rvline &   & \rvline &  q_{h_n, h_m'}
%     \end{pmatrix}_{\substack{h_i ∈ H_{g'} \\ h_j' ∈ \bigcup\limits_{h ∈ H_{g'}} \mkern-15mu H_h}}
% \end{gather*}
% \endgroup

As argued before, to construct an abstract model of probability, we show that the monad is commutative. Affineness straightforwardly stems from the following lemma:

\begin{lemma}\label{lemma:T-on-constant-presheaves}
Let $X$ be a constant presheaf on the coslice category $g/\BiG$, \ie there exists a set $S_0$ such that
$X(g \xinjto {ι} h) = S_0 \xto {\id} S_0$
for every $g \xinjto {ι} h \in g/\BiG$. Then $T(X)(g) ≅ \Prfin(S_0)^{[0, 1]^{g_L}}$.
\end{lemma}
% \begin{proof}
%   This results from a small calculation: $T(X)(g) ≅ \Big(\Prfin \int^{g ↪ h} S_0 × [0, 1]^{(h-g)_L}\Big)^{[0,1]^{g_L}}$. But as the functor $S_0 × -$ is left adjoint to $S_0 ⇒ -$ in $\Sets$, it is cocontinuous, so it preserves coends, and: $\int^{g ↪ h} S_0 × [0, 1]^{(h-g)_L} ≅ S_0 × \int^{g ↪ h} [0, 1]^{(h-g)_L} ≅ S_0 × \colim_{g ↪ h} [0, 1]^{(h-g)_L}$. Moreover, $\colim_{g ↪ h} [0, 1]^{(h-g)_L} ≅ \{\ast\}$. Indeed, $h = g$ is initial in $g/\BiG$, so it is terminal in the essential image of $[0, 1]^{((-)-g)_L}$ (by precomposition), and the resulting colimit is $[0, 1]^{(g-g)_L} ≅ [0, 1]^{∅} ≅ \{\ast\}$. Therefore, $\int^{g ↪ h} S_0 × [0, 1]^{(h-g)_L} ≅ S_0$ and the result follows.
% \end{proof}

We have the desired dataflow property, meaning that $T$ is an abstract model of probability~\cite{kock}:
\begin{theorem}
\label{thm:probabilistic-local-state-monad-commutative-affine}
The monad $T$ satisfies the dataflow property~(\ref{eqn:dataflow}): it is strong commutative and affine.
\end{theorem}

\begin{proof*}{Proof (Sketch)}
In the presheaf category, let $Z^Y × Y^X \xto {\circ} Z^X$ and $Z^Y × Y \xto {\rm ev} Z$ denote the internal composition and evaluation, and $f^\ast ≝ 1 \xto f TY^X \xto {(-)^\ast} TY^{TX}$ the internal Kleisli lifting of a global element $f$. To prove that $T$ is strong, we show, internally, the associativity ($(Ψ^\ast_g × Φ^\ast_g) \then \circ = ((Ψ^\ast × Φ) \then \circ)^\ast$) of the bind, the left unit law ($η^\ast = λ_{TX}. \id_{TX}$), and the right unit law ($(Φ^\ast × η) \then \circ = Φ$), for all $Φ：1 → TY^X, Ψ：1 → TZ^Y$. Finally, affineness stems from lemma~\ref{lemma:T-on-constant-presheaves}, and commutativity is the equation $a \bind \lambdaabs{x}{b \bind \lambdaabs{y}{η(x, y)}} \;=\; b \bind \lambdaabs{y}{a \bind \lambdaabs{x}{η(x, y)}}$ internally, for all $a：1 → TA, b：1 → TB$, which amounts to showing: $$\bigg(\Big(λ_A. \Big(\big((λ_B. η)^\ast × b\big) \,\then\, {\rm ev}\Big)\Big)^\ast × a\bigg) \then {\rm ev} = \bigg(\Big(λ_B. \Big(\big((λ_A. η)^\ast × a\big) \,\then\, {\rm ev}\Big)\Big)^\ast × b\bigg) \then {\rm ev}$$
\end{proof*}

\subsection{Categorical semantics}
\label{sec:cat-semantics}

In our language, the denotational interpretation of values, computations (return and let binding), and matching (elimination of $$'s and product types) is standard. We interpret computation judgements $Γ t A$ as morphisms
$Γ →T (A)$, by induction on the structure of typing derivations. The context $Γ$ is built of $$'s, $$, $$ and products. Therefore, $Γ$ is isomorphic to a presheaf of the form $2^k × (∘, -)^ℓ× (∙, -)^m$, where $k, ℓ, m$ are the numbers of booleans, functions and atoms in $Γ$, and $X^n$ is is the $n$-fold finite product in the category of presheaves. Computations of type $$ and $$ then have an intuitive interpretation:

\begin{proposition}\label{propos:denotation-atoms-functions}
A computation of type $\Atoms$ returns the label of an already existing atom or a fresh one with its connections to the already existing functions: $T(\den \Atoms)(g) \,≅\, \Prfin(g_R + 2^{g_L})^{[0, 1]^{g_L}}$. A computation of type $\Fns$ returns the label of an already existing function or create a new function with its connections to already existing atoms and a fixed probabilistic bias: $T(\den \Fns)(g) \,≅\, \Prfin(g_L + 2^{g_R} × [0, 1])^{[0, 1]^{g_L}}$.
\end{proposition}

For every bigraph $g$, we denote by $R_g$ (resp. $L_g$) the set of bigraphs $h ∈ g/$ having one more right (resp. left) node than $g$, and that are the same otherwise. For every $e ∈ 2^g_L$ (resp. $e ∈ 2^g_R$), we denote by $g +_e ∙∈ R_g$ (resp. $g +_e ∘∈ L_g$) the bigraph obtained by adding a new right (resp. left) node to $g$ with connectivity $e$ to the right (resp. left) nodes in $g$. We now give the denotational semantics of various constructs in our language. Henceforth, we will denote normalization constants (that can easily be inferred from the context) by $Z$.

\paragraph*{Denotations of $\cj{Γ}{\iflip} \tbool$, $\cj{Γ, v: \Fns, w: \Atoms}{v @ w} \tbool$, and $\cj{Γ, v: \Atoms, w: \Atoms}{v = w} \tbool$} First, by Lemma~\ref{lemma:T-on-constant-presheaves}, we note that $T()g  ≅   (2)^[0, 1]^g_L   ≅   [0, 1]^[0, 1]^g_L$. So naturally, the map $_g$ is the constant function returning the bias $θ$.

\paragraph*{Denotations of $\cj{Γ, v: \Fns, w: \Atoms}{v @ w} \tbool$, and $\cj{Γ, v: \Atoms, w: \Atoms}{v = w} \tbool$}

The map $v @ w_g:Γ, v: , w: (g) →[0, 1]^[0, 1]^g_L$ returns $1$ if the left node corresponding to $v$ is connected to the one of $w$ in $g$, $0$ otherwise. Using the internal edge relation $ℰ$, it is the internal composition: $$\den{v @ w} ≝ 1 × (\den{Γ} × \den{𝔽} × \den{𝔸}) \xto {η × (! × \mathcal E)} T(\den{\tbool})^{\den{\tbool}} × \den{\tbool} \xto {{\rm ev}} T(\den\tbool)$$

And similarly, the map $v = w_g:Γ, v: , w: (g) →[0, 1]^[0, 1]^g_L$ is given by: $$\den{v = w} ≝ \den{Γ} × \den{𝔸}^2 ≅  1 × \den{Γ} × \Big(よ(\bullet) + よ(\bullet + \bullet)\Big) \xto {η × ! × \big[! \,\then\, ι_{\itrue},\; ! \,\then\, ι_{\ifalse} \big]} T(\den{\tbool})^{\den{\tbool}} × \den{\tbool} \xto {{\rm ev}} T(\den\tbool)$$

where $[-,  -]$ is the copairing and $ι_, ι_： 1 → ≅ 2$ are the coprojections.

% \begin{equation*}\label{eq:denotation-at}
% \begin{split}
%   &\den{v @ w}_g：\begin{cases}
%     \den{Γ} × \BiG(\circ, g) × \BiG(\bullet, g) ⟶ [0, 1]^{[0, 1]^{g_L}} \\
%     \text{\textunderscore},\, \circ \xinjto {ƒ_v} g,\, \bullet \xinjto {a_w} g ↦ λ ↦ λ(ƒ_v(\circ))^{E^g(ƒ_v(\circ), a_w(\bullet))} \big(1-λ(ƒ_v(\circ))\big)^{1-E^g(ƒ_v(\circ), a_w(\bullet))}
%   \end{cases}
% \end{split}
% \end{equation*}

\paragraph*{Denotation of $\cj{Γ}{\ifresh} \Atoms$.}

The map $_g:Γ(g) →T ()(g)$ randomly chooses connections to each left node according to the state of biases, and makes a fresh right node with those connections.

\begin{equation*}\label{eq:denotation-fresh}
\begin{split}
2^k × \BiG(\circ, g)^\ell × \BiG(\bullet, g)^m ⟶ \Prfin(g_R + 2^{g_L})^{[0, 1]^{g_L}} \\
\text{\textunderscore},\, \text{\textunderscore},\, \text{\textunderscore} ↦ λ ↦ \displaystyle\Braket{\frac 1 Z \smash{\prod\limits_{ƒ ∈ g_L} λ(ƒ)^{E^h(ƒ, a_h(\bullet))} (1-λ(ƒ))^{1-E^h(ƒ, a_h(\bullet))}} | \big[ \smash{\underbrace{\bullet}_{\mathclap{\; ≅ \, (h-g)_R}}} \xinjto {a_h} h, \, !\big]_g}_{h ∈ R_g}
\end{cases}
\end{split}
\end{equation*}

It suffices to consider the bigraphs that belong to $R_g$ only, by garbage collection of the coend.

\paragraph*{Denotation of $\cj{Γ}{\lambdamem x u} \Fns$.}

As $$-abstractions are formed based on computation judgements of the form $Γ,x: u $. We can decompose the extra variable $x$ in the environment $Γ,   x:$, the denotation of which is of the form $Γ,   x:(g)   =   2^k × (∘, g)^ℓ× (∙, g)^m   ×   (∙,   g)$ for a bigraph $g ∈ $. Now, the extra part $x$ is a right node, and its valuation will either be a node already in the graph described in the rest of the environment, or a new one with particular edges to the rest of the environment. The argument $u$ can test (if it wants) what kind of node $x$ is, before returning a probability.

As a result, the denotation $u_g：2^k × (∘, g)^ℓ× (∙, g)^m × (∙, g) ⟶ [0, 1]^[0, 1]^g_L$ gives us the edge probability of the left node (atom) that we need to generate, both to the existing right nodes (functions), and to any future right node (which needs to be remembered). This can be formalized into a natural transformation $x u：Γ→T()$, provided that $u$ satisfies the following property:

\begin{definition}[Freshness-invariant functions]\label{def:freshness-invariant}
A function $\lambdamem{x}{u}$ is \emph{freshness-invariant} if, for every $g, b^k ∈ 2^k$, $κ_i：\circ ↪ g, \, τ_j ：\bullet ↪ g$ and $λ ∈ [0, 1]^{g_L}$, we have (where $ι_1, \, ι_2$ are the coprojections):
$$∀ e ∈ 2^{g_L}, \, \den{u}_g\big(b^k,\, (\circ \xinjto {κ_i} g \xinjto {ι_1} g +_e \bullet)_i,\, (\bullet \xinjto {τ_j} g \xinjto {ι_1} g +_e \bullet)_j, \, \bullet \xinjto {ι_2} g +_e \bullet, \, λ\big) \text{ is a constant } \tilde{p}_u$$
\end{definition}

A sufficient condition to ensure that a function of the form $xu$ be freshness-invariant is that it has no subexpression of the form $f @ y$, where $y ∉ (xu)$. An example thereof is $xbf @ x_0b(x=x_0)$. Non examples are $xyf @ y$ and $xf @ x$ (negation of $f$). %\footnote{The latter could be interpreted as a generalized element of $[\Atoms, 2]$ by taking the negation (in the internal language of the topos) of the denotation of $f$.}.
% Sam: this is a bit confusing, I'm not sure it's negation in the internal logic, which is not classical anyway
We can interpret freshness-invariant functions as follows:

\begin{equation*}
\mkern-20mu\den{\lambdamem x u}_g：\!\!\begin{cases}
2^k × \BiG(\circ, g)^\ell × \BiG(\bullet, g)^m ⟶ \Prfin(g_L + 2^{g_R} × [0, 1])^{[0, 1]^{g_L}}\\[1em]
b^k,\, \substack{\mbox{\normalsize $(\circ \xinjto {κ_i} g)_i,$}\\ \mbox{\normalsize $(\bullet \xinjto {τ_j} g)_j$}} ↦ λ ↦ \displaystyle\Braket{\frac 1 Z \smash{\prod\limits_{a ∈ g_R} p_a^{E^h(ƒ_h(\circ), a)} (1-p_a)^{1-E^h(ƒ_h(\circ), a)}} | \big[ \smash{\underbrace{\circ}_{\mathclap{\, ≅ \, (h-g)_L}}} \xinjto {ƒ_h} h, \, \text{\textunderscore} ↦ \tilde{p}_u\big]_g}_{h ∈ L_g}
\end{cases}\\
\label{eq:denotation-lambdamem}
\end{equation*}
where $p_a  ≝  u_g(b^k,  (∘κ_i g)_i,  (∙τ_j g)_j,   ∙a g,   λ)$ for every $a ∈ g_R$, and $p̃_u$ is as in Def.~\ref{def:freshness-invariant}. As a result, the probabilistic local state monad validates~\eqref{eqn:stochmem}:

\begin{theorem}\label{thm:T-mem}
The monad $T$ supports stochastic memoization (Def.~\ref{def:mem}) for freshness-invariant functions (Def.~\ref{def:freshness-invariant}), which include any function $\lambdamem{x}{u}$ that does not contain a subexpression of the form $f @ y$, where $y ∉ \fv(\lambdamem{x}{u})$ (so, in particular, constant Bernoulli functions).
\end{theorem}
\begin{proof*}{Proof (Sketch)} The denotation of $\lambdamem{}{}$-abstractions enables us to define a map $T(\den\tbool)^{\den{\Atoms}} → T(\Fns)$, which can in turn be postcomposed by $T(\Fns) \xto {φ} T\big(\den{\tbool}^{\den{\Atoms}}\big)$, where

φ_g ：\begin{cases}
T(\Fns)(g) ≅ \Prfin(g_R + 2^{g_L})^{[0, 1]^{g_L}} ⟶ [0, 1]^{[0, 1]^g × (g_R + 2^{g_L})} ≅ T\big(\den{\tbool}^{\den{\Atoms}}\big)(g)\\
ϑ ⟼ (λ, a) ∈ [0, 1]^g × (g_R + 2^{g_L})
↦ \letin{ϑ(λ)}{\sum_{a' ∈ g_R + 2^{g_L}} p_{a'} \Ket{a'}}{p_a}
\end{cases}

to obtain $\mlstinline{mem}：T(\den\tbool)^{\den{\Atoms}} → T(\den{\tbool}^{\den{\Atoms}})$, and then we show \cref{eqn:mem-monad} in the presheaf topos.
\end{proof*}

\begin{example}
The denotation of $\iletin{x}{\ifresh}{
\iletin{f}{\lambdamem{y}{\iflip}}{f @ x}}$
is the map $$1 × 1 \xto {\Big(λ_{\den \Atoms}. \Big(\big((λ_{\den \Fns}. f @ x)^\ast × (\lambdamem{y}{\iflip}) \big) \then {\rm ev}\Big) \Big)^\ast × \, \ifresh} T(\den\tbool)^{T\den\Atoms} × T(\den\Atoms) \xto {{\rm ev}} T(\den\tbool)$$
given by $\ast, \ast ↦ λ ↦ θ \Ket{\itrue} + (1-θ) \Ket{\ifalse}$, as desired.
\end{example}

\subsection{Soundness}
\label{sec:soundness}

Configurations are of the form $(γ, e, 𝖌, λ)$, where $e$ is of type $A$, and can be denotationally interpreted as

$$\den{(γ, e, 𝖌, λ)} ≝ \sum_{{\tilde e} ∈ 2^{U_{𝖌}}} \prod_{(ƒ, a) ∈ U_{𝖌}} λ(ƒ)^{{\tilde e}(ƒ, a)} \big(1-λ(ƒ)\big)^{1-{\tilde e}(ƒ, a)} \den[𝖌_{\tilde e}]{u}(γ, λ) ∈ T(A)_{𝖌_{\tilde e}}(γ)(λ)$$

where $U_𝖌 ≝ {(ƒ, a) |E(ƒ, a) = ⊥ } ⊆ 𝖌_L × 𝖌_R$ and $𝖌_ẽ$ extends $𝖌$ according to $ẽ$: $E(ƒ, a) = ẽ(ƒ, a)$ for all $(ƒ, a) ∈ U_𝖌$. We can then prove that the denotational semantics is sound with respect to the operational semantics:

\begin{theorem}[Soundness]\label{thm:soundness}
$$\den{(γ, e, 𝖌, λ)} ≅
\sum_{\substack{(γ, e, 𝖌, λ) ⟶ (γ', e', 𝖌', λ')\\ \text{with proba. } p}} p \cdot \den{(γ', e', 𝖌', λ')}$$
\end{theorem}
\begin{proof*}{Proof (Sketch)} As an intermediate step, we build a big-step semantics, and show that this is sound, \ie~making a small step of the operational semantics (\S\ref{sec:operational}) does not change the distributions in the final big-step semantics. Next, we show that the big step semantics of a configuration corresponds to the denotational semantics, for which the main thing to check is that the equivalence classes of the coend are respected.
\end{proof*}
%%%Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
%%% End:

\section{Haskell Implementation}
\label{sec:implementation}
We have a practical Haskell implementation comparing the small-step, big-step operational, and denotational semantics to showcase the soundness theorem with QuickCheck, in a setting analogous (albeit slightly different\footnote{Unlike our mathematical framework, where we can memoize all freshness-invariant functions (\ref{def:freshness-invariant}), our implementation only memoizes constant Bernoulli functions. Another key difference is that we could not implement coends in Haskell, so we used a global state monad transformer to manage the memoization bigraph, keeping track of edges between left nodes (function labels) and right nodes (atom labels) that have been sampled.}, to better suit the specificities of Haskell) to the theoretical one we presented. The artefact is openly available~\cite{stoch-mem-implementation-github}.

\section{Summary}

In conclusion, we have successfully tackled the open problem of finding a semantic interpretation of stochastic memoization for a class of functions with diffuse domain that includes the constant Bernoulli functions. Our contributions pave the way for further exploration and development of probabilistic programming and the sound application of stochastic memoization in Bayesian nonparametrics.

\section{Acknowledgements}
We are grateful to Nate Ackerman, Cameron Freer, Dan Roy and Hongseok
Yang for various conversations over many years, relating
to~\cite{statonExchangeableRandomProcesses2017}, name generation, stochastic memoization and subsequent developments.
The presheaf category here is related to the Rado
topos~\cite{caramello-fraisse} that we have been exploring in ongoing
work, with Jacek Karwowski and Sean Moss and the above four coauthors.
Thanks to Dario Stein for discussions about name generation and for
pointing out~\cite{kallianpur}.
Thanks too to Swaraj Dash, Mathieu Huot, Ohad Kammar, Oleg Kiselyov, Alex Lew, and all in the Oxford group for many discussions about this topic.
Finally, thank you to our reviewers for detailed feedback.

\bibliographystyle{./entics}
\bibliography{./bibliography}

\end{document}