Parametric Iteration in Resource Theories

Di Giorgio, Alessandro; Sobocinski, Pawel; Voorneveld, Niels

doi:10.4230/LIPIcs.CSL.2026.29

Parametric Iteration in Resource Theories

Alessandro Di Giorgio

Tallinn University of Technology, Estonia Pawel Sobocinski

Tallinn University of Technology, Estonia Niels Voorneveld

Cybernetica AS, Tartu, Estonia

Abstract

Many algorithms are specified with respect to a fixed but unknown parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key.

Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories – general calculi of processes with a string diagrammatic syntax – introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems – for instance, proving that guessing a randomly generated key has negligible success.

Keywords and phrases:

Markov categories, Cryptography, String diagrams, Asymptotic equivalence

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Program semantics ; Theory of computation

\rightarrow

Logic and verification ; Mathematics of computing

\rightarrow

Probability and statistics

Funding:

Di Giorgio, Voorneveld and Sobocinski were supported by the European Union under Grant Agreement No. 101087529. Sobocinski was additionally supported by the Estonian Research Council via grants PRG1215 and TEM-TA5 and the Estonian Center of Excellence in Artificial Intelligence (EXAI).

DOI:

10.4230/LIPIcs.CSL.2026.29

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Cryptographic protocols are designed to resist attacks by adversaries with bounded computational power. A fundamental feature is the use of a security parameter $\sigma$ , which governs the time complexity of potential attacks. As $\sigma$ increases, cryptographic schemes become more secure: for example, in public-key encryption, key lengths are chosen in relation to $\sigma$ to ensure that brute-force attacks require time exponential in $\sigma$ to succeed. More generally, security is often defined in asymptotic terms, stating that certain probabilities – such as the success rate of an adversary – become negligible as $\sigma$ grows. This notion of negligibility from cryptography [14] also appears in other computational settings, such as approximation schemes in probabilistic algorithms. In both cases, reasoning about security or approximation guarantees requires a formal understanding of how computations depend on the parameter $\sigma$ .

Traditionally, the definition of a cryptographic system follows a bottom-up approach: one chooses a model of computation, an algorithm and its notion of complexity, efficiency and security. This usually entails several technicalities that tend to hinder clarity and modularity. In particular, security proofs often become bogged down with low-level details of the computational model, making it difficult to generalise results, compare different cryptographic frameworks, or reason about their composition in a structured way.

This situation motivated the study of the subject at a higher level of abstraction, starting with the work of Canetti on Universal Composable Security [3] and followed by the work of Maurer and Renner on Abstract Cryptography [20, 19]. Motivated by similar intents, Broadbent and Karvonen [2] propose an abstract model of composable security definitions in terms of resource theories, formalised as symmetric monoidal categories.

The resource theoretic approach comes with the visual and intuitive language of string diagrams [13]. Consider the following example:

\begin{matrix}\includegraphics[scale={0.1}]{pics/S1/resth2}\end{matrix}

(1)

In the diagram above – read from left to right – we think of $f$ and $g$ as processes that transform the resources carried on the wires. The explicit splitting of wires via a copier, indicates that $f$ and $g$ share the second resource. If a resource is unused, as in the diagram on the right hand side, we simply discard it by closing the wire.

In cryptographic terms, we interpret the first input wire in (1) as carrying a message and the second as carrying a key. The processes $f$ and $g$ correspond to encryption and decryption, respectively. The equation postulates the correctness of the protocol: the original message – transformed into a cipher text by $f$ – corresponds to the one decrypted by $g$ . Equations between string diagrams such as these lead to proofs via diagrammatic reasoning, a powerful axiomatic technique that allows compositional reasoning about compound systems.

Our aim in this paper is to capture the notion of parametric algorithms within the abstract framework of resource theories. After a brief introduction to resource theories and their string diagrammatic language in Section 2, in Section 3 we define a notion of iteration bounded by an unspecified parameter, which we call $\star$ -iteration. Perhaps unexpectedly, we do not study traces (as, e.g., in monoidal streams [9]) but instead define a functorial construction: given a morphism $f\colon S\otimes A\to B\otimes S$ , we define $\tau^{k}_{S,(A),(B)}(f)\colon S\otimes A^{k}\to B^{k}\otimes S$ as its $k$ -fold iteration. Below we give a diagrammatic representation of $\tau^{k}_{S,(A),(B)}(f)$ , when $k=3$ .

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S1/iter_intro5a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S1/iter_intro5b}\end{matrix}$

Iterated morphism consumes and produces lists of resources of type $A$ and $B$ , respectively. The resource of type $S$ can be thought of as a state carried over by the computation. A similar construction is found in probabilistic programming languages [11, 24], where iteration is usually bounded. Interestingly, useful results can be proved about iteration without instantiating the parameter. To this end, we introduce a technique we dub the diagonal method that allows us to prove useful, general results that add to the arsenal of diagrammatic reasoning about abstract resource theories with parametric iteration.

Parametric iteration is a feature that extends the expressivity of resource theories. Our main application in this paper is motivated by cryptography, and the notion of negligibility in particular. To do this, we work within a probabilistic resource theoretical context. This is the category $\mathsf{FinStoch}_{\{1,0\}}$ of Boolean stochastic maps. It is both a Markov category and one that possesses a probabilistic choice structure, which we introduce in Section 4. As a notable property, the probabilistic case structure ensures a unique (up to isomorphism) normal form for probabilistic Boolean functions. This, in turn, allows us to derive a completeness result (Theorem 11). While not essential to the main developments of the paper, it provides an interesting alternative proof to the one found in [21].

Formally, we first move from symmetric monoidal categories to metric-enriched ones, so that morphisms, i.e. processes, are equipped with a notion of distance between them (see e.g. [8, 17]).

We reconcile metric-enrichment with the parameterized iteration construction in Section 5, where we introduce a notion of asymptotic equivalence on morphisms. This captures negligibility – also referred to as indistinguishability – between processes. Intuitively, two processes $f$ and $g$ , potentially involving parametric iterations, are considered indistinguishable if their distance approaches $0$ as the parameter $\sigma$ tends to $\infty$ . In related work [16], such notions of indistinguishability are studied in a bounded linear $\lambda$ -calculus.

Guided by cryptographic intuitions, we conclude with some examples. Notably, we formally prove that a randomly generated key is unlikely to be any specific key (Lemma 21), and show we can asymptotically approximate fair choice with weighted choice with the iterated von Neumann trick (Lemma 22). We also discuss how we can perform arithmetic over the cyclic groups of sizes $2^{\sigma}$ and $2^{\sigma}-1$ , which is useful for instance in Diffie-Hellman key exchange and Zero knowledge proofs.

The paper presents two theoretical contributions. We define the parametrized iteration construction on symmetric monoidal categories, prove that it forms a category, preserves several categorical structures, and admits an endofuctor $\tau^{\star}$ for parametrized iteration. We moreover define the notion of asymptotic equivalence on the parametrized iteration over a metric-enriched symmetric monoidal category, and show that it defines a congruence and is preserved under the application of $\tau^{\star}$ .

The paper includes appendices containing additional material and omitted proofs.

2 Symmetric Monoidal Categories as Resource Theories

In this section we give a brief introduction to symmetric monoidal categories (SMCs) and their associated graphical calculus [13, 23, 22] in terms of resource theories, following [6].

The basic data consists of objects $A,B,C,\ldots$ that we think of as types of resources, and morphisms $f\colon A\to B$ , which we think of as transformations that convert a resource of type $A$ into one of type $B$ . Morphisms can be composed sequentially: given $f\colon A\to B$ and $g\colon B\to C$ , their composite $f;g\colon A\to C$ represents performing $f$ followed by $g$ .

The monoidal product $\otimes$ lets us express having two resources at once – so $A\otimes C$ means having both $A$ and $C$ – and it extends to morphisms too: given $f\colon A\to B$ and $g\colon C\to D$ , the morphism $f\otimes g\colon A\otimes C\to B\otimes D$ describes applying $f$ and $g$ in parallel. There is also a void resource $I$ that acts neutrally under combination: $A\otimes I=A$ .

These ideas are captured visually using the graphical calculus of string diagrams. A resource type $A$ is drawn as a wire $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/id}\end{matrix}$ , and a transformation $f\colon A_{1}\otimes\ldots\otimes A_{n}\to B_{1}\otimes\ldots\otimes B_{m}$ is represented by a box $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/gen3}\end{matrix}$ with $n$ input wires on the left and $m$ output wires on the right. Composition of morphisms is shown by connecting boxes in sequence $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/seq\_comp}\end{matrix}$ , while the monoidal product corresponds to placing them side-by-side $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/par\_comp}\end{matrix}$ . The void resource $I$ corresponds to no wires at all – i.e., the empty diagram.

Resources can also be swapped according to the symmetry $\chi_{A,B}\colon A\otimes B\to B\otimes A$ , which is represented by a crossing of wires $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/symm}\end{matrix}$ .

Diagrams are subject to the axioms of symmetric monoidal categories (SMCs). However, note that equational reasoning in this setting amounts to deformation of diagrams without changing their topology. For example, naturality of symmetry amounts to sliding a box past a crossing of wires, illustrated as $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/symm_nat}\end{matrix}$ .

In the next section, where we introduce the parametric iteration construction, it will be convenient to explicitly track both the combination of resources via the monoidal product and the void resource. Therefore, following [4], we extend the graphical calculus with operations that introduce $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/op_2}\end{matrix}$ and discard $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/op_1}\end{matrix}$ the void resource, as well as split $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/op_4}\end{matrix}$ and combine $\begin{matrix}\includegraphics[scale={0.1}]{pics/S2/op_3}\end{matrix}$ resources. These operations are subject to the expected equations determined by the properties of the monoidal product.

Finally, note that all monoidal categories considered in this paper are taken to be strict, as justified by Mac Lane’s strictification theorem [18].

3 Parametric Iteration

We define a category of parametric iterations over a symmetric monoidal category. We do this by introducing the concept of $\star$ -iteration, which expresses the idea of iterating an operation a fixed yet unspecified number of times. We do not a priori choose how many times to iterate, the operations are parametrized over this yet to be specified choice of number of iterations.

We define parametric iteration over $\mathcal{C}$ in two stages. First we define the free iteration construction $\mathsf{FI}(\mathcal{C})$ which adds the relevant objects and operations which will be used to express iteration. We then quotient this category to create the parametric iteration construction $\textsf{PI}(\mathcal{C})$ over $\mathcal{C}$ , giving an interpretation to the added objects and operations.

We define the objects of $\mathsf{FI}(\mathcal{C})$ inductively as follows:

\frac{A\in\mathcal{C}}{\llparenthesis A\rrparenthesis\in\mathsf{FI}(\mathcal{C% })}\qquad\qquad\frac{A,B\in\mathsf{FI}(\mathcal{C})}{A\otimes B\in\mathsf{FI}(% \mathcal{C})}\qquad\qquad\frac{A\in\mathsf{FI}(\mathcal{C})}{A^{\star}\in% \mathsf{FI}(\mathcal{C})}

satisfying the equations $\llparenthesis I\rrparenthesis\otimes A=A=A\otimes\llparenthesis I\rrparenthesis$ , $\llparenthesis A\rrparenthesis\otimes\llparenthesis B\rrparenthesis=% \llparenthesis A\otimes B\rrparenthesis$ , and $(A\otimes B)\otimes C=A\otimes(B\otimes C)$ . Here $A^{\star}$ represents a $\star$ -tuple, that is a tuple of $A$ ’s, with the exact number of elements bounded by an external parameter.

Given a tuple of objects $\mathbf{A}=(A_{1},\dots,A_{n})$ , we write $\mathbf{A}\cdot\star=A_{1}^{\star}\otimes\dots\otimes A_{n}^{\star}$ , and for each $k\in{\mathbb{N}}$ , $\mathbf{A}\cdot k=A_{1}^{k}\otimes\dots\otimes A_{n}^{k}$ , following notation from [5], where $A^{k}$ is the $k$ -th power of $A$ with respect to $\otimes$ . In particular, $\mathbf{A}\cdot 1=A_{1}\otimes\dots\otimes A_{n}$ .

Morphisms of $\mathsf{FI}(\mathcal{C})$ are given inductively as follows:

