A Categorical Approach to DIBI Models

Tao Gu1 Jialu Bao2 Justin Hsu2 Alexandra Silva2 Fabio Zanasi1,3

Gu, Bao, Hsu, Silva, and Zanasi

University College London, UK

Cornell University, NY, USA

University of Bologna, Italy

The logic of Dependence and Independence Bunched Implications (DIBI) is a logic to reason about conditional independence (CI); for instance, DIBI formulas can characterise CI in probability distributions and relational databases, using the probabilistic and relational DIBI models, respectively.

Despite the similarity of the probabilistic and relational models, a uniform, more abstract account remains unsolved. The laborious case-by-case verification of the frame conditions required for constructing new models also calls for such a treatment.
In this paper, we develop an abstract framework for systematically constructing DIBI models, using category theory as the unifying mathematical language. In particular, we use string diagrams – a graphical presentation of monoidal categories – to give a uniform definition of the parallel composition and subkernel relation in DIBI models.
Our approach not only generalises known models, but also yields new models of interest and reduces properties of DIBI models to structures in the underlying categories.
Furthermore, our categorical framework enables a logical notion of CI, in terms of the satisfaction of specific DIBI formulas. We compare it with string diagrammatic approaches to CI and show that it is an extension of string diagrammatic CI under reasonable conditions.

§ INTRODUCTION

Conditional independence (CI) is a fundamental concept across various research areas, including programming languages [28, 6, 21], statistics [10], and database theory [1], among others. Although specific definitions may vary, the core idea remains straightforward: events $A$ and $B$ are   `independent' when information about one event does not convey information about the other. Furthermore, events $A$ and $B$ are `conditionally independent' given event $C$ if, with knowledge of event $C$, events $A$ and $B$ become independent. Albeit intuitive, reasoning about conditional independence is an intricate task, leading to extensive research efforts aimed at formalising such reasoning [25, 14].

For probabilistic programs, an extension of standard programs with constructs to sample from distributions, formal methods for (conditional) independence have emerged as powerful tools for program verification.
For instance, Barthe et. al. [6] introduced Probabilistic Separation Logic (PSL) and applied it to formalise several cryptography protocols, where independence of  variables guarantees no leakage of information and thus security of the algorithms.
A follow-up work from Bao et al. [5]
proposed the logic of Dependence and Independence Bunched Implications (DIBI),
which enhances PSL with the ability to reason about conditional independence. Syntactically, DIBI extends the logic of Bunched Implications (BI) [23, 27], which is the assertion logic underpinning Separation Logic (SL) [28] and PSL, with a non-commutative conjunction $\biThen$ and its adjoints.
Semantically, as in BI, the separating conjunction $\mand$ is interpreted through a partial operation $\stPlus$ on states, regarded as the parallel composition. In addition, they define a sequential composition $\stThen$ to interpret $P \biThen Q$.
Informally, $P \mand Q$ says that $P$ and $Q$ hold in states that can be separated, and $P \biThen Q$ expresses a possible dependency of $Q$ on $P$.  <Ref> will review the logic in more details.

Bao et. al [5] introduced two kinds of semantic models for DIBI logic – probabilistic and relational.
The probabilistic DIBI models

are used to reason about CI of variables in discrete probabilistic computation.

The relational DIBI models

are designed to express join dependency – a notion of conditional independence in database theory and relational algebra – between variables in relational databases.
These two models share many similarities, and the conditions to verify they are models are repetitive. This led Bao et. al. [5] to conjecture a categorical approach to construct abstract DIBI models that induce these concrete models as instances. This would greatly facilitate the construction of new models.

To solve this conjecture, we start with the observation that, in both the probabilistic and relational DIBI models, the states
resemble Markov kernels: they are maps from
input elements to distributions/powersets over output elements. Specifically, the input/output elements are value assignments on a finite set of variables, as an abstraction of program memories or database entries.
Such DIBI states can be identified categorically as morphisms in the Kleisli categories associated to the discrete distribution monad (<ref>, for the probabilistic model) or the nonempty powerset monad (<ref>, for the relational model).
However, giving a categorical definition for the parallel compositions $\stPlus$ is difficult.
The previous work [5] gives <Ref> as a pictorial intuition for the parallel composition.
The states are drawn as trapezoids, with the short and long vertical sides representing the input and output domains, respectively.

There, given a blue map $f_1$ and a red map $f_2$, their parallel composition $f_1 \oplus f_2$ takes as input the union of their inputs. Then, each $f_i$ takes its counterpart in the combined input domain and generates an output. Finally these two outputs are combined to be the output of $f_1 \oplus f_2$.
This parallel composition is partial because the combination of their outputs is allowed only when the variables overlap in particular ways.
This creates a challenge to capture DIBI models categorically because, in a categorical setting, the domains and codomains of DIBI states are objects, and it is not obvious how to define the overlap of objects used in the parallel composition.

Parallel composition depicted in [5].

A diagrammatic representation.

Intuition for parallel composition.

Our solution stems from a formalisation of this graphical intuition through string diagrams, a pictorial formalism for monoidal categories. String diagrams are widely adopted as intuitive yet mathematically rigorous reasoning tools across different areas of science, see [26] for an overview.
We formalise the trapezoids intuition in <Ref> into string diagrams as in <Ref>.

The maps previously embodied as trapezoids now have a fork shape, with some branches being straight lines and some other branches going through boxes.
The boxes represent arbitrary morphisms in the underlying category, and the straight lines represent the identity morphisms.
Whereas composition of two DIBI states were hand-waved as two trapezoids tiled together in <Ref>, with string diagram we can define it precisely:
the overlap of the two trapezoids is witnessed by the grey wires, and
the composition joins two diagrams side-by-side with the grey wires shared.
We will show in <Ref> that this string diagram representation yields DIBI models in any category with enough structure to interpret $\tikzfig{copier}$, namely, Markov categories [9, 13].
Furthermore, in <Ref>, we will derive several concrete DIBI models as instances.

Additionally, our framework enables a comparison between different characterisations  of conditional independence (CI).
The previous work [5] expresses probabilistic or relational CI in terms of satisfaction of some DIBI formulas.
Since we can construct categorical DIBI models based on any Markov categories, we define a logical notion of CI for morphisms in Markov categories as  satisfaction of those DIBI formulas.
In <Ref>, we investigate the relationship between our `logical' CI and various CI notions based on categorical structures from literature in synthetic statistics [9, 13].

Throughout the paper we fix a countably infinite set of variables $\setVar$, use $x, y, z, \dots$ for elements of $\setVar$, and use $W, X, Y, \dots$ for finite subsets of $\setVar$.

§ CATEGORY THEORY PRELIMINARIES

Unless specified, we assume that all monoidal categories we consider are strict and write $\domain{f}$ and $\codom{f}$ for the domain and codomain of any morphism $f$.
We write $\lr{\catC, \tensor, \tenUnit}$ for a (strict) monoidal category, where $\tensor$ is the monoidal product and $\tenUnit$ the unit object of $\catC$. If is also symmetric, we write $\tenSwap_{\obA, \obB} \colon \obA \tensor \obB \to \obB \tensor \obA$ for the symmetry natural transformation indexed by objects $\obA$ and $\obB$.

As detailed for instance in [29, 26, 12], morphisms of symmetric monoidal categories have a graphical presentation as string diagrams, where sequential composition and monoidal product are depicted as concatenation and juxtaposition of diagrams, respectively: given morphisms $f \colon \obX \to \obY$, $g \colon \obY \to \obZ$, $h \colon \obU \to \obV$,

\[
g \after f = \tikzfig{seq-comp} \qquad g \tensor h = \tikzfig{para-comp}
\]

Our convention is to read string diagrams from left to right, and tensor products from top to bottom. We will sometimes omit object labels in the diagrams when they are evident or irrelevant to the context. Symmetries are indicated with the string diagram $\tikzfig{swap}$. We call string diagrams consisting solely of combinations of $\tikzfig{swap}$s rewirings: intuitively, they permute the order of the objects.

We will need the notion of a Markov category, which suitably generalises categories of probabilistic processes [13].

First, a copy-delete category (CD category) is a symmetric monoidal category (SMC) $\lr{\catC, \tensor, \tenUnit}$ with `copy' $\copyMor_{\obC}$ and `delete' $\discardMor_{\obC}$ morphisms for each object $\obC$, drawn diagrammatically as $\copier$ and $\discarder$ respectively, that form a commutative comonoid:

\[
\tikzfig{copier-ass} \qquad \tikzfig{copier-discarder} \qquad \tikzfig{copier-sym}
\]