\frac{f:A\to B\in\mathcal{C}}{\llparenthesis f\rrparenthesis:\llparenthesis A% \rrparenthesis\to\llparenthesis B\rrparenthesis}\qquad\frac{A\in\mathsf{FI}(% \mathcal{C})}{\textit{id}_{A}:A\to A}\qquad\frac{f:A\to B\quad g:B\to C}{f;g:A% \to C}\qquad\frac{f:A\to B\quad g:C\to D}{f\otimes g:A\otimes C\to B\otimes D}

\qquad\frac{A,B\in\mathsf{FI}(\mathcal{C})}{\chi_{A,B}:A\otimes B\to B\otimes A% }\qquad\frac{f:S\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes S}{\tau^{% \star}_{S,\mathbf{A},\mathbf{B}}(f):S\otimes\mathbf{A}\cdot\star\to\mathbf{B}% \cdot\star\otimes S}

satisfying the relevant equations making $\mathsf{FI}(\mathcal{C})$ into a symmetric monoidal category, together with the equations $\llparenthesis\textit{id}_{A}\rrparenthesis=\textit{id}_{\llparenthesis A\rrparenthesis}$ , $\llparenthesis f;g\rrparenthesis=\llparenthesis f\rrparenthesis;\llparenthesis g\rrparenthesis$ , $\llparenthesis\chi_{A,B}\rrparenthesis=\chi_{\llparenthesis A\rrparenthesis,% \llparenthesis B\rrparenthesis}$ , $\llparenthesis f\otimes g\rrparenthesis=\llparenthesis f\rrparenthesis\otimes% \llparenthesis g\rrparenthesis$ . The latter equations make $\llparenthesis-\rrparenthesis:\mathcal{C}\to\mathsf{FI}(\mathcal{C})$ sending $A$ to $\llparenthesis A\rrparenthesis$ and $f$ to $\llparenthesis f\rrparenthesis$ into a symmetric monoidal functor.

Here $\tau^{\star}$ is the operation which represents $\star$ -iteration, transforming a list of $\star$ -tuples $\mathbf{A}\cdot\star$ into a list of $\star$ -tuples $\mathbf{B}\cdot\star$ by going through the elements one by one, carrying over the state $S$ between iterations. We annotate $\tau^{\star}$ by lists telling us exactly how the input and output of $f$ is divided into different tuples. For instance, if $f:S\otimes A^{2}\to B\otimes S$ , we could either create $\tau^{\star}_{S,(A^{2}),(B)}(f):S\otimes(A^{2})^{\star}\to B^{\star}\otimes S$ or $\tau^{\star}_{S,(A,A),(B)}(f):S\otimes A^{\star}\otimes A^{\star}\to B^{\star}\otimes S$ , where $(A^{2})^{\star}$ is a $\star$ -tuple of elements of $A^{2}$ , and $A^{\star}\otimes A^{\star}$ are two $\star$ -tuples of elements of $A$ .

String diagrammatically, we denote $\tau^{\star}_{S,\mathbf{A},\mathbf{B}}(f)$ as follows:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/starop_a}\end{matrix}\quad% \mapsto\quad\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/starop_b}\end{matrix}$

Here we mark state wires with a $\bullet$ , and the $\star$ -tuples with an interrupted wire. Each non-state wire is part of a different tuple. We may use multiple or no state wires as well.

We give an interpretation of iteration by defining $\tau^{k}$ as an operation on symmetric monoidal categories describing a constant number of $k$ iterations. Given a symmetric monoidal category $\mathcal{C}$ , we can inductively define operations $\textsf{push}^{k}_{\mathbf{A}}:\mathbf{A}\cdot 1\otimes\mathbf{A}\cdot k\to% \mathbf{A}\cdot(k+1)$ and $\textsf{pop}^{k}_{\mathbf{A}}:\mathbf{A}\cdot(k+1)\to\mathbf{A}\cdot 1\otimes% \mathbf{A}\cdot k$ which respectively pushes and pops the first element of each tuple of objects in $\mathbf{A}\cdot(k+1)$ . For instance, if $\mathbf{A}=(X,Y)$ , then $\textsf{push}^{3}_{\mathbf{A}}:X\otimes Y\otimes X^{2}\otimes Y^{2}\to X^{3}% \otimes Y^{3}$ simply swaps the second and third element.

Given a morphism $f:S\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes S$ in $\mathcal{C}$ , we inductively define $\tau^{k}_{S,\mathbf{A},\mathbf{B}}(f):S\otimes\mathbf{A}\cdot k\to\mathbf{B}% \cdot k\otimes S$ for each $k\in{\mathbb{N}}$ as:

$\blacksquare$

$\tau^{0}_{S,\mathbf{A},\mathbf{B}}(f)=\textit{id}_{S}$ ,
$\blacksquare$

$\tau^{k+1}_{S,\mathbf{A},\mathbf{B}}(f)=(\textit{id}_{S}\otimes\textsf{pop}^{k% }_{\mathbf{A}});(f\otimes\textit{id}_{\mathbf{A}\cdot k});(\textit{id}_{% \mathbf{B}\cdot 1}\otimes\tau^{k}_{S,\mathbf{A},\mathbf{B}}(f));(\textsf{push}% ^{k}_{\mathbf{B}}\otimes\textit{id}_{S})$ .

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/starop_a}\end{matrix}\quad% \mapsto\quad\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/iterop_b}\end{matrix}$

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/iter_def_a}\end{matrix}% \quad:=\quad\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/iter_def_b}% \end{matrix}\qquad\quad\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/% iter_def_c}\end{matrix}\quad:=\quad\begin{matrix}\includegraphics[scale={0.1}]% {pics/S3/iter_def_d}\end{matrix}$

Contrary to $\tau^{\star}$ , the annotations for $\tau^{k}$ serve a further clarifying role, as they are also necessary for removing ambiguity even in those instances where the type of the produced morphism is known. Without this specification, the input may be wrongly distributed into separate tuples. For instance, a $\tau^{3}$ iteration having $A^{6}$ as input, could consider this either as two triples of $A$ , or one triple of $A^{2}$ , which lead to different interpretations. In terms of string diagrams, we can keep the convention that each string represents a different tuple, which avoids the need for putting annotations in the string diagrams.

Example 1.

Suppose $f:A\otimes A\to B$ , then $\tau^{2}_{1,(A,A),(B)}(f)$ and $\tau^{2}_{1,(A^{2}),(B)}(f)$ have the same type but yield two different results, represented respectively as string diagrams as follows:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/ex_anno_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S3/ex_anno_b}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/ex_anno_c}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S3/ex_anno_d}\end{matrix}$

For any $k\in{\mathbb{N}}$ , we define a functor $S_{k}:\mathsf{FI}(\mathcal{C})\to\mathcal{C}$ inductively as follows, first on objects:

$\blacksquare$

$S_{k}(\llparenthesis A\rrparenthesis)=A$ ,
$\blacksquare$

$S_{k}(A\otimes B)=S_{k}(A)\otimes S_{k}(B)$ ,
$\blacksquare$

$S_{k}(A^{\star})=(S_{k}(A))^{k}$ .

For $\mathbf{A}=(A_{1},\dots,A_{n})$ , then $S_{k}(\mathbf{A})=(S_{k}(A_{1}),\dots,S_{k}(A_{n}))$ . $S_{k}$ is defined on morphisms as:

$\blacksquare$

$S_{k}(\textit{id}_{A})=\textit{id}_{S_{k}(A)}$ ,
$\blacksquare$

$S_{k}(\llparenthesis f\rrparenthesis)=f$ ,
$\blacksquare$

$S_{k}(f;g)=S_{k}(f);S_{k}(g)$ ,
$\blacksquare$

$S_{k}(f\otimes g)=S_{k}(f)\otimes S_{k}(g)$ ,
$\blacksquare$

$S_{k}(\chi_{A,B})=\chi_{S_{k}(A),S_{k}(B)}$ .

For $f:S\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes S$ , then $S_{k}(\tau^{\star}_{S,\mathbf{A},\mathbf{B}}(f))=\tau^{k}_{S,S_{k}(\mathbf{A})% ,S_{k}(\mathbf{B})}(S_{k}(f))$ .

Definition 2.

Two morphisms $f,g:A\to B$ in $\mathsf{FI}(\mathcal{C})$ are $\star$ -equivalent if for any $k\in{\mathbb{N}}$ , $S_{k}(f)=S_{k}(g)$ . The parametric iteration category $\textsf{PI}(\mathcal{C})$ of $\mathcal{C}$ is defined as $\mathsf{FI}(\mathcal{C})$ quotiented over this notion of $\star$ -equivalence.

We have a symmetric monoidal functor $\llparenthesis-\rrparenthesis:\mathcal{C}\to\textsf{PI}(\mathcal{C})$ and for each $k\in{\mathbb{N}}$ a symmetric monoidal functor $S_{k}:\textsf{PI}(\mathcal{C})\to\mathcal{C}$ . We consider the image of $\llparenthesis-\rrparenthesis$ in $\textsf{PI}(\mathcal{C})$ as the constant fragment of $\textsf{PI}(\mathcal{C})$ . It holds that $S_{k}\circ\llparenthesis-\rrparenthesis$ is the identity functor on $\mathcal{C}$ for each $k\in{\mathbb{N}}$ .

Before we continue on and prove results regarding $\star$ -equivalence, we introduce a powerful proof technique we call the diagonal method. Consider $\textsf{PI}(\textsf{PI}(\mathcal{C}))$ , which has two nested parametric iteration constructions, the second we label with $\star^{\prime}$ . We construct a symmetric monoidal functor $M:\textsf{PI}(\textsf{PI}(\mathcal{C}))\to\textsf{PI}(\mathcal{C})$ that unifies the two iterations, i.e. it satisfies:

$\blacksquare$

$M(A^{\star^{\prime}})=M(A^{\star})=(MA)^{\star}$ ,
$\blacksquare$

$M(\tau^{\star^{\prime}}_{S,\mathbf{A},\mathbf{B}}(f))=M(\tau^{\star}_{S,% \mathbf{A},\mathbf{B}}(f))=\tau^{\star}_{MS,M\mathbf{A},M\mathbf{B}}(Mf)$ .

Lemma 3.

There is a functor $M:\textsf{PI}(\textsf{PI}(\mathcal{C}))\to\textsf{PI}(\mathcal{C})$ satisfying the properties above.

Proof.

Let us consider the obvious functor $M^{\prime}:\mathsf{FI}(\textsf{PI}(\mathcal{C}))\to\textsf{PI}(\mathcal{C})$ . We prove that $M^{\prime}$ preserves $\star$ -equivalence. Let $f$ and $g$ be $\star$ -equivalent morphisms in $\mathsf{FI}(\textsf{PI}(\mathcal{C}))$ , then for any $k\in{\mathbb{N}}$ , $S_{k}(f)=S_{k}(g)$ in $\textsf{PI}(C)$ . So for any $r\in{\mathbb{N}}$ , $S_{r}(S_{k}(f))=S_{r}(S_{k}(g))$ in $\mathcal{C}$ . Note that the $S_{k}$ instantiates the $\star^{\prime}$ , and the $S_{r}$ the $\star$ .

Now, for any $k\in{\mathbb{N}}$ , $S_{k}(M^{\prime}f)=S_{k}(S_{k}(f))=S_{k}(S_{k}(g))=S_{k}(M^{\prime}g)$ , hence $M^{\prime}f=M^{\prime}g$ . So $M^{\prime}$ preserves $\star$ -equivalence and can be factored through $\textsf{PI}(\textsf{PI}(\mathcal{C}))$ creating $M$ . $\hfill\blacktriangleleft$

In practice, this allows us to prove $\star$ -equivalence between morphisms by instantiating some of the iteration operations but not necessarily all. We can do this as long as we can find a separation into two iteration types, marking a choice of top level $\star$ -iterations as $\star^{\prime}$ in a way that type checks. We now have sufficient tools to prove some useful properties.

Lemma 4.

The following equations hold:

\begin{array}[]{r@{\;}c@{\;}l@{\qquad}r@{\;}c@{\;}l}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S3/star_id_a}\end{matrix}&\stackrel{{% \scriptstyle(\ref*{def:tid})}}{{=}}&\begin{matrix}\includegraphics[scale={0.1}% ]{pics/S3/star_id_b}\end{matrix}&\begin{matrix}\includegraphics[scale={0.1}]{% pics/S3/star_swap_a}\end{matrix}&\stackrel{{\scriptstyle(\ref*{def:tswap})}}{{% =}}&\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/star_swap_b}\end{% matrix}\\ \begin{matrix}\includegraphics[scale={0.1}]{pics/S3/star_comp_a}\end{matrix}&% \stackrel{{\scriptstyle(\ref*{def:tcomp})}}{{=}}&\begin{matrix}% \includegraphics[scale={0.1}]{pics/S3/star_comp_b}\end{matrix}&\begin{matrix}% \includegraphics[scale={0.1}]{pics/S3/star_mono_a}\end{matrix}&\stackrel{{% \scriptstyle(\ref*{def:tmono})}}{{=}}&\begin{matrix}\includegraphics[scale={0.% 1}]{pics/S3/star_mono_b}\end{matrix}\end{array}

Proof.

Let us prove (3), the other equations are shown in Appendix A. We use the diagonal method, instantiating only the outer iteration operations. We perform induction on those instantiations:

Induction basis:: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/comp_IB_a}\end{matrix}% \stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale% ={0.1}]{pics/S3/comp_IB_b}\end{matrix}\stackrel{{\scriptstyle(\text{def})}}{{=% }}\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/comp_IB_c}\end{matrix}$
Induction step:: $\ \begin{matrix}\includegraphics[scale={0.1}]{pics/S3/comp_IS_a}\end{matrix}% \stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale% ={0.1}]{pics/S3/comp_IS_b}\end{matrix}\stackrel{{\scriptstyle(\text{hypo})}}{{% =}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/comp_IS_c}\end{matrix}% \stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale% ={0.1}]{pics/S3/comp_IS_d}\end{matrix}$

$\hfill\blacktriangleleft$

Corollary 5.

There is a symmetric monoidal endofunctor on $\textsf{PI}(\mathcal{C})$ given by $A\mapsto A^{\star}$ and $f:A\to B\mapsto\tau^{\star}_{I,(A),(B)}(f)$ .

The following property is particularly useful in forthcoming examples:

Lemma 6 (Newton’s cradle).

For any $f\colon S\to Z,g\colon Z\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes Z,% h\colon S\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes S$ , if $\;\;\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_a}\end{matrix% }\stackrel{{\scriptstyle(\text{I})}}{{=}}\begin{matrix}\includegraphics[scale=% {0.1}]{pics/S3/Newton_S_b}\end{matrix}\;\;$ then $\;\;\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_c}\end{matrix% }=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_d}\end{matrix}$ .

Proof.

We use the diagonal method, and choose to instantiate only the top level iterations. We show by induction on $k\in{\mathbb{N}}$ that for each instantiation by $k$ the equation holds.

Induction basis:: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_IBb_a}\end{matrix}% \stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale% ={0.1}]{pics/S3/Newton_IBb_b}\end{matrix}\stackrel{{\scriptstyle(\text{def})}}% {{=}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_IBb_c}\end{matrix}$
Induction step:: $\ \begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_ISb_a}\end{matrix% }\stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scal% e={0.1}]{pics/S3/Newton_ISb_b}\end{matrix}\stackrel{{\scriptstyle(\text{I})}}{% {=}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_ISb_c}\end{% matrix}\stackrel{{\scriptstyle(\text{hypo})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S3/Newton_ISb_d}\end{matrix}\stackrel{{% \scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale={0.1}]{% pics/S3/Newton_ISb_e}\end{matrix}$

$\hfill\blacktriangleleft$

Let us look at two examples which occur in $\textsf{PI}(\mathcal{C})$ for any symmetric monoidal category $\mathcal{C}$ .

Example 7.

Consider zipping two $\star$ -tuples using $\tau_{I,(A,B),(A\otimes B)}(\textit{id}_{A\otimes B})$ :

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/zip_def}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/zip_ex_a}\end{matrix}$ = $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/zip_ex_b}\end{matrix}$

On the right we see an example instantiation performing three iterations. The zip operations gives one direction of an isomorphism between $A^{\star}\otimes B^{\star}$ and $(A\otimes B)^{\star}$ .

Example 8.

The morphism $\tau^{\star}_{A,(A),(A)}(\textit{id}_{A^{2}}):A^{\star}\otimes A\to A^{\star}\otimes A$ pushes a new element to the front of a $\star$ -tuple, and pops the last element from the $\star$ -tuple to make room.

$\tau^{\star}_{A,(A),(A)}(\textit{id}_{A^{2}})=\begin{matrix}\includegraphics[s% cale={0.1}]{pics/S3/pushpop_def}\end{matrix}\qquad\qquad\tau^{k}_{A,(A),(A)}(% \textit{id}_{A^{2}})=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/% pushpop_a}\end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/% pushpop_b}\end{matrix}$

We can use this to cycle forward and backward through the elements of a $\star$ -tuple. We take $\textsf{cycle}_{A}=\tau^{\star}_{A,(A),(A)}(\textit{id}_{A^{2}});\chi_{A^{% \star},A}$ and $\textsf{cycle-back}_{A}=\tau^{\star}_{A\otimes A^{\star},(),()}(\textsf{cycle}% _{A})$ ,

$\textsf{cycle}_{A}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/cycle}% \end{matrix}\qquad\qquad\textsf{cycle-back}_{A}=\begin{matrix}\includegraphics% [scale={0.1}]{pics/S3/cycle2}\end{matrix}$

Here we cycle back by cycling forward one less than what is needed to get back to where we started. Concretely, note that $S_{k}(\textsf{cycle}_{A})=\chi_{A^{k},A}$ , and for any $a,b\in{\mathbb{N}}$ , $\chi_{A^{a+1},A^{b}};\chi_{A^{a+b},A}=\chi_{A^{b},A^{b+1}}$ , so by induction, $S_{k}(\textsf{cycle-back}_{A})=(\chi_{A^{k},A})^{k}=\chi_{A,A^{k}}$ , so $S_{k}(\textsf{cycle-back}_{A};\textsf{cycle}_{A})=\chi_{A,A^{k}};\chi_{A^{k},A% }=\textit{id}_{A^{k+1}}$ . We conclude that:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/cycle_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S3/cycle_b}\end{matrix}$

4 Reasoning with Probabilities and Distances

To model richer computational behaviors, we consider symmetric monoidal categories with additional properties and structure. In particular, for probabilistic computations, we focus on metric-enriched symmetric monoidal categories and Markov categories [10].

\begin{array}[]{c@{\quad}c@{\quad}c}\begin{matrix}\includegraphics[scale={0.1}% ]{pics/S4/ax/markov/assoc/lhs}\end{matrix}\stackrel{{\scriptstyle(\ref*{ax:% copyas})}}{{=}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/markov/% assoc/rhs}\end{matrix}&\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/% markov/unit/lhs}\end{matrix}\stackrel{{\scriptstyle(\ref*{ax:copyun})}}{{=}}% \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/id}\end{matrix}&\begin{% matrix}\includegraphics[scale={0.1}]{pics/S4/ax/markov/comm/lhs}\end{matrix}% \stackrel{{\scriptstyle(\ref*{ax:copyco})}}{{=}}\begin{matrix}\includegraphics% [scale={0.1}]{pics/S4/copy}\end{matrix}\\ &\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/markov/nat/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:discardnat})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/discard}\end{matrix}&\\ \hline\cr\lx@intercol\hfil\begin{array}[]{c@{\quad}c@{\quad}c@{\quad}c}\begin{% matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/one/lhs}\end{matrix}% \stackrel{{\scriptstyle(\ref*{ax:onedet})}}{{=}}\begin{matrix}\includegraphics% [scale={0.1}]{pics/S4/ax/pchoice/one/rhs}\end{matrix}&\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/zero/lhs}\end{matrix}% \stackrel{{\scriptstyle(\ref*{ax:zerodet})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/zero/rhs}\end{matrix}&\begin{% matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiBool/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:phiBool})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiBool/rhs}\end{matrix}&% \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiOne/lhs}\end% {matrix}\stackrel{{\scriptstyle(\ref*{ax:phiOne})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiOne/rhs}\end{matrix}\end{% array}\hfil\lx@intercol\\[15.0pt] \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiAs/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:phias})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiAs/rhs}\end{matrix}&\begin% {matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiIdemp/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:phiIdemp})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiIdemp/rhs}\end{matrix}&% \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiCo/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:phico})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiCo/rhs}\end{matrix}\\[15.0% pt] \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiI/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:phiI})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/discardB}\end{matrix}&\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiTimes/lhs}\end{matrix}% \stackrel{{\scriptstyle(\ref*{ax:phiTimes})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiTimes/rhs}\end{matrix}&% \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiNat/lhs}\end% {matrix}\stackrel{{\scriptstyle(\ref*{ax:phinat})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/ax/pchoice/phiNat/rhs}\end{matrix}\end{array}

Figure 1: Axioms for Markov categories (top) and probabilistic choice (bottom). Here

f\colon A\to B

,

q=1-p

,

c=\frac{(1-a)b}{1-ab}

and

d=ab

.

Definition 9.

A Markov category with probabilistic choice is a symmetric monoidal category equipped with operations $!_{A}\colon A\to I$ , $\blacktriangleleft_{A}\colon A\to A\otimes A$ , $\langle p\rangle\colon I\to\mathbb{B}$ and $\phi_{A}\colon A\otimes\mathbb{B}\otimes A\to A$ , represented in string diagrams, respectively, as

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/discard}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/copy}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/p}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/phi}\end{matrix}$

where $p\in[0,1]$ , $\mathbb{B}$ is a designated object and $A$ is any object, and such that the axioms in Figure 1 hold. That is:

$\blacksquare$

$(\blacktriangleleft_{A},!_{A})$ is a cocommutative comonoid, that is $\blacktriangleleft_{A}$ is associative (1), cocommutative (1) and $!_{A}$ is the unit (1),
$\blacksquare$

$\blacktriangleleft_{A}$ and $!_{A}$ are coherent with the monoidal structure,
$\blacksquare$

$!_{A}$ is natural (1),
$\blacksquare$

$\langle 1\rangle$ and $\langle 0\rangle$ are deterministic ((1) and (1)),
$\blacksquare$

$\phi_{A}$ is coherent with the monoidal structure ((1) and (1)),
$\blacksquare$

$\phi_{A}$ is natural in $A$ (1),
$\blacksquare$

$\phi_{A}^{p}$ –where $\phi_{A}^{p}$ is $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/phi_p2}\end{matrix}$ , often simply $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/phi_p}\end{matrix}$ –is a convex algebra, that is, $\phi^{p}_{A}$ is idempotent (1) and satisfies parametric associativity (1) and commutativity (1),
$\blacksquare$

$\phi$ and $\langle 1\rangle$ , $\langle 0\rangle$ interact via (1) and (1).

The $\mathbb{B}$ represents the type of two bit values, $1$ and $0$ . $\langle p\rangle$ describes a weighted coin flip, which has a chance of $p$ of producing $1$ , and a chance of $1-p$ of producing $0$ . The $\phi$ represents an if-gate, choosing between two results of the same type using a bit as an argument.

\begin{array}[]{c@{\qquad\qquad}c}\begin{matrix}\includegraphics[scale={0.1}]{% pics/S4/dlaws/phiZero/lhs}\end{matrix}\stackrel{{\scriptstyle(\ref*{ax:phiZero% })}}{{=}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/dlaws/phiZero/rhs% }\end{matrix}&\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/dlaws/phidet% /lhs}\end{matrix}\stackrel{{\scriptstyle(\ref*{ax:phidet})}}{{=}}\begin{matrix% }\includegraphics[scale={0.1}]{pics/S4/dlaws/phidet/rhs}\end{matrix}\\ \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/dlaws/decomp/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:boolsplit})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/dlaws/decomp/rhs}\end{matrix}&\begin{% matrix}\includegraphics[scale={0.1}]{pics/S4/dlaws/hcopy/lhs}\end{matrix}% \stackrel{{\scriptstyle(\ref*{ax:phidistr})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/dlaws/hcopy/rhs}\end{matrix}\end{array}

Figure 2: Derived laws for Markov categories with probabilistic choice.

Lemma 10.

The laws in Figure 2 hold in any Markov category with probabilistic choice.

Proof.

We give a proof only for (2), the rest can be found in Appendix C.

\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/dlaws/phidet/lhs}\end{% matrix}\stackrel{{\scriptstyle(\ref*{ax:phinat})}}{{=}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/dlaws/phidet/step}\end{matrix}\stackrel{% {\scriptstyle(\ref*{ax:phiTimes})}}{{=}}\begin{matrix}\includegraphics[scale={% 0.1}]{pics/S4/dlaws/phidet/rhs}\end{matrix}