Because of the leftmost equation above, we sometimes write a `trident' $\tikzfig{three-copies}$ for either side of it. Moreover, both $\copyMor$ and $\discardMor$ are compatible with the monoidal structure:

\[
\tikzfig{nat-copy-1} = \tikzfig{nat-copy-2} \qquad \qquad  \tikzfig{nat-discard-1} = \tikzfig{nat-discard-2}
\]

We say $\discardMor$ is natural if $\tikzfig{tenUnit-terminal}$ for every morphism $f$. A Markov category is a CD category in which $\discardMor$ is natural. A CD category $\catC$ has conditionals if for each morphism $f \colon \obA \to \obX \tensor \obY$, there exist (not necessarily unique) morphisms $f_{\obX} \colon \obA \to \obX$ (called the marginal) and $f_{|\obX} \colon \obX \to \obY$ (called the conditional) such that $\scalebox{.9}{\tikzfig{def-conditional-5}} = \scalebox{.9}{\tikzfig{def-conditional-6}}$. When $\catC$ is a Markov category, such marginal $f_\obX$ is unique given $\obX$ because of the naturality of

\[
\tikzfig{def-conditional-7} = \tikzfig{def-conditional-8} = \tikzfig{def-conditional-9}
\]

§ DIBI LOGIC AND ITS PROBABILISTIC MODEL

In this section we review the logic of Dependence and Independence Bunched Implications (DIBI). For space reasons, we focus on the discrete probabilistic model for DIBI, as introduced in [5]. The interested reader may refer to [5] for the relational model, whose construction follows similar steps.

DIBI formulas are defined inductively as follows:

\begin{equation*}
P, Q  ::= p \in \setAtomProp
\mid \top
\mid I
\mid P \land Q
\mid P \to Q
\mid P \mand Q
\mid P \mimp Q
\mid P \biThen Q
\mid P \biTo Q
\mid P \biOt Q
\end{equation*}

The additive conjunction $\land$ is just the standard Boolean conjunction. The multiplicative conjunction $\mand$ states that $P$ and $Q$ are independent. Both are already present in BI.  DIBI extends BI with the non-commutative conjunction $\biThen$[Not to be confused with the additive context constructor which is also denoted as $\biThen$ in the standard BI literature such as [23, 27].], where $P
\biThen Q$ states that $Q$ may depend on $P$. The operation $\mimp$ is adjoint to $\mand$, and $\biTo$, $\biOt$ are adjoints to $\biThen$. DIBI formulas are interpreted on
DIBI models, each consisting of a DIBI frame
on a set of states $A$ and a
valuation function $\valV \colon \setAtomProp \to \powset (A)$
that maps an atomic proposition to the set of states on which it is true.
While a BI frame is based on a partial commutative monoid [11], a DIBI frame consists of two monoids (one commutative and one not) on the same underlying set, taking care of the two non-additive conjunctions $\mand$ and $\biThen$, respectively.

A DIBI frame is a tuple $\frameA = \langle A, \stSmaller, \stPlus,
\stThen, \unitSet \rangle$, where $A$ is a set of states, $\stSmaller$ is a preorder on $A$, $\unitSet
\subseteq A$ are units, and $\stPlus, \stThen \colon A \times A \to \powset(A)$ are partial binary operations[Note that, even though $\stThen, \stPlus$ are also partial in the models considered in [5], they have type $A \times A \to \powset (A)$ in that work. This is because the authors obtain completeness of DIBI logic using a method developed by Docherty [11], which only works for the more general type. Because the operations are actually partial rather than non-deterministic, and we are not interested in completeness here, we stick to the more accurate type.], satisfying the frame conditions in <Ref>.

\begin{align*}
& a \stPlus b \eqIfDefined b \stPlus a
\tag{$\stPlus$-\textsc{Com}}\label{frameAx:plus-com} \\
& \exists e \in E \colon a = e \stPlus a
\tag{$\stPlus$-\textsc{UnitExist}} \label{frameAx:plus-unit-exist} \\
& (a \stPlus b) \stPlus c \eqIfDefined a \stPlus (b \stPlus c)
\tag{$\stPlus$-\textsc{Assoc}}\label{frameAx:plus-ass}
\end{align*}

\begin{align*}
& \exists e \in E \colon a = e \stThen a
\tag{$\stThen$-\textsc{UnitExist\textsubscript{L}}} \quad \label{frameAx:then-unit-left} \\
& \exists e \in E \colon a = a \stThen e
\tag{$\stThen$-\textsc{UnitExist\textsubscript{R}}} \label{frameAx:then-unit-right} \\
& (a \stThen b) \stThen c \eqIfDefined a \stThen (b \stThen c)
\tag{$\stThen$-\textsc{Assoc}}\label{frameAx:then-ass}
\end{align*}

\begin{align*}
& e \in E \,\&\, (a \stPlus e) \isDefined \,\,\onlyif (a \stPlus e) \stGeq a
\tag{$\stPlus$-\textsc{UnitCoh}} \label{frameAx:plus-unit-coherent} \\
& e \in E \,\&\, (a \stThen e) \isDefined \,\,\onlyif (a \stThen e) \stGeq a \quad
\tag{$\stThen$-\textsc{UnitCoh\textsubscript{R}}}\label{frameAx:then-coherence-right} \\
& e \in E \,\&\, e'\stGeq e \onlyif e' \in E \tag{\textsc{UnitClosure}} \label{frameAx:unit-closure} \\
& (a \stPlus b) \isDefined \,\&~\, a \stGeq a' \,\&\, b \stGeq b' \onlyif (a' \stPlus b') \isDefined \,\&\, (a \stPlus b) \stGeq (a' \stPlus b')
\tag{$\stPlus$-\textsc{DownClosed}}\label{frameAx:plus-down-closed} \\
& (a \stThen b) \isDefined \,\&\, (a \stThen b) \stLeq c' \onlyif \exists a', b' \colon a' \stGeq a \,\&\, b' \stGeq b \,\&\, c' = (a' \stThen b')
\tag{$\stThen$-\textsc{UpClosed}}\label{frameAx:then-up-closed} \\
& (a_1 \stThen a_2) \stPlus (b_1 \stThen b_2) \eqIfDefined (a_1 \stPlus b_1) \stThen (a_2 \stPlus b_2)
% & x \in y \stPlus z ~\&~ y \in y_1 \stThen y_2 ~\&~ z \in z_1 \stThen z_2
% \onlyif \exists u, v \colon u \in y_1 \stPlus z_1 \land v \in y_2 \stPlus z_2 \land x \in u \stThen v
\tag{\textsc{RevExchange}} \label{frameAx:rev-exchange}
\end{align*}

DIBI frame conditions (with implicit outermost universal quantifiers), where $\isDefined$ stands for `is defined', $\eqIfDefined$ means `equal when either side is defined'.

The operations $\stThen$ and $\stPlus$ are referred to as the sequential and parallel compositions of states. Intuitively, $a \stSmaller b$ says that $a$ can be extended to $b$,  and $E$ is the set of states that act as units for these operations.

For capturing conditional independence, atomic propositions $\setAtomProp$ have the form $\kp{S}{T}$, for finite sets of variables $S, T$. Roughly, $\kp{S}{T}$ means the values of variables in $T$ only depend on that of $S$. We now recall the semantics of DIBI formulas, restricting to the fragment that is necessary for the current work.

Given a DIBI model $\langle \frameA, \valV \rangle$, satisfaction $\satisfy{\valV}$ of -formulas at $\frameA$-states is inductively defined as follows:

$a \satisfy{\valV} I$   iff  $a \in E$
$a \satisfy{\valV} \top$  always

$a \satisfy{\valV} (\kp{A}{B})$     iff     $a \in \valV(\kp{A}{B})$

$a \satisfy{\valV} P \land Q$     iff     $a \satisfy{\valV} P ~\text{and}~ a \satisfy{\valV} Q$

$a \satisfy{\valV} P \mand Q$     iff     $\exists b_1, b_2$ such that $b_1 \stPlus b_2 \stLeq a$, $b_1 \satisfy{\valV} P$, $b_2 \satisfy{\valV} Q$

$a \satisfy{\valV} P \biThen Q$     iff
$\exists b_1,
b_2$ such that $b_1 \stThen b_2 = a$, $b_1 \satisfy{\valV} P$, $b_2 \satisfy{\valV} Q$

For a concrete example of DIBI models, we review the probabilistic models.

Let $\setVal$ be a set of values, to which variables in $\setVar$ are assigned.
A memory over a finite set of variables $X$ is a function $\memoryM \colon X \to \setVal$, and the memory space over $X$ is the set of all memories over $X$,
denoted as $\memSpace{X}{\setVal}$, or $\memSpaceS{X}$ when $\setVal$ is clear.
Given a memory $\memoryM \in \memSpaceS{X}$ and a subset $U \subseteq X$, the memory $\memProj{\memoryM}{U} \colon U \to \setVal$ is the restriction of $\memoryM$ to the domain $U$.
Given a set $S$, $\dist S$ is the set of discrete distributions over $S$; that is, for any $\mu \in \dist S$, we have $\mu \colon S \to [0,1]$, the support $\support{\mu} = \{ s \in S \mid \mu(s) > 0 \}$ is finite, and $\sum_{s \in S} \mu(s) = 1$.
A dirac distribution $\mu$ on an outcome $s$ is the distribution $\mu$ such that
$\mu(s) = 1$, and $\mu(s') = 0$ for any $s' \neq s$.
Given a distribution $\mu$ in $\dist \memSpaceS{X}$, if $Y \subseteq X$,
we define the marginalisation of $\mu$ to $\dist \memSpaceS{Y}$, written as
$\proj_{Y} \mu$, by letting $(\proj_{Y} \mu) (\memoryM_Y) = \sum_{\memoryM \in \memSpaceS{X} \mid \memProj{\memoryM}{Y} = \memoryM_Y } \mu(\memoryM)$.

To capture conditional independence, we now introduce the notion of probabilistic input-preserving kernels.

A probabilistic input-preserving kernel (or probabilistic kernel for short) is a function $f \colon \memSpaceS{X}{} \to \dist \memSpaceS{Y}{}$ satisfying:

* $X \subseteq Y$,

* $\proj_{X} \circ f = \monadUnit{\dist}{\memSpaceS{X}}$,
where $\monadUnit{\dist}{\memSpaceS{X}} (\memoryM)$ returns the dirac
distribution over $\memoryM$.

The set of all probabilistic kernels is denoted $\conProbKern$.

In words, a probabilistic kernel $f$ maps a memory $\memoryM$ on $X$ to a distribution of memories on $Y \supseteq X$ whose support contains only memories $\memoryM'$ that faithfully extends $\memoryM$ (thus the name `input-preserving'). Alternatively, $f$ can be seen as a conditional distribution $\Pr(Y \!\mid\! X)$ where $Y \supseteq X$, such that $\Pr(Y = B \!\mid\! X = A)$ is nonzero only if $B$ restricted to the domain $X$ equals $A$.

The probabilistic frame $\probFrameBasedOn{\setVal}$ based on $\Values{}$ is a tuple $\lr{\conProbKern, \stLeq, \stPlus, \stThen,
\conProbKern}$
where $\stThen, \stPlus, \stLeq$ are defined for
$f \colon \memSpaceS{X} \to \dist \memSpaceS{Y}$ and
$g \colon \memSpaceS{Z} \to \dist \memSpaceS{W} $ as:

* the sequential composition $f \stThen g$ is defined iff $Y = Z$. In this case, $f \stThen g$ is of the form $\memSpaceS{X} \to \dist \memSpaceS{W}$, and given $\memoryM \in \memSpaceS{X}$, $(f \stThen g)(\memoryM)$ maps $\memoryN \in \memSpaceS{W}$ to $\sum_{\memoryL \in \support{f(\memoryM})} g(\memoryL)(\memoryN)$;

* the parallel composition $f \stPlus g$ is defined iff $X \cap Z =
Y \cap W$. In this case, $f \stPlus g$ is of the form $\memSpaceS{X \cup Z} \to \dist \memSpaceS{Y \cup W}$ such that given $\memoryL \in \memSpaceS{X \cup Z}$ and $\memoryM \in \memSpaceS{Y \cup W}$,
we have
$(f \stPlus g)(\memoryL)(\memoryM) = f(\memProj{\memoryL}{X} )(\memProj{\memoryM}{Y}) \cdot g(\memProj{\memoryL}{Z})(\memProj{\memoryM}{W})$;

* the subkernel relation $f \stLeq g$ holds if there exist a finite set of variables $S$ and $h \in \conProbKern$ such that $g = \left( f \stPlus \monadUnit{\dist}{\memSpaceS{S}} \right) \stThen h$.