$\hfill\blacktriangleleft$ Our leading example of Markov category with probabilistic choice is $\mathsf{FinStoch}$ , the category of sets and stochastic maps. Objects are sets and morphisms $f\colon A\to B$ are functions $A\to\mathcal{D}B$ mapping each $a\in A$ to a finitely-supported discrete probability distribution over $B$ . We represent a distribution as a function $v:A\to[0,1]$ with finite support $\texttt{supp}(v):=\{a\in A\mid v(a)>0\}$ and such that $\sum_{a\in A}v(a)=1$ , or, alternatively, as a formal sum $\sum_{i}{p_{i}\ket{a_{i}}}$ , where the $\ket{\cdot}$ notation is used to separate the elements $a_{i}\in A$ from their associated probability $p_{i}\in[0,1]$ .

We write $f(b|a)$ for $f(a)(b)$ , representing the probability that $f$ returns $b$ , given $a$ . For two stochastic maps $f\colon A\to B,g\colon B\to C$ , their composition is defined by summing over the middle variable, i.e. $(f;g)(c\mid a):=\sum_{b\in B}g(c\mid b)f(b\mid a)$ . Identities $id_{A}\colon A\to A$ map each $a\in A$ to the Dirac distribution at $a$ , i.e. $id_{A}(a):=\ket{a}$ .

Given two distributions $v\in\mathcal{D}A$ and $u\in\mathcal{D}B$ , their product $v\otimes w\in\mathcal{D}{(A\times B)}$ is given by $v\otimes u(a,b):=v(a)u(b)$ . This yields a symmetric monoidal structure, with the monoidal product $\otimes$ being the cartesian product of sets $\times$ on objects and with monoidal unit the singleton set $I:=\{\bullet\}$ . For arrows $f\colon A\to B$ and $g\colon C\to D$ , $f\otimes g\colon A\otimes C\to B\otimes D$ is defined as $f\otimes g(b,d|a,c):=f(b|a)g(d|c)$ , and symmetries $\chi_{A,B}\colon A\otimes B\to B\otimes A$ as $\chi_{A,B}(a,b):=\ket{b}\otimes\ket{a}$ .

The comonoid structure is given by $\blacktriangleleft_{A}(a):=\ket{a}\otimes\ket{a}$ and $!_{A}(a):=\ket{\bullet}$ , while for the probabilistic choice structure we take as choice object the set of Booleans $\{1,0\}$ and, for any $p\in[0,1]$ , we define $\langle p\rangle\colon\{\bullet\}\to\{1,0\}$ as $\langle p\rangle(\bullet):=p\ket{1}+(1-p)\ket{0}$ and $\phi_{A}\colon A\otimes\{1,0\}\otimes A\to A$ as $\phi_{A}(a,1,b):=\ket{a}$ and $\phi_{A}(a,0,b):=\ket{b}$ . Note that $\phi^{p}_{A}(a,b)=p\ket{a}+(1-p)\ket{b}$ .

Throughout the rest of the paper we will work in $\mathsf{FinStoch}_{\{1,0\}}$ , the subcategory of $\mathsf{FinStoch}$ consisting of stochastic maps between sets that are powers of the booleans. The structure of Markov category with probabilistic choice, introduced here, is novel and it offers an alternative presentation of $\mathsf{FinStoch}_{\{1,0\}}$ to the one in [21]. In particular:

Theorem 11.

the axioms in Figure 1 are complete for $\mathsf{FinStoch}_{\{1,0\}}$ .

The interested reader can find the details in Appendix B.

As an example of diagrammatic reasoning in $\mathsf{FinStoch}_{\{1,0\}}$ we look at the one-time-pad protocol on a single bit. We regard $\langle\frac{1}{2}\rangle\colon I\to\mathbb{B}$ as an operation that produces a randomly generated bit, and the xor $\oplus\colon\mathbb{B}\otimes\mathbb{B}\to\mathbb{B}$ , defined below on the left, as an operation that encrypts and decrypts a bit.

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/xor}\end{matrix}$ := $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/xor_def}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/otp_main}\end{matrix}$

The equation on the right expresses the correctness of the protocol: encoding and decoding with the same randomly generated bit gets the same result, and that to an adversary the encrypted message looks completely random. We prove correcteness by equational reasoning:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/otp_proof}\end{matrix}$

The equations use the fact that $\oplus$ is deterministic, associative, idempotent, unitary with respect to $\langle 0\rangle$ and nullary with respect to $\langle\frac{1}{2}\rangle$ . All of these properties can be proved via the axioms of Markov categories with probabilistic choice. For example the fact that $\langle\frac{1}{2}\rangle$ is absorbing for $\oplus$ is proved using the laws in Figure 2 as follows:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/xor_null}\end{matrix}$

Looking at $\textsf{PI}(\mathsf{FinStoch}_{\{1,0\}})$ , the above example can be extended to operations on $\mathbb{B}^{\star}$ , encrypting and decrypting $\star$ -tuples of bits. We now show that the parametric iteration construction preserves the structure of Markov categories with probabilistic choice.

Lemma 12.

If $\mathcal{C}$ is a Markov category with probabilistic choice, then so is $\textsf{PI}(\mathcal{C})$ .

Proof.

For $\mathbb{B}$ we can take $\llparenthesis\mathbb{B}\rrparenthesis$ , and for $\langle p\rangle$ we take $\llparenthesis\langle p\rangle\rrparenthesis$ . We define discard $!_{A\star}$ , copy $\blacktriangleleft_{A\star}$ and case $\phi_{A^{\star}}$ for $\textsf{PI}(\mathcal{C})$ inductively on objects, with their definition on $A^{\star}$ being:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/discard_star_a}\end{matrix}$ := $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/discard_star_b}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/copy_star_a}\end{matrix}$ := $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/copy_star_b}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/if_star_a}\end{matrix}$ := $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/if_star_b}\end{matrix}$

The relevant properties can be shown using the diagonal method, with the naturality equations in particular being instances of Newton’s cradle. $\hfill\blacktriangleleft$

4.1 Quantitative Reasoning

The theory developed in the previous section allows for exact reasoning about boolean stochastic maps, enabling us to derive precise equalities between them.

However, in some cases – especially when parametric iteration is involved – we are interested in reasoning about approximate equivalence instead. To do so, we must move to metric-enriched symmetric monoidal categories. We begin by recalling some basic definitions.

Definition 13.

A metric space $(A,d)$ consists of a set $A$ and a distance function $d:A\times A\to[0,\infty)$ such that for all $a,b,c\in A$ :

d(a,b)=0\Leftrightarrow a=b,\qquad d(a,b)=d(b,a),\qquad d(a,c)\leq d(a,b)+d(b,% c).

(2)

A morphism between metric spaces $f:(A,d_{A})\twoheadrightarrow(B,d_{B})$ is given by a non-expansive function $f:A\to B$ , that is a function satisfying $d_{B}(f(a),f(b))\leq d_{A}(a,b)$ for all $a,b\in A$ .

Definition 14.

The category $\mathbb{M}$ has metric spaces as objects and non-expansive functions as arrows. This is a monoidal category, with $\otimes$ defined on objects as the metric space $(A\otimes B,d_{A\otimes B})$ , where $A\otimes B$ is the cartesian product of sets and $d_{A\otimes B}((a,b),(a^{\prime},b^{\prime})):=d_{A}(a,a^{\prime})+d_{B}(b,b^{% \prime})$ , and on arrows as $(f\otimes g)(a,c):=(f(a),g(c))$ , for every $f\colon(A,d_{A})\twoheadrightarrow(B,d_{B})$ and $g\colon(C,d_{C})\twoheadrightarrow(D,d_{D})$ .

Our objects of study in this section are metric enriched monoidal categories, or categories enriched over $\mathbb{M}$ . Unfolding the definition, a metric enriched monoidal category is a category whose homs are metric spaces, such that:

d_{A\to C}(f;g,f^{\prime};g^{\prime})\leq d_{A\to B}(f,f^{\prime})+d_{B\to C}(% g,g^{\prime})

(3)

and

d_{A\otimes C\to B\otimes D}(f\otimes g,f^{\prime}\otimes g^{\prime})\leq d_{A% \to B}(f,f^{\prime})+d_{C\to D}(g,g^{\prime}).

(4)

Lemma 15.

$\mathsf{FinStoch}$ is a metric enriched symmetric monoidal category.

Proof.

For each set $A$ , we can define a metric $\mathsf{tv}_{A}$ on $\mathcal{D}A$ called the total variation metric (see e.g. [15]). We give two equivalent formulations of $\mathsf{tv}_{A}$ below, for any $v,w\in\mathcal{D}A$ .

\mathsf{tv}_{A}(v,w):=\sum_{a\in\texttt{supp}(v)\cup\texttt{supp}(w)}\frac{|v(% a)-w(a)|}{2}=1-\sum_{a\in\texttt{supp}(v)\cap\texttt{supp}(w)}\texttt{min}(v(a% ),w(a))

We take as distance between arrows $d_{A\to B}(f,g):=\texttt{max}_{a\in A}\mathsf{tv}_{B}(f(a),g(a))$ , for every $f,g\colon A\to B$ in $\mathsf{FinStoch}$ . This choice of distance makes $\mathsf{FinStoch}$ metric enriched (see Example 3.2.7 in [12]). $\hfill\blacktriangleleft$

Just as we approached exact reasoning equationally, we now aim to reason quantitatively in a similar style. To this end, we introduce a proof system that axiomatizes distances between morphisms of metric-enriched Markov categories with probabilistic choice.

\begin{array}[]{ccccc}\frac{}{f\equiv_{0}f}\quad\frac{}{f\equiv_{1}g}&\frac{f% \equiv_{\delta}g}{g\equiv_{\delta}f}&\frac{f\equiv_{\delta}g\quad g\equiv_{% \delta^{\prime}}h}{f\equiv_{\delta+\delta^{\prime}}h}&\frac{f\equiv_{\delta}g% \quad{\delta}\leq{\delta^{\prime}}}{f\equiv_{\delta^{\prime}}g}&\frac{f\equiv_% {\delta}f^{\prime}\quad g\equiv_{\delta}g^{\prime}}{(f\otimes id_{\mathbb{B}}% \otimes g);\phi_{X}\equiv_{\delta}(f^{\prime}\otimes id_{\mathbb{B}}\otimes g^% {\prime});\phi_{X}}\\[10.0pt] \frac{f\equiv_{\delta}f^{\prime}}{f;g\equiv_{\delta}f^{\prime};g}&\frac{g% \equiv_{\delta}g^{\prime}}{f;g\equiv_{\delta}f;g^{\prime}}&\frac{f\equiv_{% \delta}f^{\prime}}{f\otimes g\equiv_{\delta}f^{\prime}\otimes g}&\frac{g\equiv% _{\delta}g^{\prime}}{f\otimes g\equiv_{\delta}f\otimes g^{\prime}}&\frac{f% \equiv_{\delta}f^{\prime}\quad g\equiv_{\gamma}g^{\prime}}{(f\otimes g);\phi^{% p}_{X}\equiv_{p\cdot\delta+(1-p)\cdot\gamma}(f^{\prime}\otimes g^{\prime});% \phi^{p}_{X}}\end{array}

(5)

We write $f\equiv_{\delta}g$ to say that $f$ and $g$ , of the same type, are provably at most $\delta$ away from each other. Moreover, we say that a proof system is sound if $f\equiv_{\delta}g$ implies $d(f,g)\leq\delta$ , and is complete if $f\equiv_{d(f,g)}g$ for each pair of morphisms $f, g$ of the same type.

Note that a sound proof system allows one to prove upper bounds to the actual distance between morphisms. As such, certain proofs give better bounds than others, allowing one to improve on a proof of distance by finding different routes. In particular, in order to prove security, one would like to prove that certain distances are below a level of allowed risk $\varepsilon$ .

We now show that the proof system above is sound and complete for $\mathsf{FinStoch}_{\{1,0\}}$ , equipped with the total variation distance.

This approach varies from the total variation treatment in [17], where the monoidal product combines different cases (disjunctive), whereas in our case the monoidal product combines resources (conjunctive).

Lemma 16.

The proof system in (5) is sound and complete for $\mathsf{FinStoch}_{\{1,0\}}$ .

Proof.

See Appendix C. $\hfill\blacktriangleleft$

5 Asymptotic Equivalence

For a metric enriched symmetric monoidal category $\mathcal{C}$ , we can equip $\textsf{PI}(\mathcal{C})$ with a notion of asymptotic equivalence. A nonnegative function $f\colon{\mathbb{N}}\to[0,\infty)$ approaches zero, written as $\lim_{k\to\infty}f(k)=0$ , if for any possible threshold $\varepsilon\in(0,\infty)$ there is some point $N\in{\mathbb{N}}$ after which the function is below $\varepsilon$ . Symbolically: $\forall\varepsilon>0.\,\exists N>0.\,\forall k\geq N.\,f(k)<\varepsilon$ .

From the perspective of cryptography, we consider $\varepsilon$ the risk factor we are trying to beat, or the allowable failure rate of our algorithm. Then $N>0$ is the minimum security parameter to guarantee that the actual probability of failure is below the allowable risk.

The following definition captures indistinguishability between morphisms in $\textsf{PI}(\mathcal{C})$ , given that they may be investigated a polynomial number of times by the distinguisher (e.g. adversary), and this distinguisher may choose a polynomial amount of inputs and study each probabilistically generated output.

Definition 17 (Asymptotic Equivalence).

For a metric enriched symmetric monoidal category $\mathsf{C}$ , the asymptotic equivalence relation $\equiv$ on morphisms of $\textsf{PI}(\mathsf{C})$ is defined as follows:

f\equiv g\iff\forall a\in{\mathbb{N}}.\;\lim_{k\to\infty}k^{a}\cdot d(S_{k}(f)% ,S_{k}(g))=0\qquad\text{for any $f,g\colon X\to Y$ in $\textsf{PI}(\mathsf{C})% $.}

Proposition 18.

$\equiv$ is preserved under sequential composition and parallel composition.

Proof.

Suppose $f\equiv f^{\prime}$ and $g\equiv g^{\prime}$ . Take $k\in{\mathbb{N}}$ , and $\varepsilon>0$ , then by assumption on $\varepsilon/2$ there are $N$ and $M$ such that if $n\geq N$ and $n\geq M$ , then respectively $n^{k}\cdot d(S_{n}(f),S_{n}(f^{\prime}))<\varepsilon/2$ and $n^{k}\cdot d(S_{n}(g),S_{n}(g^{\prime}))<\varepsilon/2$ . Taking $K=\max(N,M)$ , then for $n\geq K$ we get $n^{k}\cdot d(S_{n}(f;g),S_{n}(f^{\prime};g^{\prime}))=n^{k}\cdot d(S_{n}(f);S_% {n}(g),S_{n}(f^{\prime});S_{n}(g^{\prime}))\leq n^{k}\cdot(d(S_{n}(f),S_{n}(f^% {\prime}))+d(S_{n}(g),S_{n}(g^{\prime})))=n^{k}\cdot d(S_{n}(f),S_{n}(f^{% \prime}))+n^{k}\cdot d(S_{n}(g),S_{n}(g^{\prime}))<\varepsilon/2+\varepsilon/2=\varepsilon$ . The proof for parallel composition is analogous. $\hfill\blacktriangleleft$

We can show that the Newton’s cradle equation from before also holds for asymptotic equivalence. We prove this using a method similar to the diagonal method. As a consequence, asymptotic equivalence is preserved under application of the $\star$ -iteration operation $\tau^{\star}$ .

Lemma 19 (Newton’s cradle, reprised).

For any $f\colon S\to Z,g\colon Z\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes Z,% h\colon S\otimes\mathbf{A}\cdot 1\to\mathbf{B}\cdot 1\otimes S$ , if $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_a}\end{matrix}% \equiv\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_b}\end{matrix}$ then $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_c}\end{matrix}% \equiv\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/Newton_S_d}\end{matrix}$ .

Proof.

Let $k\in{\mathbb{N}}$ , and take $S^{\prime}=S_{k}(S)$ , $Z^{\prime}=S_{k}(Z)$ , $\mathbf{C}=S_{k}(\mathbf{A})$ , $\mathbf{D}=S_{k}(\mathbf{B})$ , $f_{k}=S_{k}(f)$ , $g_{k}=S_{k}(g)$ , and $h_{k}=S_{k}(h)$ . We shall define $a\in[0,1]$ as:
$\;\;a:=d\left(\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_I_a}% \end{matrix}\;,\;\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_I_% b}\end{matrix}\right)$ and prove that $d\left(\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_I_c}\end{% matrix}\;,\;\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_I_d}% \end{matrix}\right)\leq ka$

We prove this, by showing by induction on $r\in{\mathbb{N}}$ that: $\;\;\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_P_a}\end{matrix% }\equiv_{ra}\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_P_b}% \end{matrix}\;\;$

Induction basis:: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_IB_a}\end{matrix}% \stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale% ={0.1}]{pics/S5/Newton_IB_b}\end{matrix}\stackrel{{\scriptstyle(\text{def})}}{% {=}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_IB_c}\end{matrix}$
Induction step:: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_IS_a}\end{matrix}% \stackrel{{\scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale% ={0.1}]{pics/S5/Newton_IS_b}\end{matrix}\stackrel{{\scriptstyle}}{{\equiv_{a}}% }\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/Newton_IS_c}\end{matrix}$

$\stackrel{{\scriptstyle(\text{hypothesis})}}{{\equiv_{ra}}}\begin{matrix}% \includegraphics[scale={0.1}]{pics/S5/Newton_IS_d}\end{matrix}\stackrel{{% \scriptstyle(\text{def})}}{{=}}\begin{matrix}\includegraphics[scale={0.1}]{% pics/S5/Newton_IS_e}\end{matrix}$

together getting an upper bound for the distance of $a+ra=(r+1)a$ , as required.

Taking $r=k$ , we get a distance of $k a$ between the two sides of the equation. Hence, given any $b\in{\mathbb{N}}$ we get
$\lim_{k\to\infty}k^{b}d\left(\begin{matrix}\includegraphics[scale={0.1}]{pics/% S5/Newton_I_c}\end{matrix},\begin{matrix}\includegraphics[scale={0.1}]{pics/S5% /Newton_I_d}\end{matrix}\right)=\lim_{k\to\infty}k^{b+1}d\left(\begin{matrix}% \includegraphics[scale={0.1}]{pics/S5/Newton_I_a}\end{matrix},\begin{matrix}% \includegraphics[scale={0.1}]{pics/S5/Newton_I_b}\end{matrix}\right)=0$

$\hfill\blacktriangleleft$

5.1 Examples

Asymptotic equivalence is used to reason whether it is possible to increase the security parameter to significantly minimize the risk of two programs being distinguished. This allows us to formally ignore undesirable situations if their probability of occurring is asymptotically insignificant, or in other words: negligible. Our first example shows that a randomly generated key of length $\sigma$ is unlikely to be any specific key. This has three useful consequences:

1.

Two randomly generated keys of length $\sigma$ are not equal (asymptotically).
2.

If an adversary attempts to guess a key before that key is generated (or without any knowledge of the generated key), then this guess is wrong (asymptotically).
3.

We can uniformly generate an element of $\mathbb{Z}_{2^{\sigma}-1}$ (asymptotically),

We first define $\textsf{all-1}:\mathbb{B}^{\star}\to\mathbb{B}$ which checks if all elements of $\mathbb{B}^{\star}$ are equal to $1$ . Given an and-gate $\textsf{\&}:\mathbb{B}^{2}\to\mathbb{B}$ , we define $\textsf{all-1}:=(\langle 1\rangle\otimes id_{\mathbb{B}^{\star}});\tau^{\star}% _{\mathbb{B},(\mathbb{B}),()}(\textsf{\&})$ .

Lemma 20.

If $p<1$ , then $\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_a}\end{matrix}% \equiv\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_b}\end{matrix}$ .

Proof.

By induction on $k$ , we can prove that the two diagrams as seen through $S_{k}$ in the Lemma statement are at most $p^{k}$ apart in the underlying metric-enriched category (to cover an edge-case we use $0^{0}=1$ ). Given that $p<1$ , we have that for any $a$ , $\lim_{k\to\infty}k^{a}\cdot p^{k}=0$ . First, observe that by (3) and (3), $\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_c}\end{matrix}$ .

For $k=0$ , the required distance $\equiv_{1}$ is trivially true, i.e. $\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_IB_a}\end{matrix}% \equiv_{1}\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_IB_b}% \end{matrix}$ .

For $k^{\prime}=k+1$ , we do the following steps.

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_IS_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_IS_b}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/zero_IS_c}\end{matrix}% \equiv_{p\cdot p^{k}+(1-p)\cdot 0}\begin{matrix}\includegraphics[scale={0.1}]{% pics/S5/ex/zero_IS_d}\end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{% pics/S5/ex/zero_IS_e}\end{matrix}$

$\hfill\blacktriangleleft$

In other words, no randomly generated key with weighted choice below 1 consists of only ones. Note in particular that this is the case even if the key is used in some other context. We define equality on bits using a negated xor gate $(=):\mathbb{B}^{2}\to\mathbb{B}$ . Then equality on $\star$ -tuples $(=)^{\star}:\mathbb{B}^{\star}\otimes\mathbb{B}^{\star}\to\mathbb{B}$ is done by iterating the equality and checking that all entries are one.

Lemma 21.

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_a}\end{matrix}% \equiv\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_b}\end{matrix}$ .

Proof.

First, we merge the two iterations into one using (3) and (3). Then we can reorder $\langle 1/2\rangle$ and $(=)$ operations in such a way that they still give the same probabilistic stochastic map. Thirdly, we can separate the iteration into two iterations, and apply Lemma 20 to the first iteration. Lastly, merge the two remaining iterations again and note that equality to a random bit gives a random bit (similar to what we observed with xor before).

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_P_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_P_b}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_P_c}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_P_d}\end{matrix}% \equiv\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_P_e}\end{% matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/guess_P_f}\end{matrix}$

$\hfill\blacktriangleleft$

We consider one final example, the iterated von Neumann’s trick. This is a method for simulating a fair coin flip using a biased coin that lands on heads with probability $p\in(0,1)$ . The method involves flipping the biased coin twice and selecting the first outcome if both flips match; otherwise, the process is repeated. When a form of parametric iteration is available, the trick can be formalised as Example 11 in [24]. Here we give a categorical and diagrammatic representation as the diagram in the lemma.

Lemma 22.

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/Von_a}\end{matrix}% \equiv\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/Von_b}\end{matrix}$ .

Proof.

The equation above states that the process of flipping a bit with probability $p$ a total of $k$ -times converges to a fair coin flip as $k$ increases. We prove this by showing that for a constant number $k$ of iterations, the two diagrams are $(2p-1)^{k}$ away if $p\geq 1/2$ , and $(1-2p)^{k}$ away if $p\leq 1/2$ . In both cases, the distance approaches zero exponentially.

We shall look at the case in which $p\geq 1/2$ , the other case goes similarly. We prove the result by induction on $k$ , as follows. The base case holds since everything is $1$ away from everything else, which satisfies the condition. For the inductive step, let $k^{\prime}=k+1$ and observe that the following holds true, where we take $q=2p-1$ and $h=q^{k}$ the distance from the induction hypothesis. We write $n:\mathbb{B}\to\mathbb{B}$ for the not gate, then:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_b}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_c}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_d}\end{matrix}$

$=\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_e}\end{matrix}% \stackrel{{\scriptstyle\text{induction hypothesis}}}{{\equiv_{q\cdot q^{k}+(1-% q)\cdot 0}}}\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_f}% \end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S5/ex/von_P_g}% \end{matrix}$

$\hfill\blacktriangleleft$

6 Conclusions and Future Work

This work is a step towards an algebraic approach to cryptographic proofs completely parametric in security parameters. Such proofs normally entail showing that all protocols have polynomial time complexity with respect to the parameters, and require intricate probabilistic calculations. Binding the parameter helps avoid unsound proof pitfalls, such as accidentally using asymptotic rewriting while performing induction over number of iterations.