The probabilistic model based on $\setVal$ consists of the probabilistic frame $\probFrameBasedOn{\setVal}$ and the following natural valuation $\natVal \colon \setAtomProp \to \powset(\conProbKern)$: given $(\kp{S}{T})$ and $f \colon \memSpaceS{X} \to \dist \memSpaceS{Y}$, $f \in \natVal(\kp{S}{T})$ iff there exists a probabilistic kernel $f' \colon \memSpaceS{X'} \to \dist \memSpaceS{Y'}$ such that $f' \sqsubseteq f$, $X' = S$ and $T \subseteq Y'$.

We may simply write $\probFrame$ when the underlying set of values $\setVal$ is evident.

Next we give examples of probabilistic kernels and how they compose.
We will abbreviate a map from a variable $x$ to a value $c$ as $c_x$ and use the ket notation $\ket{\omega}$ for each probabilistic outcome $\omega$.

Consider variables $x, y, z$ that take values in $\Val = \Bool$.
We define a map $f \colon \memSpaceS{ \{ z \} } \to \dist \memSpaceS{ \{ x, y, z \} }$ by:

\begin{align*}
f( \oran{0_z}) & =
\frac{1}{4} \ket{0_x, 0_y, \oran{0_z}}
+ \frac{1}{4} \ket{0_x, 1_y, \oran{0_z}}
+ \frac{1}{4} \ket{1_y, 0_y, \oran{0_z}}
+ \frac{1}{4} \ket{1_y, 1_y, \oran{0_z}}\\
f( \purp{1_z}) & =
\frac{1}{16} \ket{0_x, 0_y, \purp{1_z}}
+ \frac{3}{16} \ket{0_x, 1_y, \purp{1_z}}
+ \frac{3}{16} \ket{1_y, 0_y, \purp{1_z}}
+ \frac{9}{16} \ket{1_y, 1_y, \purp{1_z}}
\end{align*}

The input memory (coloured) is preserved by $f$ so it is a probabilistic kernel.

Then define $g_1 \colon \memSpaceS{ \{z\} } \to \dist\memSpaceS{ \{x, z\} }$ and $g_2 \colon \memSpaceS{ \{z\} } \to \dist\memSpaceS{ \{y, z\} }$  as:

\begin{align*}
g_1 (\oran{0_z}) & = \frac{1}{2} \ket{0_x, \oran{0_z}} + \frac{1}{2} \ket{1_y, \oran{0_z}}
& g_1 (\purp{1_z}) & = \frac{1}{4} \ket{0_x, \purp{1_z}} + \frac{3}{4} \ket{1_y, \purp{1_z}} \\
g_2 (\oran{0_z}) & = \frac{1}{2} \ket{0_y, \oran{0_z}} + \frac{1}{2} \ket{1_y, \oran{0_z}}
& g_2 (\purp{1_z}) & = \frac{1}{4} \ket{0_y, \purp{1_z}} + \frac{3}{4} \ket{1_y, \purp{1_z}}
\end{align*}

Both $g_1$ and $g_2$ are probabilistic kernels as well.
The parallel composition $g_1 \stPlus g_2$ is defined since $\{ z \} \cap \{ z \} = \{x,z\} \cap \{y, z\}$; in fact, it is easy to verify that $g_1 \stPlus g_2 = f$.

Moreover, $g_1$ and $g_2$ can be obtained by projecting the output of $f$ on $\{ x, z \}$ and $\{ y, z \}$, respectively, and we can show $g_1 \stLeq f$ and $g_2 \stLeq f$.

§ DIBI MODELS IN MARKOV CATEGORIES

In this section we construct more abstract DIBI models based on categorical structures.

The starting point of our approach is a categorical characterisation of the concrete probabilistic models given above.
In the following, we begin by showing examples of how elements in that model can be reformulated in categorical terms and then formally present our categorical construction of DIBI models.

As we noted in <Ref>, the probabilistic DIBI kernels can be identified as morphisms in the Kleisli category for the distribution monad $\Kl(\dist)$ (<Ref>); however, not all morphisms in $\Kl(\dist)$ are probabilistic DIBI kernels, so we need to define the extra conditions categorically.
Let $\catMemProb$ be the subcategory of $\Kl(\dist)$ where objects are restricted to memory spaces over $\setVal$. That is, the objects are memory spaces $\memoryM  \colon X \to \setVal$, and the morphisms are maps $f: \memSpaceS{X} \to \dist{\memSpaceS{Y}}$.

Then, probabilistic kernels are exactly those morphisms in the  $\catMemProb$ that satisfy the input-preserving condition in <Ref>.
To visualise the probabilistic kernels, we depict them using string diagrams, which is possible because $\catMemProb$ is a subcategory of $\Kl(\dist)$ and $\Kl(\dist)$ has the monoidal structure(<Ref>).
We also observe that the codomain of an input-preserving kernel $f \colon \memSpaceS{X} \klto \memSpaceS{Y}$ can be decomposed as $\memSpaceS{X} \times \memSpaceS{Y \setminus X}$,

Recall the probabilistic kernel $f$ from <Ref>. Since its codomain $\memSpaceS{\{x, y, z\}}$ can be decomposed as $\memSpaceS{\{x\}} \times \memSpaceS{\{y\}} \times \memSpaceS{\{z\}}$, we can draw it as follows:

\[\tikzfig{kernel-eg-3}\]

Intuitively, $\tikzfig{copy-Mz}$ produces two copies of the value of $z$, and the values of $x$ and $y$ are computed from that of $z$ via $\tikzfig{f-prime}$, while the value of $z$ gets preserved through a straight wire in the bottom.
As in this example, such copy structure of $\Kl(\dist)$ enables us to capture the `input-preserving' condition of probabilistic kernels generally.

Next we want to express the sequential ($\stThen$) and parallel ($\stPlus$) compositions of probabilistic kernels categorically.
The former is exactly the sequential composition of morphisms in $\Kl(\dist)$.
The parallel composition, however, is not the monoidal product $\tensor$ in $\Kl(\dist)$, which is the Cartesian product on objects. By definition, the monoidal product is total, while the parallel composition is partial. Even when the parallel composition is defined, the types of the resulting morphisms do not match. Suppose that the parallel composition of $f \colon \memSpaceS{X} \klto \memSpaceS{Y}$ and $g \colon \memSpaceS{U} \klto \memSpaceS{V}$ is defined, we have

\[
f \stPlus g \colon \memSpaceS{ X \cup U } \klto \memSpaceS{ Y \cup V }
\quad
f \tensor g \colon \memSpaceS{X} \times \memSpaceS{U} \klto \memSpaceS{Y} \times \memSpaceS{V}
\]

The key difference is that parallel composition considers a single memory that can be projected into two pieces, while the monoidal product considers the cartesian product of two pieces of memory, no matter if they agree or not on overlapped variables.

To combine $\memSpaceS{X}$ and $\memSpaceS{U}$ into $\memSpaceS{X \cup U}$ categorically, we note that for disjoint $Z_1, Z_2$, $\memSpaceS{Z_1 \cup Z_2} \cong \memSpaceS{Z_1} \times \memSpaceS{Z_2}$, therefore
$\memSpaceS{X \cup U} \cong \memSpaceS{X\setminus U} \times \memSpaceS{X \cap U} \times \memSpaceS{U \setminus X}$.

Thus we can illustrate the parallel composition of two probabilistic kernels as in the following example.

The probabilistic kernels $g_1$ and $g_2$ from <Ref> – seen as $\Kl(\dist)$-morphisms – are drawn as the first and second string diagram below respectively.

\begin{equation*}
\tikzfig{diagram-g1} \qquad \tikzfig{diagram-g2} \qquad  \scalebox{.9}{\tikzfig{g1-g2-para-comp}}
\end{equation*}

where $g_1' \colon \memSpaceS{\{z\}} \klto \memSpaceS{\{x\}}$ and $g_2' \colon \memSpaceS{\{z\}} \klto \memSpaceS{\{y\}}$ represent the conditional distributions obtained by suitable projections of $g_1$ and $g_2$, respectively. The parallel composition $g_1 \stPlus g_2$ is given by the rightmost string diagram above.

We omit the formal string diagrammatic definitions here as they can be easily derived from their counterparts in the generic construction of DIBI models, defined later in <Ref>.

Towards that categorical construction of DIBI models,
we also want to generalise the concept of memory spaces
$\memSpaceS{X}$, which were customised for reasoning about probabilistic programs and relational databases.
We observe that the side conditions of the parallel and sequential compositions are all based on comparing the set of variables in the (co)domains, so they only depend on the $X$ part in $\memSpaceS{X}$.
This motivates us to define DIBI states as morphisms in a category whose objects are made of variables in <Ref>.

To express finite sets of variables and the union of disjoint such sets in a monoidal category,
in the following we will represent finite sets of variables as lists. We impose a linear order $\varLeq$ on $\setVar$ such that indexed variables  inherit the order of their indices, e.g., $x_1 \varLeq x_2 \varLeq x_3$.
Let $x \varLessThan y$ abbreviate for $x \varLeq y$ and $x \neq y$.

Then, finite sets of variables can be represented as finite lists of variables ordered by $\varLessThan$, via a translation that we write as $\setToList{\cdot}$. For instance, $\setToList{\{ x_3, x_1, x_3, x_4 \}} = [x_1, x_3, x_4]$.

Throughout the rest of the section we fix a Markov category $\lrangle{\catC, \tensor, \tenUnit}$, and assignment $\obChoice \colon \Var \to \ob{\catC}$ of a $\catC$-object to each $x \in \Var$.

Let $\catWithVarName{\catC}{\obChoice}$ be the symmetric monoidal category whose objects are finite lists of variables, and morphisms $[x_1, \dots, x_m] \to [y_1, \dots, y_n]$ are $\catC$-morphisms $\obChoice(x_1) \tensor \cdots \tensor \obChoice(x_m) \to \obChoice(y_1) \tensor \cdots \tensor \obChoice(y_n)$.
Sequential composition is defined as in $\catC$. The identity on $[x_1, \dots, x_m]$ is $\idMor_{\obChoice x_1 \tensor \cdots \tensor \obChoice x_m}$.
The monoidal product in $\catWithVarName{\catC}{\obChoice}$ – which we also write as $\tensor$ with abuse of notation – is list concatenation on objects, and monoidal product in $\catC$ on morphisms.

Since $\catC$ is a Markov category, it follows immediately that $\catWithVarName{\catC}{\obChoice}$ is also a Markov category.
Sometimes we restrict ourselves to a uniform assignment $\obChoice$; that is, for some fixed $\obC \in \ob{\catC}$, $\obChoice(x) = \obC$ for all $x \in \setVar$. This is in line with the scenario where a fixed value space $\setVal$ is used for all variables (see <Ref>).

In this case, we write $\catWithVarName{\catC}{\obChoice}$ as $\catWithVarName{\catC}{\obC}$ to emphasise the uniform value of the assignment. This category can be seen as the full subcategory of $\catC$ freely generated by $\obC$, but with each occurrence of the generating object named by a variable. The next example shows how the construction in <Ref> selects morphisms of $\Kl(\dist)$ that act on memory spaces, among which we have all the probabilistic kernels.

Let $\catC$ be $\Kl(\dist)$, and $\obChoice \colon \setVar \to \ob{\Kl(\dist)}$ be the constant function $x \mapsto \setVal$ for all $x \in \setVar$. Then there is a full and faithful embedding functor $\iota \colon \catMemProb \to \catWithVarName{\Kl(\dist)}{\obChoice}$: on objects, given a set $X$, $\iota(\memSpaceS{X}) = \setToList{X}$; on morphisms, given $f \colon \memSpaceS{X} \to \dist \memSpaceS{Y}$ with $X = \{ x_1, \dots, x_m \}$ and $Y = \{ y_1, \dots, y_n \}$, its image $\iota(f) \colon X \to Y$ is the composed map $\setVal^{m} \xrightarrow{\cong} \memSpaceS{X} \xrightarrow{f} \dist \memSpaceS{Y} \xrightarrow{\dist \cong} \dist \setVal^n$, where the isomorphisms are, e.g., $\memSpaceS{Y} \xrightarrow{\cong} \memSpaceS{y_1} \times \cdots \times \memSpaceS{y_n} \xrightarrow{\cong^{\obChoice} } \setVal^n$, using the valuation $\obChoice(y_j) = \setVal$.

Now that we have abstracted the concept of memory spaces used in concrete DIBI models as objects in Markov categories, the states of DIBI models — the role that in the probabilistic models is filled by probabilistic kernels — takes the form of morphisms in these categories. Next we  identify  those $\catC$-morphisms that constitute the states of DIBI models. We call them the input-preserving kernels in $\catC$, written $\setSemKernel{\catWithVarName{\catC}{\obChoice}}$.

A $\catWithVarName{\catC}{\obChoice}$-morphism $f \colon [x_1, \dots, x_m] \to [y_1, \dots, y_n]$ is a $\catWithVarName{\catC}{\obChoice}$ input-preserving kernel (or $\catWithVarName{\catC}{\obChoice}$-kernel for short) if $x_1 \varLessThan \cdots \varLessThan x_m$, $y_1 \varLessThan \cdots \varLessThan y_n$, and $f$ can be decomposed as follows, where $\sigma$ is rewiring:

\begin{equation}
\label{eq:C-kernel}
\tikzfig{diagram-f} = \scalebox{0.9}{\tikzfig{C-kernel-1}}
\end{equation}

In words, a $\catWithVarName{\catC}{\obChoice}$-kernel is a morphism whose interfaces are essentially finite sets of variables, such that the input is preserved as part of the output (through the upper leg of those $\copier$s). The map $f'$ in (<ref>) is referred to as the nontrivial part of the input-preserving kernel.
It follows from <Ref> that, for a $\catWithVarName{\catC}{\obChoice}$-kernel, its codomain $[ y_1, \dots, y_n]$ always subsumes its domain $[ x_1, \dots, x_m ]$; also, $u_1, \dots, u_k $ are precisely those $y_j$s that are not among these $x_i$s. Since the (co)domains of $\catWithVarName{\catC}{\obChoice}$-kernel are list presentation of sets, we also write the types of $\catWithVarName{\catC}{\obChoice}$-kernels using the corresponding sets, e.g., in (<ref>), $f \colon \{ x_1, \dots, x_m \} \to \{ y_1, \dots, y_n \}$.

Next we define compositions on input-preserving kernels, generalising what we have seen in Example <ref> for the probabilistic models.

Given arbitrary $\catWithVarName{\catC}{\obChoice}$-kernels $f \colon X \to Y$ and $g \colon U \to V$ as in <Ref>, their sequential composition $f \stThen g$ is defined iff $\codom{f} = \domain{g}$, in which case $f \stThen g = g \after f$. Their parallel composition $f \stPlus g$ is defined iff $X \cap U = Y \cap V$. Assume $\listL = \setToList{ X \cap U }$, $\listL_1 = \setToList{ X \setminus (X \cap U) }$, $\listL_2 = \setToList{ U \setminus (X \cap U) }$, $\listK_1 = \setToList{Y \setminus (Y \cap V)}$, and $\listK_2 = \setToList{V \setminus (Y \cap V)}$, then $f \stPlus g \colon X \cup U \to Y \cup V$ is defined as in <Ref>, where all the $\sigma_i$s are rewiring morphisms for making the input and output variables $\varLessThan$-ordered.

\[
% c =
\scalebox{.88}{\tikzfig{def-kernel-para-comp-3}} ~
% d =
\scalebox{.88}{\tikzfig{def-kernel-para-comp-4}}
\]

$\catWithVarName{\catC}{\obChoice}$-kernels $f$ and $g$.

\[
% c \stPlus d =
\scalebox{.88}{\tikzfig{def-kernel-para-comp-5}}
\]

$f \stPlus g$

Parallel composition of $\catWithVarName{\catC}{\obChoice}$.

Note here a benefit of the diagrammatic representation: we can easily identify the memory overlap $\memSpaceS{X \cap Y}$, as it is depicted a separate wire; with traditional syntax, we would need to apply associativity and commutativity to extract it from $\memSpaceS{X \cup Y}$.
It is easy to see that kernels are closed under compositions. Also, for curious readers, we note that $\catWithVarName{\catC}{\obChoice}$-kernels with their parallel compositions form a partially monoidal category [3]. Next we define the subkernel relation.

Given two $\catWithVarName{\catC}{\obChoice}$-kernels $f$ and $g$, we say $f$ is a
subkernel of $g$ – denoted as $f \stLeq g$ – if there exist $z_1, \cdots, z_n \in \setVar$, a $\catWithVarName{\catC}{\obChoice}$-kernel $h$, and rewiring morphisms $\sigma_1, \sigma_2$ such that $g$ can expressed as on the right-hand side.

\begin{equation*}\label{eq:def-kernel-leq}
g = \tikzfig{def-subkernel}
\end{equation*}

The subkernel relation is transitive and reflexive, which can be shown simply by manipulations of the string diagram.
We are finally able to state the main result of this section: $\catWithVarName{\catC}{\obChoice}$-kernels and their compositions form a DIBI frame.

$\frameSemKernel{\catWithVarName{\catC}{\obChoice}} = \lrangle{ \setSemKernel{\catWithVarName{\catC}{\obChoice}}, \stLeq, \stPlus, \stThen, \setSemKernel{\catWithVarName{\catC}{\obChoice}} }$ is a DIBI frame.

Also, under the natural valuation $\natVal$, a $\catWithVarName{\catC}{\obChoice}$-kernel $f \colon X \to Y$ satisfies $\kp{S}{T}$ iff there is a subkernel $(f' \colon X' \to Y') \stLeq f$ such that $X' = S$ and $Y' \supseteq T$. Thus:
$(\frameSemKernel{\catWithVarName{\catC}{\obChoice}}, \natVal)$ is a DIBI model.

We will see in <Ref> how to use this categorical construction to derive a wide range of DIBI models. Moreover, it also helps to extract properties of the underlying category that are essential to a specific feature of a DIBI model. Here is an example.

If $\catC$ further satisfies that for arbitrary morphisms $f, g$ and object $\obD$, $f \tensor \discardMor_{\obD} = g \tensor \discardMor_{\obD}$ implies $f = g$, then subkernel is unique given its type in the following sense: if $\catWithVarName{\catC}{\obChoice}$-kernels $f_1, f_2 \colon U \to V$ are both subkernels of $g$, then $f_1 = f_2$.

Note that the uniqueness of subkernels has been observed already in the context of probabilistic and relational models, see <cit.>. <Ref> reveals the general conditions under which we have this uniqueness for a wider class of DIBI models. In particular, we will see in <Ref> how the probabilistic models meets the conditions of <Ref>.

§ EXAMPLES

In this section we provide concrete instances of the categorical construction in <Ref>. The first example concerns the probabilistic DIBI models.
The remaining examples are new DIBI models. Some of them have been suggested in the DIBI paper [5], yet not materialised due to the complexity involved in stating each component and verifying the frame conditions. Within our framework, these steps become much easier to perform.

§.§ Probabilistic (and Relational) DIBI Models

As we sketched in <Ref> and <Ref>,
the probabilistic DIBI kernels and
$\lrangle{\frameSemKernel{\Kl(\dist)}, \natVal}$ input-preserving kernels
correspond to each other.
We now formally show that the probabilistic DIBI model in  <Ref> can be recovered from the categorical DIBI model $\lrangle{\frameSemKernel{\Kl(\dist)}, \natVal}$. Since both models are equipped with the natural valuation $\natVal$, we focus on the frame part.

To make the correspondence precise, we introduce the category of DIBI frames, as hinted in <cit.>.

In the category of DIBI frames $\catDibiFrame$, objects are DIBI frames; morphisms $f \colon \lr{S, \stLeq_{S}, \stPlus_{S}, \stThen_{S}, \unitSet_{S}} \to \lr{T, \stLeq_{T}, \stPlus_{T}, \stThen_{T}, \unitSet_{T}}$ are functions $f \colon S \to T$ that respect all the relations and partial operations: for arbitrary $s, s' \in S$,

* $s \stLeq_{S} s'$ implies $f(s) \stLeq_{T} f(s')$;

* if $s \operateVar_{S} s'$ is defined, then $f(s) \operateVar_{S} f(s')$ is defined, and $f(s) \operateVar_{T} f(s') = f(s \operateVar_{S} s')$, for $\operateVar \in \{ \stPlus, \stThen \}$;

* $s \in \unitSet_{S}$ implies $f(s) \in \unitSet_{T}$.

It turns out that the function $\iota$ introduced in <Ref> extends to an isomorphism of DIBI frames from $\probFrameBasedOn{\setVal}$ to $\frameSemKernel{\catWithVarName{\Kl(\dist)}{\setVal}}$.

$\probFrameBasedOn{\setVal} \cong \frameSemKernel{\catWithVarName{\Kl(\dist)}{\setVal}}$.

The probabilistic kernel $g_1 \colon \memSpaceS{\{z\}} \to \dist \memSpaceS{ \{ x, z\} }$ from <Ref> corresponds to the following $\catWithVarName{\Kl(\dist)}{\{0, 1\}}$-kernel $h_1 \colon [z] \to [x, z]$ – i.e., a $\Kl(\dist)$-morphism $\{0, 1\} \klto \{0, 1\}^2$ – where: $\oran{0} \mapsto \frac{1}{2} \ket{0, \oran{0}} + \frac{1}{2} \ket{1, \oran{0}}$, $\purp{1} \mapsto \frac{1}{4} \ket{0, \purp{1}} + \frac{3}{4} \ket{1, \purp{1}}$.

Diagrammatically, $h_1$ is of the form $\tikzfig{eg-prob-kern-1}$,
where $h'_1 \colon [z] \to [x]$ is the map such that $\oran{0} \mapsto \frac{1}{2} \ket{0} + \frac{1}{2} \ket{1}$ and $\purp{1} \mapsto \frac{1}{4} \ket{0} + \frac{3}{4} \ket{1}$

Similarly, the relational DIBI model from [5] with the value space $\setVal$ can be shown to be isomorphic to $\frameSemKernel{\catWithVarName{\Kl(\ipowset)}{\setVal}}$, where $\ipowset$ is the nonempty powerset monad.

§.§ Stochastic DIBI Models

Using our categorical construction, we can derive a notion of DIBI model for continuous probabilistic (stochastic) processes, not previously considered. This is of interest because, as we will later show in <ref>, it allows to capture conditional independence for continuous probability using DIBI formulas.

We take as underlying category $\catStoch$ of stochastic processes, defined as the Kleisli category $\Kl(\monadGiry)$ for the Giry monad on measurable spaces – see <Ref> for a full definition. Since $\monadGiry$ is an affine symmetric monoidal monad, $\catStoch$ is a Markov category [13].

Applying <Ref> to $\catC = \catStoch$,  we get DIBI frames based on stochastic processes.

Given an arbitrary map $\obChoice: \Var \to \ob{\catMeas}$,
$\frameSemKernel{\catWithVarName{\catStoch)}{\obChoice}} = \lrangle{ \setSemKernel{\catWithVarName{\catStoch}{\obChoice}}, \stLeq, \stPlus, \stThen, \setSemKernel{\catWithVarName{\catStoch}{\obChoice}} }$
is a DIBI frame.

We call $\frameSemKernel{\catWithVarName{\catStoch}{\obChoice}}$ the stochastic DIBI frame based on $\theta$ and elements in $\setSemKernel{\catWithVarName{\catStoch}{\obChoice}}$ stochastic kernels.

We show a representation of the Box-Muller transformation using stochastic kernels.
Consider $\obChoice$ that maps all variable names to the
Borel $\sigma$-algebra over reals $(\real, \borel(\real))$.
Define stochastic kernels $g_1 \colon \empset \to \{u\}$ and $g_2 \colon \empset \to \{w\}$ – both standing for $\catStoch$-morphisms $(\setOne, \{ \empset, \setOne \}) \to (\real, \borel(\real))$, or equivalently, a probabilistic measure on $(\real, \borel(\real))$ – by $g_i(\bullet) = \uniform(0, 1)$ for $i= 1, 2$, where $\uniform(0, 1)$ is the uniform measure over the interval $(0, 1)$. Such a uniform measure over infinite outcomes is
not possible in the discrete probabilistic DIBI model.
Define another stochastic kernel $f: \{u, w\} \to \{u, w, x, y\}$ where the value of $x, y$
are determined by the value of $u, w$:

\[
f(u \mapsto v_u, w \mapsto v_w)
= \dirac{v_u, v_w, \left( \sqrt{-2 \ln u} \cdot \cos (2 \pi w)\right)_x,  \left( \sqrt{-2 \ln u} \cdot \sin (2 \pi w)\right)_y}.
\]

Then $h = (g_1 \stPlus g_2) \stThen f$ gives a stochastic kernel $\empset \to \{u, w, x, y\}$.
Box-Muller transformation says that $x$ and
$y$ are independent in $h(\trivList)$, despite their seemingly dependence on $u$ and $w$. We will explain more on this in <Ref>.

Comparison with  [21].
Our stochastic DIBI models can be used to reason about independence and conditional probabilities in continuous distributions. A recent work  by Li et al. [21] proposed a BI model for the same goal, yet with some crucial differences in the set-up.

First, the states in Lilac's BI model are probabilistic space fragments of a fixed sample space, and their variables are mathematical random variables that deterministically map elements in the sample space to values.

In comparison, we treat variables as names that can be associated to values or distributions.

Our stochastic kernels – though not using an ambient sample space – can encode their set-up: we can devise a special variable $\Omega$ for `the sample space,' and deterministic kernels from $\Omega$ to other variables encode random variables.

Second, to reason about conditional probabilities,  want probability spaces to be disintegrable with respect to well-behaved random variables.
To achieve that, they require probability spaces in their model to be extensible to Borel spaces, since disintegration works nicer in Borel spaces.
By working with kernels, which already represents conditional probability spaces, we do not need to impose disintegratability on our DIBI states to reason about conditional probabilities.
For instance, while disintegration is not always possible in the category $\catStoch$, we
can still construct a DIBI model based on $\catStoch$.

Other measure-theoretic probabilistic DIBI models.
The category $\catStoch$ is not the only Markov category for
measure-theoretic probability. Another choice is $\catBorelStoch$, a subcategory of $\catStoch$ obtained by
restricting to standard Borel spaces as objects. It has some nice properties that $\catStoch$ does not satisfy, such as having conditionals as mentioned above.

$\catBorelStoch$ is also a Markov category and we can easily instantiate a DIBI model.

Given any map $\obChoice \colon \setVar \to \ob{\catBorelStoch}$,
$\frameSemKernel{\catWithVarName{\catBorelStoch}{\obChoice}}$ defined as
$\lrangle{ \setSemKernel{\catWithVarName{\catBorelStoch}{\obChoice}}, \stLeq, \stPlus, \stThen, \setSemKernel{\catWithVarName{\catBorelStoch}{\obChoice}} }$
is a DIBI frame.

The study of measure theory is also intertwined with topology,

and another category for measure-theoretic probability is
the Kleisli category of the Radon monad $\monadRadon$
based on the category of compact Hausdorff spaces $\catHaus$ and continuous maps (cf. <Ref>), which we will denote as $\Kl_{\catHaus}(\monadRadon)$. $\Kl_{\catHaus}(\monadRadon)$ is also a Markov category [13], so <Ref> applies.

Given any map $\obChoice: \Var \to \ob{\Kl_{\catHaus}(\monadRadon)}$,
$\frameSemKernel{\catWithVarName{\Kl_{\catHaus}(\monadRadon)}{\obChoice}}$ defined as $ \lrangle{ \setSemKernel{\catWithVarName{\Kl_{\catHaus}(\monadRadon)}{\obChoice}}, \stLeq, \stPlus, \stThen, \setSemKernel{\catWithVarName{\Kl_{\catHaus}(\monadRadon)}{\obChoice}} }$
is a DIBI frame.

A measure-theoretic Markov category not formed as Kleisli categories is the Gaussian probability category
$\catGauss$ [13].  Its objects are natural numbers, and a morphism $n \to m$ is a tuple $(M, \cov, \mu)$ representing the function $f: \real^{n} \to \real^{m}$ with $f(v) = M \cdot v + \xi$, where $\xi$ is the Gaussian noise with mean $\mu$ and covariance matrix $\cov$. Its monoidal product is addition $+$ on the objects and vector concatenation on morphisms.
$\catGauss$ differs from $\catStoch, \catBorelStoch$ and $\Kl_{\catHaus}(\monadRadon)$ in that it does not arise as the Kleisli category associated to some monad. But since it is a Markov category, we can again instantiate DIBI models based on $\catGauss$.

Given any map $\obChoice: \Var \to \ob{\catGauss}$,
$\frameSemKernel{\catWithVarName{ \catGauss}{\obChoice}}$ defined as $\lrangle{ \setSemKernel{\catWithVarName{ \catGauss}{\obChoice}}, \stLeq, \stPlus, \stThen, \setSemKernel{\catWithVarName{\catGauss}{\obChoice}} }$
is a DIBI frame.

§.§ Syntactic DIBI Models

The DIBI models defined so far all have kernels defined by some processes over memory spaces. It is worth considering a different flavour: purely formal, syntactically generated DIBI models.
We start by defining the underlying category.

$\catSynVar$ is the Markov category freely generated as follows:

* the generating objects are variables in $\setVar$;

* there is exactly one generating morphism of type $[u_1, \dots, u_m] \to [v_1, \dots, v_n]$ for distinct variables $u_1 \varLessThan \cdots \varLessThan u_m$ and $v_1 \varLessThan \cdots \varLessThan v_n$, written as string diagrams of the form $\tikzfig{gen-mor}$.

In words, $\catSynVar$-objects are finite lists of variables (without the requirements of duplicate-free or $\varLeq$-ordered); morphisms are diagrams freely concatenated using $\tikzfig{id-diagram}$, $\copier$, $\discarder$, $\swap$, and $\tikzfig{gen-mor}$, taken equivalence class modulo the Markov category equations.
The syntactic DIBI frame is based on the category $\catWithVarName{\catSynVar}{\id}$, where $\id \colon \setVar \to \ob{\catSynVar}$ is the identity function.

$\frameSynKernel = \lrangle{ \setSemKernel{\catWithVarName{\catSynVar}{\id}}, \stLeq, \stPlus, \stThen, \setSemKernel{\catWithVarName{\catSynVar}{\id}} }$ is a DIBI frame.

Equipped with the natural valuation $\natVal$, one obtains a DIBI model $\lrangle{\frameSynKernel, \natVal}$.
We postpone an example of $\catWithVarName{\catSynVar}{\id}$-kernels till <Ref>, <Ref>, in which $\catWithVarName{\catSynVar}{\id}$-kernels are used to distinguish two notions of conditional independence in Markov categories.

An interesting question for future work is how to extend the syntactic DIBI model to a term model. Typically being initial objects in categories of models, term models play an important role in proving completeness and defining categorical semantics for formal systems, including algebraic theories [20], logics [30]

(e.g., Lindenbaum–Tarski algebras)
and type theories [18, 17].
A term model for DIBI could lead to a sound and complete axiomatisation of the specific version of DIBI logic in this paper, whose atomic propositions take the form of $\kp{S}{T}$.

§ CONDITIONAL INDEPENDENCE

DIBI logic is designed for reasoning about CI. The prior work [5] shows that, conditional independence in the discrete probabilistic models and join dependency in the relational  models can be characterised by the same class of DIBI formulas.

Generalising this result, in this section we define a notion of CI on $\catWithVarName{\catC}{\obChoice}$-kernels based on formula satisfaction.
Since $\catWithVarName{\catC}{\obChoice}$ is a Markov category, we can compare our logical notion of CI with existing categorical definitions of CI in Markov categories [9, 13].

Fix a Markov category $\catC$ and a map $\obChoice \colon \setVar \to \ob{\catC}$. We define CI in the DIBI model $\lrangle{\frameSemKernel{\catWithVarName{\catC}{\obChoice}}, \natVal}$.

For any mutually disjoint finite sets of variables $W, X, Y, U$, $X$ and $Y$ are DIBI conditionally independent given $W$ in a $\catWithVarName{\catC}{\obChoice}$-kernel[Note that $\catWithVarName{\catC}{\obChoice}$-kernels with domain $\empset$ are not to be thought of as maps with empty domains. For instance, $\catWithVarName{\Kl(\dist)}{\obChoice}$-kernels of the form $\empset \to \{x, y\}$ corresponds to $\Kl(\dist)$-morphisms $\setOne \klto \obChoice(x) \times \obChoice(y)$, which denote distributions over $x, y$.]$f \colon \empset \to W \cup X \cup Y \cup U$ if

\begin{equation}\label{eq:CI}
f \satisfy{\natVal} (\kp{\empset}{W}) \biThen ( (\kp{W}{X}) \mand (\kp{W}{Y}) ).
\end{equation}

In this case, we write $\dibiCI{X}{Y}{W}$.

Let us unfold what (<ref>) means. Under the natural valuation $\natVal$, an atomic proposition of shape $\kp{S}{T}$ encodes the dependence of $T$ on $S$: formally, a $\catWithVarName{\catC}{\obChoice}$-kernel $f \colon X \to Y$ satisfies $\kp{S}{T}$ iff $f$ contains some subkernel $f' \colon S \to Y'$ such that $T \subseteq Y'$.
So the formula (<ref>) requires that $f$ is a kernel with empty domain that can be decomposed as $f \sqsupseteq f_0 \stThen (f_1 \stPlus f_2)$,
where $f_0$ determines the value on $W$,
$f_1$ determines the value on $X$ given the value on $W$, $f_2$ determines the value on $Y$ given the value on $W$, and $f_1$ and $f_2$ do so independently of each other.

We illustrate the formula with examples in the discrete probabilistic DIBI model and the stochastic DIBI model.

In the setting of <Ref>, consider the probabilistic kernel $h \colon \memSpaceS{\empset} \to \dist \memSpaceS{\{x, y, z\}}$ representing the following distribution:

\begin{align*}
\mu = & \frac{1}{8} \ket{0_x, 0_y, \oran{0_z}}
+ \frac{1}{8} \ket{0_x, 1_y, \oran{0_z}}
+ \frac{1}{8} \ket{1_y, 0_y, \oran{0_z}}
+ \frac{1}{8} \ket{1_y, 1_y, \oran{0_z}} \\
& + \frac{1}{32} \ket{0_x, 0_y, \purp{1_z}}
+ \frac{3}{32} \ket{0_x, 1_y, \purp{1_z}}
+ \frac{3}{32} \ket{1_y, 0_y, \purp{1_z}}
+ \frac{9}{32} \ket{1_y, 1_y, \purp{1_z}}
\end{align*}

Then $h \satisfy{\natVal} (\kp{\empset}{\{z\}}) \biThen ( (\kp{\{z\}}{\{z, x\}}) \mand (\kp{\{z\}}{\{z, y\}}) )$, because $h = h_0 \stThen f = h_0 \stThen (f_1 \stPlus f_2 )$, where $h_0$ denotes the uniform distribution $\frac{1}{2} \ket{0_z} + \frac{1}{2} \ket{1_z}$.

Define $g_1, g_2, f, h$ as in <Ref>. We want to assert that variables $x$ and $y$ are independent in the distribution
constructed by Box-Muller Transform.
Independence is a special case of conditional independence in which the set of conditioned variables is empty.
Thus, the goal is to assert $(\kp{\empset}{\empset}) \biThen ( (\kp{\empset}{\{x\}}) \mand (\kp{\empset}{\{y\}}) )$ – equivalently, $(\kp{\empset}{\{x\}}) \mand (\kp{\empset}{\{y\}})$.

Define $h_1: \empset \to \{x\}$ and $h_2: \empset \to \{y\}$

both as the standard normal distribution $\normal(0,1)$.
Clearly $h_1 \satisfy{\natVal} \kp{\empset}{\{x\}}$ and $h_2 \satisfy{\natVal} \kp{\empset}{\{y\}}$.

Moreover, some non-trivial calculations would show that
$ (h_1 \stPlus h_2)\stLeq h$, and consequently we have $h \satisfy{\natVal} (\kp{\empset}{\{x\}}) \mand (\kp{\empset}{\{y\}})$ by definition.

Since the categorical DIBI models are based on Markov categories, we compare our logical notion of CI on kernels with the canonical notion of CI in Markov categories, which defines CI as decomposability of morphisms. In <Ref>, a Markov category $\catX$ is fixed.

An $\catX$-morphism $s \colon
\tenUnit \to \obW \tensor \obX \tensor \obY$ displays the
conditional independence of $\obX$ and $\obY$ given $\obW$ if there exist $\catX$-morphisms $s_{\obW} \colon \tenUnit \to \obW$, $g_{\obX} \colon \obW \to \obX$, $g_{\obY} \colon \obW \to
\obY$ such that equation on the right holds. We write this as $\displayCI{\obX}{\obY}{\obW}$.

\[
\ \ \ \scalebox{0.95}{\tikzfig{display-CI-plain-1}} = \scalebox{0.95}{\tikzfig{display-CI-plain-2}}
\]

In the context of DIBI models, <Ref> restricts to stating the conditional independence of $X$ and $Y$ given $W$ in $\catWithVarName{\catC}{\obChoice}$-kernels of the form $\empset \to W \cup X \cup Y$. In particular, no extra variable in the kernel's codomain is allowed.

We show an example of this notion of CI in the Markov category $\catGauss$.
Consider morphism $s: \empset \to \{w, x, y\}$ specified by the tuple
\begin{align*}
\left(\initialMap,
\cov = \begin{bsmallmatrix}
1 &1 &1\\
1 &2 &1\\
1 &1 &2
\end{bsmallmatrix} ,
\mu = \begin{bsmallmatrix}
0 \\
0 \\
\end{bsmallmatrix}
\right),
\text{where $\initialMap$ denotes the trivial map from empty domain. }
\end{align*}

That is, $s$ takes a length 0 vector and generates a length 3 vector, holding the values of $w, x$ and $y$,
with the normal distribution $\normal(\mu, \cov)$.
This $s$ can be decomposed as in <Ref>
with $s_w = (\initialMap, 0, 1)$, $g_x = (1, 0, 1)$, and $g_y = (1, 0, 1)$:
composing $s_2$, $g_x$ and $g_y$ as in <Ref>,
we get $\EE(w) = \EE(\xi_w) = 0$,
$\EE(x) = \EE(w + \xi_x) = 0 + 0 = 0$ , and similarly,
$\EE(y) = \EE(w + \xi_y) = 0$, justifying the noise's mean $\mu$ being a zero vector.
For the covariance matrix, let $v = (w, x, y) - (\EE(w), \EE(x), \EE(y)) $.
$\cov = \EE(v \cdot v^T) = \EE((w, x, y) \cdot (w, x, y)^T) $, and one may show that $\cov$ is equal to the matrix above.

For any $\catWithVarName{\catC}{\obChoice}$-kernel $s \colon
\empset \to W \cup X \cup Y$ where $W, X, Y$ are mutually disjoint, $\displayCI{X}{Y}{W}$ iff $\dibiCI{X}{Y}{W}$.

In order to extend <Ref> to the scenario in <Ref> where a kernel $f$ might contain some $U$ in its codomain that does not appear in the CI statement, we need to modify the notion of CI from <Ref> – referred to as plain CI – to allow objects that do not appear in the CI statement to occur in the codomain of $s$. We suggest two sensible extensions.

Given an $\catX$-morphism $s \colon \tenUnit \to \obW \tensor \obX \tensor \obY \tensor \obU$,

$s$ displays Markov CI if there exist $\catX$-morphisms $s_{\obW}, g_{\obX}, g_{\obY}$ such that <ref> holds. We write this as $\markovCI{\obX}{\obY}{\obW}$.

$s$ displays superset CI if there exist $\catX$-morphisms $s_{0}, g_1, g_2$ such that <ref> holds. We write this as $\procCI{\obX}{\obY}{\obW}$.

display-CI-markov-1 = display-CI-markov-2
Markov CI.

display-CI-process-1 = display-CI-process-2
superset CI.

Two possible extension of plain CI.

These two notions differ regarding to the treatment of the extra object $\obU$.
In <Ref>, we project out the extra object $\obU$ and reduce the situation to that of <Ref>.
In <Ref>, $\obU$ is kept and passed along through $s_0, g_1, g_2$.

Clearly, both reduce to <Ref> when no such $\obU$ appears.

We can now state that DIBI CI coincides with Markov CI, but is weaker than superset CI.

Given the $\catWithVarName{\catC}{\obChoice}$-kernel $f \colon \empset \to W \cup X \cup Y \cup U$ from <Ref>,

* $f$ satisfies $\markovCI{X}{Y}{W}$ if and only if it satisfies $\dibiCI{X}{Y}{W}$;

* if $f$ satisfies $\procCI{X}{Y}{Z}$, then it also satisfies $\dibiCI{X}{Y}{Z}$.

The proof of <Ref> is in <Ref>.
<Ref> follows from <Ref> and that $\procCI{\obX}{\obY}{\obW}$ implies $\markovCI{\obX}{\obY}{\obW}$: one can simply apply $\discarder_{\obU}$ on both sides of <ref> and obtain <Ref> via naturality if $\discarder$.
The converse of <Ref>

does not hold in general, as demonstrated by the following example.

Consider the syntactic DIBI model $\lr{\frameSynKernel, \natVal}$ from <Ref>.

Define the $\catWithVarName{\catSynVar}{\id}$-kernel $f$ as on the right-hand side, where $c_0, c_1, c_2, d$ are all generating morphisms, i.e., not further decomposable.

Then $f$ satisfies the DIBI CI $\dibiCI{x}{y}{w}$, but not the superset CI $\procCI{x}{y}{w}$: one cannot rewrite the diagram in the dotted box into a juxtaposition of two diagrams with output wires containing $x$ and $y$, respectively; in other words, it cannot be rewritten as the style in <Ref>.

<Ref> gives some hint at how to weaken the superset CI to match DIBI CI: there one needs to allow some morphism $d$ following the morphism which witnesses $\procCI{x}{y}{z}$. We formalise this idea and show the resulting notion is indeed equivalent to both Markov and DIBI CI.

An $\catX$-morphism $s \colon
\tenUnit \to \obW \tensor \obX \tensor \obY \tensor \obU$ displays the extended superset conditional independence – denoted as $\extSupsetCI{\obX}{\obY}{\obW}$ – if there exist $\catX$-morphisms $s_0, g_1, g_2, h$ such that $s$ can be decomposed as on the right-hand side.

\begin{equation}
\label{eq:extend-superset-CI}
\tikzfig{extend-superset-CI-2}
\end{equation}

Compared with <Ref>, here one allows an extra morphism $h$ to appear after the original superset CI diagrams in <Ref>; in fact, modulo rewiring, (<ref>) is exactly $\scalebox{1}{\tikzfig{extend-superset-CI-3}}$, where $s_1 = \scalebox{.9}{\tikzfig{extend-superset-CI-4}}$.
One intuitive way to think of the extended superset CI is to view the morphisms as certain computational processes [24]: $\obX$ and $\obY$ are independent given $\obW$ in $s$ if $s$ could be obtained via a computation in which $\obX$ and $\obY$ are computed independently from $\obW$ (using $g_1$ and $g_2$ in (<ref>) respectively),
after which some further computation may apply (for which stands the $h$ part in (<ref>)).

In Markov categories with conditionals, extended superset CI and Markov CI are equivalent. Therefore, in the context of <Ref>, suppose further that $\catC$ has conditionals, then the three notions of CI – DIBI CI, Markov CI, and extended superset CI – coincide.

§ CONCLUSION

In this paper we provided a general recipe to construct models for DIBI logic, generalising the previously studied probabilistic and relational models. We adopted string diagrams to best visualise the `input-preserving' property that characterises the states in the models, as well as the compositions and subkernel relations, whose definition would be quite convoluted in non-diagrammatic syntax. Then we derived various new classes DIBI models of interest. Also, we abstractly define a notion of conditional independence in terms of DIBI formulas. As our approach is based on Markov categories, we were then able to compare it with other definitions of CI proposed in the literature.

There are many promising directions for future work. On the logic side, DIBI logic – interpreted in the probabilistic models – was designed to be the assertion logic of Conditional Probabilistic Separation Logic (CPSL). Our categorical construction of a wide class of DIBI models suggests a generalisation of CPSL to obtain program logics in various scenarios beyond probabilistic programs, in the spirit of Moggi [22].

The notion of CI we propose can be straightforwardly generalised from Markov categories to copy-delete categories (see <Ref>). This would allow us to encompass models such as relations with bag semantics in databases [8, 16], sub-probability measures [19]. However, to the best of the authors' knowledge, <Ref> fails for generic CD categories. Hence, finding appropriate notions of CI in this more general setting remains an open question.

From a categorical perspective, the definition of the category $\catWithVarName{\catC}{\obChoice}$ deserves further exploration, from at least two angles.
First, the $\catWithVarName{\catC}{\obChoice}$-morphisms may be seen as a “bundle” of the images of some syntactic categories of variables and renaming (similar to $\catSynVar$ from <Ref>) under suitable functors – usually referred to as `models' in functorial semantics. We would like to make the connection with functorial semantics rigorous in terms of the categorical structures involved. [20, 7].
Second, while the current work represents finite sets of variables using deduplicated finite $\varLeq$-ordered lists, towards a more principled treatment, it is worth exploring using nominal string diagrams, a diagrammatic calculus for variables and renaming [3, 4, 2],
to represent sets of variables.

[1]
Aho, A.V., Beeri, C., Ullman, J.D.: The theory of joins in relational
databases. ACM Transactions on Database Systems (TODS)  4(3),
297–314 (1979). 10.1145/320083.320091

[2]
Balco, S.: Display calculi and nominal string diagrams. Ph.D. thesis,
University of Leicester (2020)

[3]
Balco, S., Kurz, A.: Partially monoidal categories and the algebra of
simultaneous substitutions (2018), available at

[4]
Balco, S., Kurz, A.: Nominal String Diagrams. In: Roggenbach, M., Sokolova,
A. (eds.) 8th Conference on Algebra and Coalgebra in Computer Science (CALCO
2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 139,
pp. 18:1–18:20. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl,
Germany (2019). 10.4230/LIPIcs.CALCO.2019.18

[5]
Bao, J., Docherty, S., Hsu, J., Silva, A.: A bunched logic for conditional
independence. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS). pp. 1–14. IEEE (2021). 10.1109/LICS52264.2021.9470712

[6]
Barthe, G., Hsu, J., Liao, K.: A probabilistic separation logic. Proceedings of
the ACM on Programming Languages  4(POPL),  1–30 (2019).

[7]
Bonchi, F., Sobociński, P., Zanasi, F.: Deconstructing lawvere with
distributive laws. Journal of logical and algebraic methods in programming
95,  128–146 (2018). 10.1016/j.jlamp.2017.12.002

[8]
Chaudhuri, S., Vardi, M.Y.: Optimization of real conjunctive queries. In:
Proceedings of the twelfth ACM SIGACT-SIGMOD-SIGART symposium on Principles
of database systems. pp. 59–70 (1993). 10.1145/153850.153856

[9]
Cho, K., Jacobs, B.: Disintegration and Bayesian inversion via string
diagrams. Mathematical Structures in Computer Science  29(7),
938–971 (2019). 10.1017/S0960129518000488

[10]
Dawid, A.P.: Conditional independence in statistical theory. Journal of the
Royal Statistical Society: Series B (Methodological)  41(1),  1–15
(1979). 10.1111/j.2517-6161.1979.tb01052.x

[11]
Docherty, S.: Bunched logics: a uniform approach. Ph.D. thesis, UCL (University
College London) (2019)

[12]
Fong, B., Spivak, D.I.: An invitation to applied category theory: seven
sketches in compositionality. Cambridge University Press (2019).

[13]
Fritz, T.: A synthetic approach to markov kernels, conditional independence and
theorems on sufficient statistics. Advances in Mathematics  370,
107239 (Aug 2020). 10.1016/j.aim.2020.107239

[14]
Glymour, C., Zhang, K., Spirtes, P.: Review of causal discovery methods based
on graphical models. Frontiers in genetics  10,  524 (2019).

[15]
Golubtsov, P.V.: Monoidal kleisli category as a background for information
transformers theory. Inf. Process.  2(1),  62–84 (2002)

[16]
Green, T.J.: Bag Semantics, pp. 201–206. Springer US, Boston, MA (2009).

[17]
Hofmann, M.: On the interpretation of type theory in locally cartesian closed
categories. In: Pacholski, L., Tiuryn, J. (eds.) Computer Science Logic. pp.
427–441. Springer Berlin Heidelberg, Berlin, Heidelberg (1995).

[18]
Jacobs, B.: Semantics of weakening and contraction. Annals of pure and applied
logic  69(1),  73–106 (1994). 10.1016/0168-0072(94)90020-5

[19]
Klenke, A.: Probability theory: a comprehensive course. Springer Science &
Business Media (2013). 10.1007/978-1-84800-048-3

[20]
Lawvere, F.W.: Functorial semantics of algebraic theories. Proceedings of the
National Academy of Sciences  50(5),  869–872 (1963).

[21]
Li, J.M., Ahmed, A., Holtzen, S.: Lilac: a modal separation logic for
conditional probability. Proceedings of the ACM on Programming Languages
7(PLDI),  148–171 (2023). 10.1145/3591226

[22]
Moggi, E.: Notions of computation and monads. Information and computation
93(1),  55–92 (1991). 10.1016/0890-5401(91)90052-4

[23]
O'Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of
Symbolic Logic  5(2),  215–244 (1999). 10.2307/421090

[24]
Pavlovic, D.: Programs as diagrams: From categorical computability to
computable categories. Springer Nature (2023).

[25]
Pearl, J.: Causality. Cambridge university press (2009).

[26]
Piedeleu, R., Zanasi, F.: An introduction to string diagrams for computer
scientists. CoRR  abs/2305.08768 (2023)

[27]
Pym, D.J.: The semantics and proof theory of the logic of bunched implications,
vol. 26. Springer Science & Business Media (2013).

[28]
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures.
In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. pp.
55–74. IEEE (2002), <https://dl.acm.org/doi/10.5555/645683.664578>

[29]
Selinger, P.: A survey of graphical languages for monoidal categories. In: New
structures for physics, pp. 289–355. Springer (2010).

[30]
Tarski, A.: Logic, semantics, metamathematics: papers from 1923 to 1938.
Hackett Publishing (1983). 10.2307/2216869