In order to incorporate further cryptographic protocols however, we need two further extensions. First, we need to allow for cryptographic primitives, which should be given as families of operations in $\mathcal{C}$ indexed over the security parameter, with accompanying assumptions regarding distances. This should be possible by extending $\mathcal{C}$ accordingly, and deriving further equations once one takes the parametric iteration over $\mathcal{C}$ .

The second extension entails dealing with operations like pseudorandom number generators, as e.g. used in stream ciphers. In the current framework, we cannot generate more randomness from less. Concretely, we theoretically cannot have a morphism $f:\mathbb{B}^{\star}\to\mathbb{B}^{\star}\otimes\mathbb{B}$ such that $\tau^{\star}(\langle\frac{1}{2}\rangle);f\equiv\tau^{\star}(\langle\frac{1}{2}% \rangle)\otimes\langle\frac{1}{2}\rangle$ . The solution to this problem is to define a coarser relation, that of contextual equivalence relative to contexts of morphisms which can only investigate a finite amount of data, meaning whose input and output are constant (from $\mathcal{C}$ ). Our notion of asymptotic equivalence is (trivially) sound with respect to this notion of contextual equivalence, though further investigation of this relation is for future research.

On the topic of probabilistic computations, we use the fact that all our computations are total, which is reflected in the naturality property of our if-gate operation. Extending to partial probabilistic computations, we should generalize to partial Markov categories with a condition/equality operation. Our if-gate as well as the discard operation will only be natural over all total computations (those not involving conditioning). In order to more accurately model an if-statement as might be used in a programming language, we should either introduce a more structured functorial if operation, or move towards distributive monoidal categories and their associated languages of tape/sheet diagrams [1, 7].

References

[1] Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape Diagrams for Monoidal Monads. In Corina Cîrstea and Alexander Knapp, editors, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025), volume 342 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:24, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CALCO.2025.11.
[2] Anne Broadbent and Martti Karvonen. Categorical composable cryptography: extended version. Logical Methods in Computer Science, Volume 19, Issue 4, December 2023. doi:10.46298/lmcs-19(4:30)2023.
[3] Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proceedings 42nd IEEE Symposium on Foundations of Computer Science, pages 136–145. IEEE, 2001. doi:10.1109/SFCS.2001.959888.
[4] Titouan Carette, Dominic Horsman, and Simon Perdrix. Szx-calculus: Scalable graphical quantum reasoning. In MFCS 2019-44th International Symposium on Mathematical Foundations of Computer Science, volume 138, pages 55–1, 2019.
[5] Apiwat Chantawibul and Pawel Sobocinski. Monoidal multiplexing. In B. Fischer and T. Uustalu, editors, Theoretical Aspects of Computing ? ICTAC 2018, volume 11187, pages 116–131. Springer, October 2018. doi:10.1007/978-3-030-02508-3_7.
[6] Bob Coecke, Tobias Fritz, and Robert W Spekkens. A mathematical theory of resources. Information and Computation, 250:59–86, 2016. doi:10.1016/J.IC.2016.02.008.
[7] Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories. arXiv preprint arXiv:2010.13361, 2020.
[8] Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.4.
[9] Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal streams for dataflow programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533365.
[10] Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020. arXiv:1908.07021.
[11] Steven Holtzen, Guy Van den Broeck, and Todd Millstein. Scaling exact inference for discrete probabilistic programs. Proceedings of the ACM on Programming Languages, 4(OOPSLA):1–31, 2020. doi:10.1145/3428208.
[12] Nicholas Gauguin Houghton-Larsen. A mathematical framework for causally structured dilations and its relation to quantum self-testing. arXiv preprint arXiv:2103.02302, 2021. arXiv:2103.02302.
[13] André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55–112, July 1991. doi:10.1016/0001-8708(91)90003-P.
[14] Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptography, Second Edition. Chapman & Hall/CRC, 2nd edition, 2014.
[15] A.N. Kolmogorov and S.V. Fomin. Introductory Real Analysis. Selected Russian publications in the mathematical sciences. Prentice-Hall, 1970. URL: https://books.google.nl/books?id=9l4PAQAAMAAJ.
[16] Ugo Dal Lago, Zeinab Galal, and Giulia Giusti. On computational indistinguishability and logical relations. In Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings, pages 241–263, Berlin, Heidelberg, 2024. Springer-Verlag. doi:10.1007/978-981-97-8943-6_12.
[17] Gabriele Lobbia, Wojciech Różowski, Ralph Sarkis, and Fabio Zanasi. Quantitative Monoidal Algebra: Axiomatising Distance with String Diagrams. In Paweł Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak, editors, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025), volume 345 of Leibniz International Proceedings in Informatics (LIPIcs), pages 68:1–68:21, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.MFCS.2025.68.
[18] Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1998.
[19] Ueli Maurer. Constructive cryptography–a new paradigm for security definitions and proofs. In Joint Workshop on Theory of Security and Applications, pages 33–56. Springer, 2011. doi:10.1007/978-3-642-27375-9_3.
[20] Ueli Maurer and Renato Renner. Abstract cryptography. In Bernard Chazelle, editor, Innovations in Computer Science - ICS 2011, Tsinghua University, Beijing, China, January 7-9, 2011. Proceedings, pages 1–21. Tsinghua University Press, 2011. URL: http://conference.iiis.tsinghua.edu.cn/ICS2011/content/papers/14.html.
[21] Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, and Fabio Zanasi. A complete axiomatisation of equivalence for discrete probabilistic programming. In Programming Languages and Systems: 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part II, pages 202–229, Berlin, Heidelberg, 2025. Springer-Verlag. doi:10.1007/978-3-031-91121-7_9.
[22] Robin Piedeleu and Fabio Zanasi. An Introduction to String Diagrams for Computer Scientists. Elements in Applied Category Theory. Cambridge University Press, 2025.
[23] P. Selinger. A Survey of Graphical Languages for Monoidal Categories, volume 813 of Lecture Notes in Physics, pages 289–355. Springer, Berlin, Heidelberg, 2010. doi:10.1007/978-3-642-12821-9_4.
[24] Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi. On iteration in discrete probabilistic programming. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), volume 299 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.FSCD.2024.20.

Appendix A Appendix to Section 3

Extended proof of Lemma 4.

We prove each property using the diagonalisation method, instantiating the top level iterations by $k$ . We prove the relevant equation by induction on $k$ . The base case is relatively simple. We prove the induction steps below, unfolding once, then using the induction hypothesis, and finishing with an optional refolding.

Induction step for (3):: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_id_P_a}\end{matrix}% =\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_id_P_b}\end{matrix% }=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_id_P_c}\end{% matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_id_P_d}\end% {matrix}$
Induction step for (3):: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_swap_P_a}\end{% matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_swap_P_b}% \end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_swap_P% _c}\end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_% swap_P_d}\end{matrix}$

Induction step for (3) is proved in Section 3.

Induction step for (3):: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_mono_P_a}\end{% matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_mono_P_b}% \end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_mono_P% _c}\end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/star_% mono_P_d}\end{matrix}=\begin{matrix}\includegraphics[scale={0.1}]{pics/S3/A/% star_mono_P_e}\end{matrix}$

$\hfill\blacktriangleleft$

Appendix B A Complete Equational Theory of Boolean Stochastic Maps

The structure of Markov categories with probabilistic choice, introduced in Section 4, is novel. Thus, it is interesting to study whether the axioms are complete with respect to the category $\mathsf{FinStoch}_{\{1,0\}}$ . Here, completeness means that any equality between Boolean stochastic maps in $\mathsf{FinStoch}_{\{1,0\}}$ can also be derived syntactically using the axioms listed in Figure 1.

In order to formally state completeness, we introduce the syntactic category $\mathsf{PBCirc}$ of probabilistic boolean circuits. This is the symmetric monoidal category of string diagrams freely generated by the single-sorted signature $(\mathbb{B},\Sigma)$ , where $\Sigma:=\{\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/discardB}\end{% matrix},\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/copyB}\end{% matrix},\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phiB}\end{matrix% },\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/p}\end{matrix}\}$ and such that the morphisms are quotiented by the axioms in Figure 1.

Diagrams in $\mathsf{PBCirc}$ take semantics in $\mathsf{FinStoch}_{\{1,0\}}$ via the interpretation functor $\llbracket-\rrbracket\colon$ ${\mathsf{PBCirc}\to\mathsf{FinStoch}_{\{1,0\}}}$ , defined inductively as follows:

\llbracket\mathbb{B}\rrbracket:=\{1,0\}\quad\llbracket\begin{matrix}% \includegraphics[scale={0.1}]{pics/S4/A/discardB}\end{matrix}\rrbracket:=!_{\{% 1,0\}}\quad\llbracket\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/% copyB}\end{matrix}\rrbracket:=\blacktriangleleft_{\{1,0\}}\quad\llbracket% \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phiB}\end{matrix}% \rrbracket:=\phi_{\{1,0\}}\quad\llbracket\begin{matrix}\includegraphics[scale=% {0.1}]{pics/S4/A/p}\end{matrix}\rrbracket:=\langle p\rangle

Then we say that the equational theory of $\mathsf{PBCirc}$ is complete for $\mathsf{FinStoch}_{\{1,0\}}$ if, for any two diagrams $c,d\in\mathsf{PBCirc}$ of the same type, if $\llbracket c\rrbracket=\llbracket d\rrbracket$ then their equality can be derived using the axioms in Figure 1. We rephrase Theorem 11.

Theorem 23.

The equational theory of $\mathsf{PBCirc}$ is complete for $\mathsf{FinStoch}_{\{1,0\}}$ .

Proof.

The proof shows that each element of $\mathsf{FinStoch}_{\{1,0\}}$ has a unique normal form representation as a diagram in $\mathsf{PBCirc}$ , and each diagram in $\mathsf{PBCirc}$ is provably equal to a diagram in normal form.

We first equip each set $\mathbb{B}^{n}$ with a linear order. We then say that a formal sum $p_{1}\cdot x_{1}+\dots+p_{m}\cdot x_{m}$ over $\mathbb{B}^{n}$ is in normal form if all $p_{i}>0$ and the list $x_{1},\dots,x_{m}$ forms a sorted list of elements without repetition. As such, a formal sum in normal form is either of the form $1\cdot x$ , or $p\cdot x+(1-p)\cdot s$ with $p\in(0,1)$ , and $s$ a formal sum in normal form, containing values $x^{\prime}$ all higher than $x$ according to the chosen order. Importantly, each distribution has a unique normal formal sum representation.

A weighted probabilistic tree over $\mathbb{B}^{n}$ is a diagram $I\to\mathbb{B}^{n}$ inductively defined as:

t,r\quad:=\quad\langle b_{1}\rangle\otimes\dots\otimes\langle b_{n}\rangle\mid% (t\otimes r);\phi^{p}_{\mathbb{B}^{n}}

where each $b_{i}\in\{0,1\}$ . We represent a normal formal sum as a weighted probabilistic tree, by representing $1\cdot(b_{1},\dots,b_{n})$ as $\langle b_{1}\rangle\otimes\dots\otimes\langle b_{n}\rangle$ , and $p\cdot(b_{1},\dots,b_{n})+(1-p)\cdot s$ as $(\langle b_{1}\rangle\otimes\dots\otimes\langle b_{n}\rangle\otimes t);\phi^{p% }_{\mathbb{B}^{n}}$ , where $t$ is the representation of the normal formal sum $s$ . It can be shown that any weighted probabilistic tree over $\mathbb{B}^{n}$ is equal to the tree representation of a normal formal sum. This is done by using axioms (1), (1) and (1) to get rid of zero-probability branches, sorting the order, and re-associating branches, as well as determinism of $\langle 1\rangle$ , $\langle 0\rangle$ combined with (1) to combine branches with the same result.

The normal forms of type $\mathbb{B}^{0}\to\mathbb{B}^{n}$ are the tree representations of normal formal sums, which are unique for each distribution. We generalize to arbitrary $\mathbb{B}^{k}\to\mathbb{B}^{n}$ by doing a case distinction on inputs, where a normal form of type $\mathbb{B}^{k+1}\to\mathbb{B}^{n}$ is of the form: $(\blacktriangleleft_{\mathbb{B}^{k}}\otimes\textit{id}_{\mathbb{B}});(\textit{% id}_{\mathbb{B}^{k}}\otimes\chi_{\mathbb{B}^{k},\mathbb{B}});(f_{1}\otimes% \textit{id}_{\mathbb{B}}\otimes f_{0});\phi_{\mathbb{B}^{n}}$ , where $f_{1}$ and $f_{0}$ are normal forms of morphisms of type $\mathbb{B}^{k}\to\mathbb{B}^{n}$ . Each morphism $f:\mathbb{B}^{k}\multimap\mathbb{B}^{n}$ of $\mathsf{FinStoch}_{\{1,0\}}$ has a unique normal form of this kind, with $f:\mathbb{B}^{0}\to\mathbb{B}^{n}$ represented by the tree representation of the normal formal sum for the distribution given by $f(*)$ , and $f:\mathbb{B}^{k+1}\to\mathbb{B}^{n}$ represented by taking $f_{1}$ and $f_{0}$ to be the normal form of the functions $(b_{1},\dots,b_{k})\mapsto f(b_{1},\dots,b_{k},1)$ and $(b_{1},\dots,b_{k})\mapsto f(b_{1},\dots,b_{k},0)$ respectively. This normal form is unique, as this specification is necessitated by the $\llbracket-\rrbracket$ functor.

See below examples of normal forms, with a normal form of a morphism of type $\mathbb{B}^{0}\to\mathbb{B}^{3}$ on the left in the form of a sorted weighted tree (using lexicographic ordering on $\mathbb{B}^{3}$ ), and a normal form of a morphism of type $\mathbb{B}^{3}\to\mathbb{B}^{k}$ with a weighted tree at each $t$ (some liberties were taken regarding the order of swaps and copies).

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/normal_tree}\end{matrix}$ $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/normal_case}\end{matrix}$

We prove that each diagram is equivalent to one in normal form.

$\blacksquare$

First we show that the identity diagrams $\textit{id}_{\mathbb{B}^{n}}:\mathbb{B}^{n}\to\mathbb{B}^{n}$ can be put in normal form. This can be shown by using the equations (1) and (1) together with monoidal coherence and naturality of $\phi$ , given in equations (1), (1), and (1).
$\blacksquare$
Second, note that each morphism in a freely generated monoidal category can be described as a composition of morphisms of the form $(\textit{id}_{A}\otimes s\otimes\textit{id}_{B})$ , with $s$ a generator, which in our case is of $\{\chi\}\cup\Sigma=\{\chi,\blacktriangleleft,!,\langle p\rangle,\phi\}$ . Then show that $f;(\textit{id}_{A}\otimes s\otimes\textit{id}_{B})$ can be reduced to a normal form, given that $f$ is in normal form. This is done in three steps:
1. 1.
  
  Pull $(\textit{id}_{A}\otimes s\otimes\textit{id}_{B})$ through each $\phi$ using naturality (1), both the if-gates used to distinguish between different inputs, as well as the if-gates used in the weighted probabilistic trees, until we get to leaves of the trees.
2. 2.
  
  Reduce each $(\langle b_{1}\rangle\otimes\dots\otimes\langle b_{n}\rangle);(\textit{id}_{A}% \otimes s\otimes\textit{id}_{B})$ to a weighted probabilistic tree.
3. 3.
  
  The result is $f$ , but with different weighted probabilistic trees at each case in its case distinction. Put all those trees into normal form.

Hence we can normalize each $f:\mathbb{B}^{k}\to\mathbb{B}^{n}$ by first giving it a specification as composition of $(\textit{id}_{A}\otimes s\otimes\textit{id}_{B})$ morphisms. Then normalize the identity function on $\mathbb{B}^{k}$ and inductively normalize by composing with each additional layer. $\hfill\blacktriangleleft$

Lemma 24.

$\mathsf{PBCirc}$ is a metric enriched symmetric monoidal category.

Proof of Lemma 24.

We take as distance between arrows

d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}(c,d):=d_{\{1,0\}^{n}\to\{1,0\}^{m}}(% \llbracket c\rrbracket,\llbracket d\rrbracket)

for every $c,d\colon\mathbb{B}^{n}\to\mathbb{B}^{m}$ in $\mathsf{PBCirc}$ .

First, we verify that $d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}$ is indeed a distance – that is, it satisfies the conditions in (2). Most properties are straightforward to check; the only non-trivial one is $d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}(c,d)=0\iff c=d$ , which we prove below:

$\displaystyle d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}(c,d)=0$	$\displaystyle\iff d_{\{1,0\}^{n}\to\{1,0\}^{m}}(\llbracket c\rrbracket,% \llbracket d\rrbracket)=0$	(Definition of $d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}$ )
	$\displaystyle\iff\llbracket c\rrbracket=\llbracket d\rrbracket$	(Lemma 15)
	$\displaystyle\iff c=d$	(Theorem 11)

To conclude that $\mathsf{PBCirc}$ is metric enriched, we need to verify also that ; and $\otimes$ are non-expansive, that is (3) and (4). We prove (3) below, the proof for the other is analogous.

$\displaystyle d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}(c;d,c^{\prime};d^{\prime})$	$\displaystyle=d_{\{1,0\}^{n}\to\{1,0\}^{m}}(\llbracket c;d\rrbracket,% \llbracket c^{\prime};d^{\prime}\rrbracket)$	(Definition of $d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}$ )
	$\displaystyle=d_{\{1,0\}^{n}\to\{1,0\}^{m}}(\llbracket c\rrbracket;\llbracket d% \rrbracket,\llbracket c^{\prime}\rrbracket;\llbracket d^{\prime}\rrbracket)$	( $\llbracket-\rrbracket$ is a functor)
	$\displaystyle\leq d_{\{1,0\}^{n}\to\{1,0\}^{l}}(\llbracket c\rrbracket,% \llbracket c^{\prime}\rrbracket)+d_{\{1,0\}^{l}\to\{1,0\}^{m}}(\llbracket d% \rrbracket,\llbracket d^{\prime}\rrbracket)$	((3))
	$\displaystyle=d_{\mathbb{B}^{n}\to\mathbb{B}^{l}}(c,c^{\prime})+d_{\mathbb{B}^% {l}\to\mathbb{B}^{m}}(d,d^{\prime})$	(Definition of $d_{\mathbb{B}^{n}\to\mathbb{B}^{m}}$ )

$\hfill\blacktriangleleft$

Appendix C Additional Proofs for Section 4

Proof of Lemma 10.

(2) is proven by using (1) and (1).

Now to prove (2): $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/If_lemma}\end{matrix}$

First we apply axiom (1), (1), and (1) to each of the incoming wires, and combining those with monoidal coherence (1). Then we pull the main morphism through the $\phi$ -gate using naturality. As a third step, we use determinism of $1$ and $0$ , as well as (1) and (2). Lastly, we use naturality of the discard operation to get the right result.

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/If_lemma_proof}\end{matrix}$

Lastly, proving (2): $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/Split_Lemma}\end{matrix}$

For simplicity, we define: $\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/Split_Lemma_Help}\end{matrix}$ , and swap the first two wires of (2). We then prove as follows, starting with the equations (1), (1), and (1), then use (1), and finally simplifying using equations (1) and (2):

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/Split_Lemma_Proof}\end{matrix}$ $\hfill\blacktriangleleft$

Extended proof of Lemma 12.

We define copy, discard and if-gate on objects as done in Section 4. We then show that in $\mathcal{C}$ , $\tau^{k}_{1,(A),(A,A)}(\blacktriangleleft_{A})=\blacktriangleleft_{A^{k}}$ , $\tau^{k}_{1,(A),()}(!_{A})=!_{A^{k}}$ , and

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phik_a}\end{matrix}=% \begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phik_b}\end{matrix}$

Consequently, by induction on $A$ in $\textsf{PI}(\mathcal{C})$ , we then reason that with the chosen definition, $S_{k}(\blacktriangleleft_{A})=\blacktriangleleft_{S_{k}(A)}$ , $S_{k}(!_{A})=!_{S_{k}(A)}$ , and $S_{k}(\phi_{A})=\phi_{S_{k}(A)}$ . This allows us to lift the equations for Markov categories and probabilistic choice to $\textsf{PI}(\mathcal{C})$ via $S_{k}$ .

We prove the relevant property for $\phi$ stated above by induction on $k$ . The induction basis is simple. The induction step goes as follows:

$\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phik_P_a}\end{matrix}\!=% \!\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phik_P_b}\end{matrix}% \!=\!\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phik_P_c}\end{% matrix}\!=\!\begin{matrix}\includegraphics[scale={0.1}]{pics/S4/A/phik_P_d}% \end{matrix}$

Using the above property, we can show by induction on objects $A$ that $S_{k}(\phi_{A})=\phi_{S_{k}(A)}$ . This allows us to prove the relevant equations by lifting them from $\mathcal{C}$ . $\hfill\blacktriangleleft$

Proof of Lemma 16.

For soundness we proceed by induction on the rules in (5). Observe that the laws which do not involve the probabilistic choice are trivially verified from the fact that $\mathsf{FinStoch}_{\{1,0\}}$ is metric-enriched.

For the top rightmost rule, given maps $c,c^{\prime}\colon\{1,0\}^{n}\to\{1,0\}^{m}$ and $d,d^{\prime}\colon\{1,0\}^{l}\to\{1,0\}^{m}$ such that $c\equiv_{\delta}c^{\prime}$ and $d\equiv_{\delta}d^{\prime}$ , by inductive hypothesis we have that $d_{\{1,0\}^{n}\to\{1,0\}^{m}}(c,c^{\prime})\leq\delta$ and $d_{\{1,0\}^{l}\to\{1,0\}^{m}}(d,d^{\prime})\leq\delta$ . Now let $h=(c\otimes\textit{id}_{\mathbb{B}}\otimes d);\phi_{\{1,0\}^{m}}$ and $h^{\prime}=(c^{\prime}\otimes\textit{id}_{\mathbb{B}}\otimes d^{\prime});\phi_% {\{1,0\}^{m}}$ and observe that for any $a\in\{1,0\}^{n},b\in\{1,0\}^{l}$ , we have the following cases:

\begin{array}[]{cc}h(a,0,b)={(c\otimes!_{\{1,0\}^{l}})}(a,b)=c(a)&h^{\prime}(a% ,0,b)={(c^{\prime}\otimes!_{\{1,0\}^{l}})}(a,b)=c^{\prime}(a)\\ h(a,1,b)={(!_{\{1,0\}^{n}}\otimes d)}(a,b)=d(b)&h^{\prime}(a,1,b)={(!_{\{1,0\}% ^{n}}\otimes d^{\prime})}(a,b)=d^{\prime}(b)\end{array}

Thus, $d_{\{1,0\}^{m}}(h(a,0,b),h^{\prime}(a,0,b))=d_{\{1,0\}^{m}}(c(a),c^{\prime}(a)% )\leq\delta$ and $d_{\{1,0\}^{m}}({h}(a,1,b),{h^{\prime}}(a,1,b))$ $=d_{\{1,0\}^{m}}(d(b),d^{\prime}(b))\leq\delta$ .

To conclude we have that

	$\displaystyle d_{\{1,0\}^{n+1+l}\to\{1,0\}^{m}}(h,h^{\prime})$	$\displaystyle=\texttt{max}_{(a,i,b)\in\{1,0\}^{n+i+l}}\mathsf{tv}_{\{1,0\}^{m}% }({h}(a,i,b),{h^{\prime}}(a,i,b))$
		$\displaystyle\leq\texttt{max}_{(a,i,b)\in\{1,0\}^{n+i+l}}\delta=\delta.$

For the bottom rightmost rule, given maps $c,c^{\prime}\colon\{1,0\}^{n}\to\{1,0\}^{m}$ and $d,d^{\prime}\colon\{1,0\}^{l}\to\{1,0\}^{m}$ such that $c\equiv_{\delta}c^{\prime}$ and $d\equiv_{\delta^{\prime}}d^{\prime}$ , by inductive hypothesis: $d_{\{1,0\}^{n}\to\{1,0\}^{m}}(c,c^{\prime})\leq\delta$ and $d_{\{1,0\}^{l}\to\{1,0\}^{m}}(d,d^{\prime})\leq\gamma$ . Now let $h=(c\otimes d);\phi^{p}_{\{1,0\}^{m}}$ and $h^{\prime}=(c^{\prime}\otimes d^{\prime});\phi^{p}_{\{1,0\}^{m}}$ and observe that for any $a\in\{1,0\}^{n},b\in\{1,0\}^{l}$ , we have that

\begin{array}[]{cc}{h}(a,b)=p\cdot{c}(a)+(1-p)\cdot{d}(b)&{h^{\prime}}(a,b)=p% \cdot{c^{\prime}}(a)+(1-p)\cdot{d^{\prime}}(b)\end{array}

and thus,

		$\displaystyle d_{\{1,0\}^{n+l}\to\{1,0\}^{m}}(h,h^{\prime})=\texttt{max}_{(a,b% )\in\{1,0\}^{n+l}}\mathsf{tv}_{\{1,0\}^{m}}({h}(a,b),{h^{\prime}}(a,b))$
	$\displaystyle=$	$\displaystyle\,\texttt{max}_{(a,b)\in\{1,0\}^{n+l}}\sum_{x}\frac{\|{h}(a,b)(x)-% {h^{\prime}}(a,b)(x)\|}{2}$
	$\displaystyle=$	$\displaystyle\,\texttt{max}_{(a,b)\in\{1,0\}^{n+l}}\sum_{x}\frac{\|p\cdot({c}(a% )(x)-{c^{\prime}}(a)(x))+(1-p)\cdot({d}(b)(x)-{d^{\prime}}(b)(x))\|}{2}$
	$\displaystyle\leq$	$\displaystyle\,p\cdot\texttt{max}_{a\in\{1,0\}^{n}}\sum_{x}\frac{\|{c}(a)(x)-{c% ^{\prime}}(a)(x)\|}{2}+(1-p)\cdot\texttt{max}_{b\in\{1,0\}^{l}}\sum_{x}\frac{\|{% d}(b)(x)-{d^{\prime}}(b)(x)\|}{2}$
	$\displaystyle=$	$\displaystyle\,p\cdot d_{\{1,0\}^{n}\to\{1,0\}^{m}}({c},{c^{\prime}})+(1-p)% \cdot d_{\{1,0\}^{l}\to\{1,0\}^{m}}({d},{d^{\prime}})\leq p\cdot\delta+(1-p)% \cdot\gamma.$

For completeness, we rely on the normal form Theorem 11 and use the rules from (5). For morphisms $f,g\colon n\to m$ in normal form, we prove $f\equiv_{d(f,g)}g$ by induction on $n$ and $m$ .

$\blacksquare$

Base case: $n=m=0$ , then both morphisms are $\textit{id}_{I}$ . So $f\equiv_{0}g$ and $d(f,g)=0$ .
$\blacksquare$

Suppose $n=0$ and $m=m^{\prime}+1$ . Then $f=(\langle 1\rangle\otimes f_{1}\otimes\langle 0\rangle\otimes f_{0});\phi^{p}$ and $g=(\langle 1\rangle\otimes g_{1}\otimes\langle 0\rangle\otimes g_{0});\phi^{q}$ . Now, $d(f,g)=\min(p,q)\cdot d(f_{1},g_{1})+\min(1-p,1-q)\cdot d(f_{0},g_{0})+(1-\min% (p,q)-\min(1-p,1-q))$ , since $d(\langle i\rangle\otimes f_{i},\langle i\rangle\otimes g_{i})=d(f_{i},g_{i})$ , and $d(\langle i\rangle\otimes f_{i},\langle 1-i\rangle\otimes g_{i-1})=1$ .

Assume w.l.o.g. that $p\leq q$ , so $\min(p,q)=p$ and $\min(1-p,1-q)=1-q$ , and $d(f,g)=p\cdot d(f_{1},g_{1})+(1-q)\cdot d(f_{0},g_{0})+(q-p)$ . Define $k=\frac{q-p}{1-p}$ . We can then prove that $f=(\langle 0\rangle\otimes f_{0}\otimes\langle 0\rangle\otimes f_{0});(\langle 1% \rangle\otimes f_{1}\otimes\phi^{k});\phi^{p}$ using (1), (2), and $g=(\langle 1\rangle\otimes g_{1}\otimes\langle 0\rangle\otimes g_{0});(\langle 1% \rangle\otimes g_{1}\otimes\phi^{k});\phi^{p}$ using the same rules and (1). By induction hypothesis, $\langle 1\rangle\otimes f_{1}\equiv_{d(f_{1},g_{1})}\langle 1\rangle\otimes g_% {1}$ and $\langle 0\rangle\otimes f_{0}\equiv_{d(f_{0},g_{0})}\langle 0\rangle\otimes g_% {0}$ , and trivially $\langle 0\rangle\otimes f_{0}\equiv_{1}\langle 1\rangle\otimes g_{1}$ . Applying the second quantitative $\phi$ -rule twice, we get that $f\equiv_{\alpha}g$ for: $\alpha=p\cdot d(f_{1},g_{1})+(1-p)\cdot(k\cdot 1+(1-k)\cdot d(f_{0},g_{0}))=p% \cdot d(f_{1},g_{1})+(p-q)+(1-q)\cdot d(f_{0},g_{0})$ .

\blacksquare

Suppose $n=k+1$ . Then $f=(\blacktriangleleft_{\mathbb{B}^{k}}\otimes\textit{id}_{\mathbb{B}});(% \textit{id}_{\mathbb{B}^{k}}\otimes\chi_{\mathbb{B},\mathbb{B}^{k}});(f_{1}% \otimes\textit{id}_{\mathbb{B}}\otimes f_{0});\phi_{\mathbb{B}^{m}}$ and $g=(\blacktriangleleft_{\mathbb{B}^{k}}\otimes\textit{id}_{\mathbb{B}});(% \textit{id}_{\mathbb{B}^{k}}\otimes\chi_{\mathbb{B},\mathbb{B}^{k}});(g_{1}% \otimes\textit{id}_{\mathbb{B}}\otimes g_{0});\phi_{\mathbb{B}^{m}}$ . Note that

	$\displaystyle d(f,g)$	$\displaystyle=\texttt{max}_{(x,i)\in\{1,0\}^{n}}(d(f(x,i),g(x,i)))=\texttt{max% }_{(x,i)\in\{1,0\}^{n}}(d(f_{i}(x),g_{i}(x)))$
		$\displaystyle=\texttt{max}(\texttt{max}_{x\in\{1,0\}^{k}}(d(f_{1}(x),g_{1}(x))% ),\texttt{max}_{x\in\{1,0\}^{k}}(d(f_{0}(x),g_{0}(x))))$
		$\displaystyle=\texttt{max}(d(f_{1},g_{1}),d(f_{0},g_{0})).$

By induction hypothesis, $f_{1}\equiv_{d(f_{1},g_{1})}g_{1}$ and $f_{0}\equiv_{d(f_{0},g_{0})}g_{0}$ . So since $d(f_{i},g_{i})\leq d(f,g)$ as proven above, $f_{1}\equiv_{d(f,g)}g_{1}$ and $f_{0}\equiv_{d(f,g)}g_{0}$ . Applying the first quantitative $\phi$ -rule, we get: $(f_{1}\otimes\textit{id}_{\mathbb{B}}\otimes f_{0});\phi_{\mathbb{B}^{k}}% \equiv_{d(f,g)}(g_{1}\otimes\textit{id}_{\mathbb{B}}\otimes g_{0});\phi_{% \mathbb{B}^{k}}$ , so with compositionality, $f\equiv_{d(f,g)}g$ as required.

$\hfill\blacktriangleleft$

[bib.bib1] [1] Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape Diagrams for Monoidal Monads. In Corina Cîrstea and Alexander Knapp, editors, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025), volume 342 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:24, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CALCO.2025.11.

[bib.bib2] [2] Anne Broadbent and Martti Karvonen. Categorical composable cryptography: extended version. Logical Methods in Computer Science, Volume 19, Issue 4, December 2023. doi:10.46298/lmcs-19(4:30)2023.

[bib.bib3] [3] Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proceedings 42nd IEEE Symposium on Foundations of Computer Science, pages 136–145. IEEE, 2001. doi:10.1109/SFCS.2001.959888.

[bib.bib4] [4] Titouan Carette, Dominic Horsman, and Simon Perdrix. Szx-calculus: Scalable graphical quantum reasoning. In MFCS 2019-44th International Symposium on Mathematical Foundations of Computer Science, volume 138, pages 55–1, 2019.

[bib.bib5] [5] Apiwat Chantawibul and Pawel Sobocinski. Monoidal multiplexing. In B. Fischer and T. Uustalu, editors, Theoretical Aspects of Computing ? ICTAC 2018, volume 11187, pages 116–131. Springer, October 2018. doi:10.1007/978-3-030-02508-3_7.

[bib.bib6] [6] Bob Coecke, Tobias Fritz, and Robert W Spekkens. A mathematical theory of resources. Information and Computation, 250:59–86, 2016. doi:10.1016/J.IC.2016.02.008.

[bib.bib7] [7] Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories. arXiv preprint arXiv:2010.13361, 2020.

[bib.bib8] [8] Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.4.

[bib.bib9] [9] Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal streams for dataflow programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, New York, NY, USA, 2022. Association for Computing Machinery. doi:10.1145/3531130.3533365.

[bib.bib10] [10] Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020. arXiv:1908.07021.

[bib.bib11] [11] Steven Holtzen, Guy Van den Broeck, and Todd Millstein. Scaling exact inference for discrete probabilistic programs. Proceedings of the ACM on Programming Languages, 4(OOPSLA):1–31, 2020. doi:10.1145/3428208.

[bib.bib12] [12] Nicholas Gauguin Houghton-Larsen. A mathematical framework for causally structured dilations and its relation to quantum self-testing. arXiv preprint arXiv:2103.02302, 2021. arXiv:2103.02302.

[bib.bib13] [13] André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55–112, July 1991. doi:10.1016/0001-8708(91)90003-P.

[bib.bib14] [14] Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptography, Second Edition. Chapman & Hall/CRC, 2nd edition, 2014.

[bib.bib15] [15] A.N. Kolmogorov and S.V. Fomin. Introductory Real Analysis. Selected Russian publications in the mathematical sciences. Prentice-Hall, 1970. URL: https://books.google.nl/books?id=9l4PAQAAMAAJ.

[bib.bib16] [16] Ugo Dal Lago, Zeinab Galal, and Giulia Giusti. On computational indistinguishability and logical relations. In Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings, pages 241–263, Berlin, Heidelberg, 2024. Springer-Verlag. doi:10.1007/978-981-97-8943-6_12.

[bib.bib17] [17] Gabriele Lobbia, Wojciech Różowski, Ralph Sarkis, and Fabio Zanasi. Quantitative Monoidal Algebra: Axiomatising Distance with String Diagrams. In Paweł Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak, editors, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025), volume 345 of Leibniz International Proceedings in Informatics (LIPIcs), pages 68:1–68:21, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.MFCS.2025.68.

[bib.bib18] [18] Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1998.

[bib.bib19] [19] Ueli Maurer. Constructive cryptography–a new paradigm for security definitions and proofs. In Joint Workshop on Theory of Security and Applications, pages 33–56. Springer, 2011. doi:10.1007/978-3-642-27375-9_3.

[bib.bib20] [20] Ueli Maurer and Renato Renner. Abstract cryptography. In Bernard Chazelle, editor, Innovations in Computer Science - ICS 2011, Tsinghua University, Beijing, China, January 7-9, 2011. Proceedings, pages 1–21. Tsinghua University Press, 2011. URL: http://conference.iiis.tsinghua.edu.cn/ICS2011/content/papers/14.html.

[bib.bib21] [21] Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, and Fabio Zanasi. A complete axiomatisation of equivalence for discrete probabilistic programming. In Programming Languages and Systems: 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part II, pages 202–229, Berlin, Heidelberg, 2025. Springer-Verlag. doi:10.1007/978-3-031-91121-7_9.

[bib.bib22] [22] Robin Piedeleu and Fabio Zanasi. An Introduction to String Diagrams for Computer Scientists. Elements in Applied Category Theory. Cambridge University Press, 2025.

[bib.bib23] [23] P. Selinger. A Survey of Graphical Languages for Monoidal Categories, volume 813 of Lecture Notes in Physics, pages 289–355. Springer, Berlin, Heidelberg, 2010. doi:10.1007/978-3-642-12821-9_4.

[bib.bib24] [24] Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi. On iteration in discrete probabilistic programming. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), volume 299 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.FSCD.2024.20.