Department of Computer Science, University College London, United Kingdom and
https://wkrozowski.github.iow.rozowski@cs.ucl.ac.ukhttps://orcid.org/0000-0002-8241-7277
Wojciech Różowski <ccs2012> <concept>
<concept_id>10003752.10003766.10003776</concept_id> <concept_desc>Theory of
computation Regular languages</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Regular languages This work was partially supported
by ERC grant Autoprobe (grant agreement 101002697).

###### Acknowledgements.

The author wishes to thank Giorgio Bacci, Leo Lobski, Alexandra Silva and
Mateo Torres-Ruiz for discussions and feedback, as well as anonymous reviewers
for their comments.Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola
Svensson 4 51st International Colloquium on Automata, Languages, and
Programming (ICALP 2024) ICALP 2024 ICALP 2024 July 8–12, 2024 Tallinn,
Estonia 297 137

# A Complete Quantitative Axiomatisation of Behavioural Distance of Regular
Expressions

Wojciech Różowski

###### Abstract

Deterministic automata have been traditionally studied through the point of
view of language equivalence, but another perspective is given by the
canonical notion of _shortest-distinguishing-word_ distance quantifying the of
states. Intuitively, the longer the word needed to observe a difference
between two states, then the closer their behaviour is. In this paper, we give
a sound and complete axiomatisation of _shortest-distinguishing-word_ distance
between regular languages. Our axiomatisation relies on a recently developed
quantitative analogue of equational logic, allowing to manipulate rational-
indexed judgements of the form $e\equiv_{\varepsilon}f$ meaning _term $e$ is
approximately equivalent to term $f$ within the error margin of
$\varepsilon$_. The technical core of the paper is dedicated to the
completeness argument that draws techniques from order theory and Banach
spaces to simplify the calculation of the behavioural distance to the point it
can be then mimicked by axiomatic reasoning.

###### keywords:

Regular Expressions, Behavioural Distances, Quantitative Equational Theories

###### category:

##  1 Introduction

Transition systems have been widely employed to model computational phenomena.
In theoretical computer science, it is customary to model computations as
transition systems and subsequently reason about their equivalence or
similarity. Classical examples include checking language equivalence of
deterministic finite automata using Hopcroft and Karp’s algorithm [18] or
constructing bisimulations between labelled transition systems [25].
Throughout the years, especially in the concurrency theory community,
researchers have studied a plethora of different notions of behavioural
equivalences and preorders one could impose on a transition system [40].
However, in many practical applications, especially when dealing with
probabilistic or quantitative transition systems, asking about such classical
notions of equivalence (or similarity) could be too strict, and it might be
more reasonable to ask quantitative questions about how far apart the
behaviour of the two states is.

A growing line of work on _behavioural distances_ [37, 5, 38, 39, 13] answers
this problem by equipping state-spaces of transition systems with
(pseudo)metric structures quantifying the dissimilarity of states. In such a
setting, states at distance zero are not necessarily the same, but rather
equivalent with respect to some classical notion of behavioural equivalence.
In a nutshell, equipping transition systems with such a notion of distance
crucially relies on the possibility of _lifting_ the distance between the
states to the distance on the observable behaviour of the transition system.
Behavioural distances were originally studied in the context of probabilistic
transition systems [16, 38], where observable behaviour is in the form of
probability distribution among possible transitions. In such a case, the
necessary lifting of distances between states to distances between probability
distributions of possible outcomes relies on the famous
Kantorovich/Wasserstein liftings, studied traditionally in transportation
theory [41]. In general, transition systems can be viewed more abstractly
through a well-established category-theoretic framework of coalgebras for an
endofunctor [27]. Recent work [5] generalised the Kantorovich/Wassertstein
lifting to lifting endofunctors (modelling one-step behaviour of transition
systems) from the category of sets and functions to the category of
(pseudo)metric spaces and nonexpansive functions, thus allowing equipping a
multitude of different kinds of transition systems with a sensible notion of
behavioural distance.

Traditionally, besides looking at behavioural equivalence/similarity purely
from the algorithmic point of view, one can look at those problems
axiomatically, by describing behaviours of transition systems as expressions
and by providing formal systems based on (in)equational logic for reasoning
about equivalence/similarity of the transition systems described by the
expressions. Classic examples include reasoning about language equivalence of
Kleene’s regular expressions representing deterministic finite automata using
inference systems of Salomaa [29] or Kozen [19], or reasoning about
bisimilarity of finite-state labelled transition systems through Milner’s
calculus of finite-state behaviours [24].

In this paper, we are interested in a similar axiomatic point of view, but in
the case of behavioural distances. Unfortunately, the classical (in)equational
logic cannot be applied here, as it has no way of talking about approximate
equivalence. Instead, we rely on the quantitative analogue of equational logic
[22], which deals with the statements of the form $e\equiv_{\varepsilon}f$,
intuitively meaning _term $e$ is within the distance of at most
$\varepsilon\in\mathbb{Q}^{+}$ from the term $f$_. While the existing work [4,
2, 1] looked at quantitative axiomatisations of behavioural distance for
probabilistic transition systems calculated through the
Kantorovich/Wasserstein lifting, which can be thought of as a special case of
the abstract coalgebraic framework relying on lifting endofunctors to the
category of pseudometric spaces, the notions of behavioural distance for other
kinds of transition systems have not been axiomatised before. It turns out
that the approach to completeness used in [2] relies on properties which are
not unique to distances obtained through the Kantorovich/Wasserstein lifting
and can be employed to give complete axiomatisations of behavioural distances
for other kinds of transition systems obtained through the coalgebraic
framework [5]. In this paper, as a starting point, we look at one of the
simplest instantiations of that abstract framework in the case of
deterministic automata, yielding _shortest-distinguishing-word_ distance. To
illustrate that notion of distance, consider the following three deterministic
finite automata:

$\mathbf{q_{0}}$starta$\mathbf{r_{0}}$start$\mathbf{r_{1}}$$\mathbf{r_{2}}$aaa$\mathbf{s_{0}}$starta

Neither of the above automata are language equivalent. Their languages are
respectively (from the left) $\\{\epsilon,a,aa,aaa,\dots\\}$,
$\\{\epsilon,a\\}$ and $\emptyset$. However, one could argue that the
behaviour of the middle automaton is closer to the one on the left rather than
the one on the right. In particular, languages of the left and middle
automaton agree on all of the words of length less than two, while the left
and right one disagree on all words. One can make this idea precise, by
providing $1$-bounded metric
$d_{\mathcal{L}}:\mathcal{P}(A^{*})\times\mathcal{P}(A^{*})\to[0,1]$ on the
set of all formal languages over some fixed alphabet $A$ given by the
following formula, where $\lambda\in]0,1[$ and $L,M\subseteq A^{*}$:

$d_{\mathcal{L}}(L,M)=\begin{cases}\lambda^{|w|}&w\text{ is the shortest word
that belongs to only one of }L\text{ and }M\\\ 0&\text{if }L=M\end{cases}$ (1)

If we set $\lambda=\frac{1}{2}$, then
$d_{\mathcal{L}}(\\{\epsilon,a,aa,aaa,\dots\\},\\{\epsilon,a\\})=\frac{1}{4}$
and $d_{\mathcal{L}}(\\{\epsilon,a,aa,aaa,\dots\\},\emptyset)=1$, which allows
to formally state that the behaviour of the middle automaton is a better
approximation of the left one, rather than the right one. Observe, that we
excluded $\lambda=0$ and $\lambda=1$, as in both cases $d_{\mathcal{L}}$ would
become a pseudometric setting all languages to be at distance zero or one.
Automata in the example above correspond to the regular expressions $a^{*}$,
$a+1$ and $0$ respectively. In order to determine the distance between
arbitrary regular expressions $e$ and $f$ one would have to construct
corresponding deterministic finite automata and calculate (or approximate) the
distance between their languages. Instead, as a main contribution of this
paper, we present a sound and complete quantitative inference system for
reasoning about the shortest-distinguishing-word distance of languages denoted
by regular expressions in question. Formally speaking, if
$\llbracket-\rrbracket:\mathsf{Exp}\to\mathcal{P}(A^{*})$ is a function taking
regular expressions to their languages, then our inference system satisfies
the following:

$\vdash e\equiv_{\varepsilon}f\iff d_{\mathcal{L}}(\llbracket
e\rrbracket,\llbracket f\rrbracket)\leq\varepsilon$

Although much of our development is grounded in category theory and coalgebra,
we spell out all the definitions and results concretely, without the need for
specialised language. We organise the paper as follows:

  * •

In Section 2 we review basic definitions from automata theory and recall the
semantics of regular expressions through Brzozowski derivatives [10]. Then, in
order to talk about distances, we state basic definitions and properties
surrounding (pseudo)metric spaces.

  * •

In Section 3 we instantiate the framework of coalgebraic behavioural metrics
[5] to the concrete case of deterministic automata. We recall the abstract
results from [5] in simple automata-theoretic terms.

  * •

In Section 4 we start by recalling the definitions surrounding the
quantitative equational theories [22] from the literature. We then present the
axioms of our inference system for the shortest-distinguishing-word distance
of regular expressions, give soundness result and provide a discussion about
the axioms. The interesting insight is that when relying on quantitative
equational theories which contain an infinitary rule capturing the notion of
convergence, there is no need for any fixpoint introduction rule. We
illustrate this by axiomatically deriving Salomaa’s fixpoint rule for regular
expressions [29].

  * •

The key result of our paper is contained in Section 5, where we prove
completeness of our inference system. The heart of the argument relies on
showing that the behavioural distance of regular expressions can be
approximated from above using Kleene’s fixpoint theorem, which can be then
mimicked through the means of axiomatic reasoning. This part of the paper
makes heavy use of the order-theoretic and Banach space structures carried by
the sets of pseudometrics over a given set.

  * •

We conclude in Section 6, review related literature, and sketch directions for
future work.

##  2 Preliminaries

We start by recalling basic definitions surrounding deterministic automata,
regular expressions and (pseudo)metric spaces from the literature.

### Deterministic automata.

A deterministic automaton $\mathcal{M}$ with inputs in a finite alphabet $A$
is a pair $(M,\langle o_{M},t_{M}\rangle)$ consisting of a set of states $M$
and a pair of functions $\langle o_{M},t_{M}\rangle$, where
$o_{M}:M\to\\{0,1\\}$ is the _output_ function which determines whether a
state $m$ is final ($o_{M}(m)=1$) or not ($o_{M}(m)=0$), and $t:M\to M^{A}$ is
the _transition_ function, which, given an input letter $a$ determines the
next state. If the set $M$ of states is finite, then we call an automaton
$\mathcal{M}$ a deterministic finite automaton (DFA). We will frequently write
$m_{a}$ to denote $t_{M}(m)(a)$ and refer to $m_{a}$ as the derivative of $m$
for the input $a$. Definition of derivatives can be inductively extended to
words $w\in A^{\ast}$, by setting $m_{\varepsilon}=m$ and
$m_{aw^{\prime}}=(m_{a})_{w^{\prime}}$. Note that our definition of
deterministic automaton slightly differs from the most common one in the
literature, by not explicitly including the initial state. Instead of talking
about the language of the automaton, we will talk about the languages of
particular states of the automaton. Given a state $m\in M$, we write
$L_{\mathcal{M}}(m)\subseteq{A^{\ast}}$ for its language, which is formally
defined by $L_{\mathcal{M}}(m)=\\{w\in A^{\ast}\mid o(m_{w})=1\\}$. Given two
deterministic automata $(M,\langle o_{M},t_{M}\rangle)$ and $(N,\langle
o_{N},t_{N}\rangle)$, a function $h:M\to N$ is a homomorphism if it preserves
outputs and input derivatives, that is $o_{N}(h(m))=o_{M}(m)$ and
$h(m)_{a}=h(m_{a})$. The set of all languages $\mathcal{P}(A^{\ast})$ over an
alphabet $A$ can be made into a deterministic automaton
$(\mathcal{P}(A^{\ast}),\langle o_{L},t_{L}\rangle)$, where for
$l\in\mathcal{P}(A^{\ast})$ the output function is given by
$o_{L}(l)=[\epsilon\in l]$ and for all $a\in A$ the input derivative is
defined to be $l_{a}=\\{w\mid aw\in l\\}$. This automaton is _final_ , that is
for any other automaton $\mathcal{M}=(M,\langle o_{M},t_{M}\rangle)$ there
exists a unique homomorphism from $M$ to $\mathcal{P}(A^{\ast})$, which is
precisely given by the map $L_{\mathcal{M}}:M\to\mathcal{P}(A^{\ast})$ taking
each state $m\in S$ to its language. Given a set of states
$M^{\prime}\subseteq M$, we write $\langle
M^{\prime}\rangle_{{\mathcal{M}}}\subseteq M$ for the smallest set of states
reachable from $M^{\prime}$ through the transition function of the automaton
$\mathcal{M}$. Clearly, $(\langle M^{\prime}\rangle_{{\mathcal{M}}},\langle
o_{M},t_{M}\rangle)$ is a deterministic automaton. We will abuse the notation
and write $\langle M^{\prime}\rangle_{{\mathcal{M}}}$ for $(\langle
M^{\prime}\rangle_{{\mathcal{M}}},\langle o_{M},t_{M}\rangle)$. The canonical
inclusion map $\iota:\langle M^{\prime}\rangle_{{\mathcal{M}}}\hookrightarrow
M$ given by $\iota(m)=m$ for all $m\in\langle
M^{\prime}\rangle_{{\mathcal{M}}}$ is a homomorphism from $\langle
M^{\prime}\rangle_{{\mathcal{M}}}$ to $\mathcal{M}$. In the case of singleton
and two-element sets of states, we will simplify the notation and write
$\langle m\rangle_{{\mathcal{M}}}$ and $\langle
m,m^{\prime}\rangle_{{\mathcal{M}}}$.

### Regular expressions.

We let $e,f$ range over _regular expressions over $A$_ generated by the
following grammar:

$e,f\in\mathsf{Exp}::=0\mid 1\mid a\in A\mid e+f\mid e\mathbin{;}f\mid
e^{\ast}$

The standard interpretation of regular expressions
$\llbracket-\rrbracket:\mathsf{Exp}\to\mathcal{P}(A^{\ast})$ is inductively
defined by the following:

$\llbracket 0\rrbracket=\emptyset\quad\llbracket
1\rrbracket=\\{\epsilon\\}\quad\llbracket a\rrbracket=\\{a\\}\quad\llbracket
e+f\rrbracket=\llbracket e\rrbracket\cup\llbracket f\rrbracket\quad\llbracket
e\mathbin{;}f\rrbracket=\llbracket e\rrbracket\diamond\llbracket
f\rrbracket\quad\llbracket e^{\ast}\rrbracket=\llbracket e\rrbracket^{\ast}$

We write $\epsilon$ for the empty word. Given $L,M\subseteq A^{\ast}$, we
define $L\diamond M=\\{lm\mid l\in L,m\in M\\}$, where mere juxtaposition
denotes concatenation of words. $L^{\ast}$ denotes the _asterate_ of the
language $L$ defined as $L^{\ast}=\bigcup_{i\in\mathbb{N}}L^{i}$ with
$L^{0}=\\{\epsilon\\}$ and $L^{n+1}=L\diamond L^{n}$.

### Brzozowski derivatives.

The famous Kleene’s theorem states that the formal languages accepted by DFA
are in one-to-one correspondence with formal languages definable by regular
expressions. One direction of this theorem involves constructing a DFA for an
arbitrary regular expression. The most common way is via Thompson
construction, $\epsilon$-transition removal and determinisation. Instead, we
recall a direct construction due to Brzozowski [10], in which the set
$\mathsf{Exp}$ of regular expressions is equipped with a structure of
deterministic automaton $\mathcal{R}=(\mathsf{Exp},\langle
o_{\mathcal{R}},t_{\mathcal{R}}\rangle)$ through so-called Brzozowski
derivatives [10]. The output derivative
$o_{\mathcal{R}}:\mathsf{Exp}\to\\{0,1\\}$ is defined inductively by the
following for $a\in A$ and $e,f\in\mathsf{Exp}$:

$\displaystyle o_{\mathcal{R}}(0)=0\quad o_{\mathcal{R}}(1)=1\quad
o_{\mathcal{R}}(a)=0$ $\displaystyle
o_{\mathcal{R}}(e+f)=o_{\mathcal{R}}(e)\vee o_{\mathcal{R}}(f)\quad
o_{\mathcal{R}}(e\mathbin{;}f)=o_{\mathcal{R}}(e)\wedge
o_{\mathcal{R}}(f)\quad o_{\mathcal{R}}(e^{\ast})=1$

Similarly, the transition derivative $t_{\mathcal{R}}\in\mathsf{Exp}\to
A\to\mathsf{Exp}$ denoted $t_{\mathcal{R}}(e)(a)=(e)_{a}$ is defined by the
following:

$\displaystyle(0)_{a}=0\quad(1)_{a}=0\quad(a^{\prime})_{a}=\begin{cases}1&a=a^{\prime}\\\
0&a\neq a^{\prime}\end{cases}$
$\displaystyle(e+f)_{a}=(e)_{a}+(f)_{a}\quad(e\mathbin{;}f)_{a}=(e_{a})\mathbin{;}f+o_{\mathcal{R}}(e)\mathbin{;}f\quad(e^{\ast})=(e)_{a}\mathbin{;}e^{\ast}$

The canonical language-assigning homomorphism from $\mathcal{R}$ to
$\mathcal{L}$, happens to coincide with the semantics map
$\llbracket-\rrbracket$ assigning a language to each regular expression.

######  Lemma 2.1 ([32, Theorem 3.1.4]).

For all $e\in\mathsf{Exp}$, $\llbracket e\rrbracket=L_{\mathcal{R}}(e)$

Instead of looking at infinite-state automaton defined on the state-space of
all regular expressions, we can restrict ourselves to the subautomaton
$\langle e\rangle_{{\mathcal{R}}}$ of $\mathcal{R}$ while obtaining the
semantics of $e$.

######  Lemma 2.2.

For all $e\in\mathsf{Exp}$, $\llbracket e\rrbracket=L_{\langle
e\rangle_{{\mathcal{R}}}}(e)$

Unfortunately, for an arbitrary regular expression $e\in\mathsf{Exp}$, the
automaton $\langle e\rangle_{{\mathcal{R}}}$ is not guaranteed to have a
finite set of states. However, simplifying the transition derivatives by
removing duplicates in the expressions in the form $e_{1}+\dots+e_{n}$,
guarantees a finite number of reachable states from any expression. Formally
speaking, let
${{\mathrel{\dot{\equiv}}}}\subseteq{\mathsf{Exp}\times\mathsf{Exp}}$ be the
least congruence relation closed under ${{(e+f)+g}{\leavevmode\nobreak\
{\mathrel{\dot{\equiv}}}\leavevmode\nobreak\ }{e+(f+g)}}$ (Associativity),
${e+f}{\leavevmode\nobreak\ {\mathrel{\dot{\equiv}}}\leavevmode\nobreak\
}{f+e}$ (Commutativity) and ${e}{\leavevmode\nobreak\
{\mathrel{\dot{\equiv}}}\leavevmode\nobreak\ }{e+e}$ (Idempotence) for all
$e,f,g\in\mathsf{Exp}$. We will write
${{\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}}$ for the quotient of
$\mathsf{Exp}$ by the relation ${\mathrel{\dot{\equiv}}}$ and
$[-]_{{\mathrel{\dot{\equiv}}}}:\mathsf{Exp}\to{\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}$
for the canonical map taking each expression $e\in\mathsf{Exp}$ into its
equivalence class $[e]_{{\mathrel{\dot{\equiv}}}}$ modulo
${\mathrel{\dot{\equiv}}}$. Because of [27, Proposition 5.8],
${\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}$ can be equipped with a structure
of deterministic automaton
$\mathcal{Q}=({\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}},\langle
o_{\mathcal{Q}},t_{\mathcal{Q}}\rangle)$, where for all $e\in\mathsf{Exp},a\in
A$, $o_{\mathcal{Q}}([e]_{{\mathrel{\dot{\equiv}}}})=o_{\mathcal{R}}(e)$ and
$([e]_{{\mathrel{\dot{\equiv}}}})_{a}=[e_{a}]_{{\mathrel{\dot{\equiv}}}}$,
which makes the quotient map
$[-]_{{\mathrel{\dot{\equiv}}}}:\mathsf{Exp}\to{\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}$
into an automaton homomorphism from the Brzozowski automaton $\mathcal{R}$
into $\mathcal{Q}$. This automaton enjoys the following property:

######  Lemma 2.3 ([10, Theorem 4.3]).

For any $e\in\mathsf{Exp}$, the set $\langle
e\rangle_{{\mathcal{Q}}}\subseteq{\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}$ is
finite.

Through an identical line of reasoning as before (Lemma 2.2), we can show
that:

######  Lemma 2.4.

For all $e\in\mathsf{Exp}$,
$L_{\langle[e]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}}([e]_{{\mathrel{\dot{\equiv}}}})=\llbracket
e\rrbracket$

### (Pseudo)metric spaces.

Let $\top\in\left]0,\infty\right]$ be a fixed maximal element. A
$\top$-bounded _pseudometric_ on a set $X$ (equivalently $\top$-_pseudometric_
or even just a _pseudometric_ if $\top$ is clear from the context) is a
function $d:X\times X\to[0,\top]$ satisfying $d(x,x)=0$ (_reflexivity_),
$d(x,y)=d(y,x)$ (_symmetry_) and $d(x,z)\leq d(x,y)+d(y,z)$ (_triangle
inequality_) for all $x,y,z\in X$. If additionally $d(x,y)=0$ implies $x=y$,
$d$ is called a $\top$-_metric_. A _(pseudo)metric_ space is a pair $(X,d)$
where $X$ is a set and $d$ is a (pseudo)metric on $X$. Given pseudometric
spaces $(X,d_{X})$ and $(Y,d_{Y})$, we call a map $f:X\to Y$ _nonexpansive_ ,
if for all $x,x^{\prime}\in X$, $d_{Y}(f(x),f(x^{\prime}))\leq
d_{X}(x,x^{\prime})$ and an _isometry_ if
$d_{Y}(f(x),f(x^{\prime}))=d_{X}(x,x^{\prime})$. A simple example of a
pseudometric is the discrete metric which can be defined on any set $X$ as
$d_{X}(x,x)=0$ for all $x\in X$ and $d(x,y)_{X}=\top$ for $x,y\in X$ such that
$x\neq y$. The set $D_{X}$ of (pseudo)metrics over some fixed set $X$ can be
equipped with a partial order structure given by the pointwise order, i.e.
$d\sqsubseteq d^{\prime}\iff\forall x,x^{\prime}\in X.d(x,y)\leq
d^{\prime}(x,y)$.

######  Lemma 2.5 ([5, Lemma 3.2]).

$(D_{X},\sqsubseteq)$ is a complete lattice. The join of an arbitrary set of
pseudometrics $D\subseteq D_{X}$ is taken pointwise, ie. $\left(\sup
D\right)(x,y)=\sup\\{d(x,y)\mid d\in D\\}$ for $x,y\in X$. The meet of $D$ is
defined to be $\inf D=\sup\\{d\mid d\in D_{X},\forall{d^{\prime}\in
D},d\sqsubseteq d^{\prime}\\}$.

Crucially for our completeness proof, if we are dealing with descending
chains, that is sequences $\\{d_{i}\\}_{i\in\mathbb{N}}$, such that
$d_{i}\sqsupseteq d_{i+1}$ for all $i\in\mathbb{N}$, then we can also
calculate infima in the pointwise way111Lemma 2.6 is one of the intermediate
results used in the proof of [2, Lemma 5.6] that was communicated to us by the
authors of [2]. As this result was excluded in the mentioned paper, we
incorporated it along with its proof for the sake of completeness. .

######  Lemma 2.6.

Let $\\{d_{i}\\}_{i\in\mathbb{N}}$ be an infinite descending chain in the
lattice $(D_{X},\sqsubseteq)$ of pseudometrics over some fixed set $X$. Then
$(\inf\\{d_{i}\mid i\in\mathbb{N}\\})(x,y)=\inf\\{d_{i}(x,y)\mid
i\in\mathbb{N}\\}$ for any $x,y\in X$.

######  Proof 2.7.

It suffices to argue that $d(x,y)=\inf\\{d_{i}(x,y)\mid i\in\mathbb{N}\\}$ is
a pseudometric. For reflexivity, observe that $d(x,x)=\inf\\{d_{i}(x,x)\mid
i\in\mathbb{N}\\}=\inf\\{0\\}=0$ for all $x\in X$. For symmetry, we have that
$d(x,y)=\inf\\{d_{i}(x,y)\mid i\in\mathbb{N}\\}=\inf\\{d_{i}(y,x)\mid
i\in\mathbb{N}\\}=d(y,x)$ for any $x,y\in X$. The only difficult case is
triangle inequality. First, let $i,j\in\mathbb{N}$ and define $k=\min(i,j)$.
Since $d_{k}\sqsubseteq d_{i}$ and $d_{k}\sqsubseteq d_{j}$, we have that
$d_{k}(x,y)+d_{k}(y,z)\leq d_{i}(x,y)+d_{j}(y,z)$. Therefore
$\inf\\{d_{l}(x,y)+d_{l}(y,z)\mid l\in\mathbb{N}\\}$ is a lower bound of
$d_{i}(x,y)+d_{j}(y,z)$ for any $i,j\in\mathbb{N}$ and hence it is below the
greatest lower bound, that is $\inf\\{d_{l}(x,y)+d_{l}(y,z)\mid
l\in\mathbb{N}\\}\leq\inf\\{d_{i}(x,y)+d_{j}(y,z)\mid i,j\in\mathbb{N}\\}$. We
can use that property to show the following $d(x,y)=\inf\\{d_{i}(z,y)\mid
i\in\mathbb{N}\\}\leq\inf\\{d_{i}(x,y)+d_{i}(y,z)\mid
i\in\mathbb{N}\\}\leq\\{d_{i}(x,y)+d_{j}(y,z)\mid
i,j\in\mathbb{N}\\}=\inf\\{d_{i}(x,y)\mid
i\in\mathbb{N}\\}+\inf\\{d_{j}(y,z)\mid j\in\mathbb{N}\\}=d(x,y)+d(y,z)$,
which completes the proof.

Additionally, the set of pseudometrics can be equipped with a norm. We write
$\overline{\mathbb{R}}=[-\infty,\infty]$ for the set of extended reals. For
any set $X$, the set of functions $\overline{\mathbb{R}}^{X\times X}$, which
is a superset of $D_{X}$, can be seen as a Banach space [26] (complete normed
vector space) by means of the sup-norm $\|d\|=\sup_{x,y\in X}|d(x,y)|$. This
structure will implicitly underly some of the claims used as intermediate
steps in the proof of completeness.

##  3 Behavioural distance

We now instantiate the abstract coalgebraic framework [5] to the case of
deterministic automata relying on the lifting described in [5, Example 5.33].
We concretise the generic results from that paper and spell them in simple
automata-theoretic terms.

### Lifting pseudometrics.

Let $\mathcal{M}=(M,\langle o_{M},t_{M}\rangle)$ be a deterministic automaton.
Its one-step observable behaviour (after applying the output and transition
derivatives) can be seen as pairs of the type $\\{0,1\\}\times M^{A}$, where
the first component determines whether the given state is accepting or not and
the second one gives successor state for each letter from the input alphabet.
Let’s say we have two such observations $\langle o_{1},f_{1}\rangle,\langle
o_{2},f_{2}\rangle\in\\{0,1\\}\times M^{A}$. If we had had some notion of a
distance defined on the state-space of our automaton, or speaking more
formally a $1$-pseudometric $d:M\times M\to[0,1]$, then we can _lift_ this
notion of distance, to a distance on observations, given by the following:

$d_{\\{0,1\\}\times M^{A}}(\langle o_{1},f_{1}\rangle,\langle
o_{2},f_{2}\rangle)=\max\\{d_{2}(o_{1},o_{2}),\lambda\cdot\max_{a\in
A}d(f_{1}(a),f_{2}(a))\\}\qquad\lambda\in\left]0,1\right[$

The definition above involves $d_{2}$, the discrete metric on the set
$\\{0,1\\}$. One can observe that $d_{\\{0,1\\}\times M^{A}}$ is again a
$1$-pseudometric, but this time defined on the set $\\{0,1\\}\times M^{A}$
instead. We now move on to showing how one could use this lifting in order to
equip a state-space of automaton $\mathcal{M}$ with a sensible notion of
behavioural pseudometric.

### Behavioural pseudometric.

If one gave us a $1$-metric $d:M\times M\to[0,1]$ on the state-space of the
automaton, we could use our lifting to produce a new pseudometric
$\Phi_{\mathcal{M}}(d):M\times M\to[0,1]$ on the same set, which would
calculate a distance between an arbitrary pair of states by first applying the
output and transition derivatives to obtain a pair of observations and then by
calculating the distance between them using the aforementioned lifting of
pseudometric $d$ to the pseudometric defined on the set $\\{0,1\\}\times
M^{A}$. Formally speaking, define a map $\Phi_{\mathcal{M}}:D_{M}\to D_{M}$ on
the lattice of $1$-pseudometrics on $M$ given by the following:

$\Phi_{\mathcal{M}}(d)(m,m^{\prime})=\max\\{d_{2}(o_{M}(m),o_{M}(m^{\prime})),\lambda\cdot\max_{a\in
A}d(m_{a},m^{\prime}_{a})\\}\qquad\lambda\in\left]0,1\right[$

The construction above only tells us how to construct new pseudometrics on the
state-space of the automaton out of existing ones, but does not give one to
start with. It turns out, that the map $\Phi_{\mathcal{M}}$ is a monotone
mapping on the lattice of $1$-psuedometrics on the set $M$ [5, Lemma 6.1].
Because of that, one can use the Knaster-Tarski fixpoint theorem [35] and
construct its least fixed point, explicitly given by
$d_{\mathcal{M}}=\inf\\{d\mid d\in D_{M}\wedge\Phi_{\mathcal{M}}(d)\sqsubseteq
d\\}$. Pseudometrics, which are fixpoints of $\Phi_{\mathcal{M}}$ intuitively
interact well with the automaton structure, as they satisfy the property that
the distance between two states is the same as the distance between their
observable behaviour calculated using the lifting. Taking the least such
pseudometric satisfies several desirable properties [5] and thus we will call
$d_{\mathcal{M}}$ a behavioural pseudometric on the automaton $\mathcal{M}$.
First of all, preserving automaton transitions also preserves behavioural
distances.

######  Proposition 3.1.

Let $\mathcal{M}=(M,\langle o_{M},t_{M}\rangle)$ and $\mathcal{N}=(N,\langle
o_{N},t_{N}\rangle)$ be deterministic automata. If $h:M\to N$ is a
homomorphism, then it is also an isometric mapping between pseudometric spaces
$(M,d_{\mathcal{M}})$ and $(N,d_{\mathcal{N}})$.

If we look at the final automaton on the set of all formal languages over a
fixed finite alphabet $A$, then one can easily verify that the behavioural
distance given by the least fixpoint construction precisely corresponds to the
Equation 1 defining the shortest-distinguishing-word distance we stated in
Section 1. In general, states of an arbitrary deterministic automaton
characterised by the behavioural pseudometric to be in distance zero are
language equivalent. When we look at $d_{\mathcal{L}}$ defined on the states
of the final automaton, whose state-space consists of formal languages, then
the language equivalence corresponds to the equality of states. In other words
$d_{\mathcal{L}}$ becomes a metric space.

######  Lemma 3.2.

Let $\mathcal{M}=(M,\langle o_{M},t_{M}\rangle)$ be an arbitrary deterministic
automaton and let $\mathcal{L}=(\mathcal{P}(A^{\ast}),\langle
o_{L},t_{L}\rangle)$ be a deterministic automaton structure on the set of all
languages over an alphabet $A$.

  1. 1.

$(\mathcal{P}(A^{\ast}),d_{\mathcal{L}})$ is a metric space.

  2. 2.

For any $m,m^{\prime}\in M$, $d_{\mathcal{M}}(m,m^{\prime})=0\iff
L_{\mathcal{M}}(m)=L_{\mathcal{M}}(m^{\prime})$.

##  4 Quantitative Axiomatisation

In order to provide a quantitative inference system for reasoning about the
behavioural distance of languages denoted by regular expressions, we first
recall the definition of quantitative equational theories from the existing
literature [22, 2] following the notational conventions from [2]. We then
present our axiomatisation and demonstrate its soundness. The interesting
thing about our axiomatisation is the lack of any fixpoint introduction rule.
We show that in the case of quantitative analogue of equational logic [22]
containing the infinitary rule capturing the notion of convergence, we can use
our axioms to derive Salomaa’s fixpoint rule from his axiomatisation of
language equivalence of regular expressions [29].

### Quantitative equational theories.

Let $\Sigma$ be an algebraic signature (in the sense of universal algebra
[11]) consisting of operation symbols $f_{n}\in\Sigma$ of arity
$n\in\mathbb{N}$. If we write $X$ for the countable set of _metavariables_ ,
then $\mathbb{T}(\Sigma,X)$ denotes a set of freely generated terms over $X$
built from the signature $\Sigma$. As a notational convention, we will use
letters $t,s,u,\ldots\in\mathbb{T}(\Sigma,X)$ to denote terms. By a
_substitution_ we mean a function of the type $\sigma\colon
X\to\mathbb{T}(\Sigma,X)$ allowing to replace metavariables with terms. Each
substitution can be inductively extended to terms in a unique way by setting
$\sigma(f(t_{1},\dots,t_{n}))=f(\sigma(t_{1}),\dots,\sigma(t_{n}))$ for each
operation symbol $f_{n}\in\Sigma$ from the signature. We will write
$\mathcal{S}(\Sigma)$ for the set of all substitutions. Given two terms
$t,s\in\mathbb{T}(\Sigma,X)$ and a nonnegative rational number
$\varepsilon\in\mathbb{Q}^{+}$ denoting the distance between the terms, we
call $t\equiv_{\varepsilon}s$ a _quantitative equation (of type $\Sigma$)_.
Notation-wise, we will write $\mathcal{E}(\Sigma)$ to denote the set of all
quantitative equations (of type $\Sigma$) and we will use the capital Greek
letters $\Gamma,\Theta,\ldots\subseteq\mathcal{E}(\Sigma)$ to denote the
subsets of $\mathcal{E}(\Sigma)$. By a _deducibility relation_ we mean a
binary relation denoted
${\vdash}\subseteq\mathcal{P}({\mathcal{E}(\Sigma)})\times\mathcal{E}(\Sigma)$.
Similarly, to the classical equational logic, we will use the following
notational shorthands $\Gamma\vdash
t\equiv_{\varepsilon}s\iff(\Gamma,t\equiv_{\varepsilon}s)\in{\vdash}$ and
$\vdash t\equiv_{\varepsilon}s\iff\emptyset\vdash t\equiv_{\varepsilon}s$.
Furthermore, following the usual notational conventions, we will write
$\Gamma\vdash\Theta$ as a shorthand for the situation when $\Gamma\vdash
t\equiv_{\varepsilon}s$ holds for all $t\equiv_{\varepsilon}s\in\Theta$. To
call $\vdash$ a _quantitative deduction system (of type $\Sigma$)_ it needs to
satisfy the following rules of inference:

$\displaystyle(\textsf{Refl})\quad$ $\displaystyle\vdash t\equiv_{0}t\,,$
$\displaystyle(\textsf{Symm})\quad$
$\displaystyle\\{t\equiv_{\varepsilon}s\\}\vdash s\equiv_{\varepsilon}t\,,$
$\displaystyle(\textsf{Triang})\quad$
$\displaystyle\\{t\equiv_{\varepsilon}u,u\equiv_{\varepsilon^{\prime}}s\\}\vdash
t\equiv_{\varepsilon+\varepsilon^{\prime}}s\,,$
$\displaystyle(\textsf{Max})\quad$
$\displaystyle\\{t\equiv_{\varepsilon}s\\}\vdash
t\equiv_{\varepsilon+\varepsilon^{\prime}}s\,,\text{ for all
$\varepsilon^{\prime}>0$}\,,$ $\displaystyle(\textsf{Cont})\quad$
$\displaystyle\\{t\equiv_{\varepsilon^{\prime}}s\mid\varepsilon^{\prime}>\varepsilon\\}\vdash
t\equiv_{\varepsilon}s\,,$ $\displaystyle(\textsf{NExp})\quad$
$\displaystyle\\{t_{1}\equiv_{\varepsilon}s_{1},\ldots,t_{n}\equiv_{\varepsilon}s_{n}\\}\vdash
f(t_{1},\dots,t_{n})\equiv_{\varepsilon}f(s_{1},\dots,s_{n})\,,\text{ for all
$f_{n}\in\Sigma$}\,,$ $\displaystyle(\textsf{Subst})\quad$ If $\Gamma\vdash
t\equiv_{\varepsilon}s$, then
$\sigma(\Gamma)\vdash\sigma(t)\equiv_{\varepsilon}\sigma(s)$, for all
$\sigma\in\mathcal{S}(\Sigma)$ $\displaystyle(\textsf{Cut})\quad$
$\displaystyle\text{If $\Gamma\vdash\Theta$ and $\Theta\vdash
t\equiv_{\varepsilon}s$, then $\Gamma\vdash t\equiv_{\varepsilon}s$}\,,$
$\displaystyle(\textsf{Assum})\quad$ $\displaystyle\text{If
$t\equiv_{\varepsilon}s\in\Gamma$, then $\Gamma\vdash
t\equiv_{\varepsilon}s$}\,.$

where $\sigma(\Gamma)=\left\\{\sigma(t)\equiv_{\varepsilon}\sigma(s)\mid
t\equiv_{\varepsilon}s\in\Gamma\right\\}$. Finally, by a _quantitative
equational theory_ we mean a set ${\mathcal{U}}$ of universally quantified
_quantitative inferences_
$\\{t_{1}\equiv_{\varepsilon_{1}}s_{1},\dots,t_{n}\equiv_{\varepsilon_{n}}s_{n}\\}\vdash
t\equiv_{\varepsilon}s\,,$ with _finitely many premises_ , closed under
$\vdash$-derivability.

### Quantitative algebras.

Quantitative equational theories lie on the syntactic part of the picture. On
the semantic side, we have their models called _quantitative algebras_ ,
defined as follows.

######  Definition 4.1 ([22, Definition 3.1]).

A quantitative algebra is a tuple
$\mathcal{A}=(A,\Sigma^{\mathcal{A}},d^{\mathcal{A}})$, such that
$(A,\Sigma^{\mathcal{A}})$ is an algebra for the signature $\Sigma$ and
$(A,d^{\mathcal{A}})$ is an $\infty$-pseudometric such that for all operation
symbols $f_{n}\in\Sigma$, for all $1\leq i\leq n$, $a_{i},b_{i}\in A$,
$d^{\mathcal{A}}(a_{i},b_{i})\leq\varepsilon$ implies
$d^{\mathcal{A}}(f^{\mathcal{A}}(a_{1},\dots,a_{n}),f^{\mathcal{A}}(b_{1},\dots,b_{n}))\leq\varepsilon$.

Consider a quantitative algebra
$\mathcal{A}=(A,\Sigma^{\mathcal{A}},d^{\mathcal{A}})$. Given an assignment
$\iota\colon X\to A$ of meta-variables from $X$ to elements of carrier $A$,
one can inductively extend it to $\Sigma$-terms $t\in\mathbb{T}(\Sigma,X)$ in
a unique way. We will abuse the notation and just write $\iota(t)$ for the
interpretation of the term $t$ in quantitative algebra $\mathcal{A}$. We will
say that $\mathcal{A}$ _satisfies_ the quantitative inference $\Gamma\vdash
t\equiv_{\varepsilon}s$, written
$\Gamma\models_{\mathcal{A}}t\equiv_{\varepsilon}s$, if for any assignment of
the meta-variables $\iota\colon X\to A$ it is the case that for all
$t^{\prime}\equiv_{\varepsilon^{\prime}}s^{\prime}\in\Gamma$ we have that
$d^{\mathcal{A}}(\iota(t^{\prime}),\iota(s^{\prime}))\leq\varepsilon^{\prime}$
implies $d^{\mathcal{A}}(\iota(t),\iota(s))\leq\varepsilon$. Finally, we say
that a quantitative algebra $\mathcal{A}$ _satisfies_ (or is a _model_ of) the
quantitative theory ${\mathcal{U}}$, if whenever $\Gamma\vdash
t\equiv_{\varepsilon}s\in{\mathcal{U}}$, then
$\Gamma\models_{\mathcal{A}}t\equiv_{\varepsilon}s$.

### Quantitative algebra of regular expressions.

From now on, let’s focus on the signature
$\Sigma=\\{0_{0},1_{0},+_{2},\mathbin{;}_{2},{(-)^{\ast}}_{1}\\}\cup\\{a_{0}\mid
a\in A\\}$, where $A$ is a finite alphabet. This signature consists of all
operations of regular expressions. We can easily interpret all those
operations in the set $\mathsf{Exp}$ of all regular expressions, using trivial
interpretation functions eg. $+^{\mathcal{B}}(e,f)=e+f$, which interpret the
operations by simply constructing the appropriate terms. Formally speaking, we
can do this because the set $\mathsf{Exp}$ is the carrier of initial algebra
[11] (free algebra over the empty set of generators) for the signature
$\Sigma$.

To make this algebra into a quantitative algebra, we first equip the set
$\mathsf{Exp}$ with a $\infty$-pseudometric, given by
$d^{\mathcal{B}}(e,f)=d_{\mathcal{L}}(\llbracket e\rrbracket,\llbracket
f\rrbracket)$ for all $e,f\in\mathsf{Exp}$. Recall that $d_{\mathcal{L}}$ used
in the definition above is a behavioural pseudometric on the final
deterministic automaton carried by the set $\mathcal{P}(A^{\ast})$ of all
formal languages over an alphabet $A$. In other words, we define the distance
between arbitrary expressions $e$ and $f$ to be the distance between formal
languages $\llbracket e\rrbracket$ and $\llbracket f\rrbracket$ calculated
through the shortest-distinguishing-word metric. It turns out, that in such a
situation all the interpretation functions of $\Sigma$-algebra structure on
$\mathsf{Exp}$ are non-expansive with respect to to the pseudometric defined
above. In other words, we have that:

######  Lemma 4.2.

$\mathcal{B}=(\mathsf{Exp},\Sigma^{\mathcal{B}},d^{\mathcal{B}})$ is a
quantitative algebra.

### Axiomatisation.

In order to talk about the quantitative algebra $\mathcal{B}$ of the
behavioural distance of regular expressions in an axiomatic way, we introduce
the quantitative equational theory REG (Figure 1).

$\begin{array}[]{ll}&\textbf{Nondeterministic choice}\\\ (\mathsf{SL1})&\vdash e+e\equiv_{0}e\,,\\\ (\mathsf{SL2})&\vdash e+f\equiv_{0}f+e\,,\\\ (\mathsf{SL3})&\vdash(e+f)+g\equiv_{0}e+(f+g)\,,\\\ (\mathsf{SL4})&\vdash e+0\equiv_{0}e\,,\\\ (\mathsf{SL5})&\\{e\equiv_{\varepsilon}g,f\equiv_{\varepsilon^{\prime}}h\\}\\\ &\quad\vdash e+f\equiv_{\max(\varepsilon,\varepsilon^{\prime})}g+h\,,\\\ \\\ \\\ &\textbf{Loops}\\\ (\mathsf{Unroll})&\vdash e^{\ast}\equiv_{0}e\mathbin{;}e^{\ast}+1\,,\\\ (\mathsf{Tight})&\vdash(e+1)^{\ast}\equiv_{0}e^{\ast}\,,\\\\[4.64996pt] \end{array}$ | $\begin{array}[]{ll}&\textbf{Sequential composition}\\\ (\mathsf{1S})&\vdash 1\mathbin{;}e\equiv_{0}e\,,\\\ (\mathsf{S})&\vdash e\mathbin{;}(f\mathbin{;}g)\equiv_{0}(e\mathbin{;}f)\mathbin{;}g\,,\\\ (\mathsf{S1})&\vdash e\mathbin{;}1\equiv_{0}e\,,\\\ (\mathsf{0S})&\vdash 0\mathbin{;}e\equiv_{0}0\,,\\\ (\mathsf{S0})&\vdash e\mathbin{;}0\equiv_{0}0\,,\\\ (\mathsf{D1})&\vdash e\mathbin{;}(f+g)\equiv_{0}e\mathbin{;}f+e\mathbin{;}g\,,\\\ (\mathsf{D2})&\vdash(e+f)\mathbin{;}g\equiv_{0}e\mathbin{;}g+f\mathbin{;}g\,,\\\ \\\ &\textbf{Behavioural pseudometric}\\\ (\textsf{Top})&\vdash e\equiv_{1}f\,,\\\ (\textsf{$\lambda$-Pref})&\\{e\equiv_{\varepsilon}f\\}\vdash a\mathbin{;}e\equiv_{\varepsilon^{\prime}}a\mathbin{;}f\,,\text{for $\varepsilon^{\prime}\geq\lambda\cdot\varepsilon$}\\\\[4.64996pt] \end{array}$
---|---
Figure 1: Axioms of the quantitative equational theory REG for
$e,f,g\in\mathsf{Exp}$ and $a\in A$.

The first group of axioms capture properties of the nondeterministic choice
operator $+$ (SL1-SL5). The first four axioms (SL1-SL4) are the usual laws of
semilattices with bottom element $0$. (SL5) is a quantitative axiom allowing
one to reason about distances between sums of expressions in terms of
distances between expressions being summed. Moreover, (SL1-SL5) are axioms of
so-called _Quantitative Semilattices with zero_ , which have been shown to
axiomatise the Hausdorff metric [22]. The sequencing axioms (1S), (S1), (S)
state that the set $\mathsf{Exp}$ of regular expressions has the structure of
a monoid (with neutral element $1$) with absorbent element $0$ (0S), (S0).
Additionally, (D1-D2) talk about interaction of the nondeterministic choice
operator $+$ with sequential composition. The loop axioms (Unroll) and (Tight)
are directly inherited from Salomaa’s axiomatisation of language equivalence
of regular expressions [29]. (Unroll) axiom associates loops with their
intuitive behaviour of choosing, at each step, between successful termination
and executing the loop body once. (Tight) states that the loop whose body
might instantly terminate, causing the next loop iteration to be executed
immediately is provably equivalent to a different loop, whose body does not
contain immediate termination. The last remaining group are behavioural
pseudometric axioms. (Top) states that any two expressions are at most in
distance one from each other. Finally, ($\lambda$-Pref) captures the fact that
prepending the same letter to arbitrary expressions shrinks the distance
between them by the factor of $\lambda\in]0,1[$ (used in the definition of
$d^{\mathcal{B}}$). This axiom is adapted from the axiomatisation of
discounted probabilistic bisimilarity distance [2].

Through a simple induction on the length of derivation, one can verify that
indeed $\mathcal{B}$ is a model of the quantitative theory REG.

######  Theorem 4.3.

(Soundness) The quantitative algebra
$\mathcal{B}=(\mathsf{Exp},\Sigma^{\mathcal{B}},d^{\mathcal{B}})$ is a model
of the quantitative theory $\mathsf{REG}$. In other words, for any
$e,f\in\mathsf{Exp}$ and $\varepsilon\in\mathbb{Q}^{+}$, if $\Gamma\vdash
e\equiv_{\varepsilon}f\in\mathsf{REG}$, then
$\Gamma\models_{\mathcal{B}}e\equiv_{\varepsilon}f$

######  Proof 4.4.

By the structural induction on the judgement $\Gamma\vdash
e\equiv_{\varepsilon}f\in\mathsf{REG}$. $(\textsf{Subst})$, $(\textsf{Cut})$
and $(\textsf{Assum})$ deduction rules from classical logic hold immediately.
The soundness of $(\textsf{Refl})$, $(\textsf{Symm})$, $(\textsf{Triang})$,
$(\textsf{Cont})$ and $(\textsf{Max})$ follows from the fact that
$d^{\mathcal{B}}$ is a pseudometric. $(\textsf{NExp})$ follows from the fact
that interpretations of symbols from the algebraic signature are nonexpansive
(Lemma 4.2). Recall that
$d^{\mathcal{B}}=d_{\mathcal{L}}\circ(\llbracket-\rrbracket\times\llbracket-\rrbracket)$.
The soundness of $(\textsf{Top})$ follows from the fact that $d_{\mathcal{L}}$
is a 1-pseudometric. Additionally, for all axioms in the form $\vdash
e\equiv_{0}f$ it suffices to show that $\llbracket e\rrbracket=\llbracket
f\rrbracket$. $(\mathsf{SL1})$, $(\mathsf{SL2})$, $(\mathsf{SL3})$,
$(\mathsf{SL4})$, $(\mathsf{1S})$, $(\mathsf{S})$, $(\mathsf{S1})$,
$(\mathsf{0S})$, $(\mathsf{S0})$, $(\mathsf{D1})$, $(\mathsf{D2})$,
$(\mathsf{Unroll})$ and $(\mathsf{Tight})$ are taken from Salomaa’s
axiomatisation of language equivalence of regular expressions [29] and thus
both sides of those equations denote the same formal languages [42, Theorem
5.2]. For $(\textsf{$\lambda$-Pref})$ assume that the premise is satisfied in
the model, that is $d_{\mathcal{L}}(\llbracket e\rrbracket,\llbracket
f\rrbracket)\leq\varepsilon$. Let
$\varepsilon^{\prime}\geq\lambda\cdot\varepsilon$. We show the following:

$\displaystyle d^{\mathcal{B}}(a\mathbin{;}e,a\mathbin{;}f)$
$\displaystyle=d_{\mathcal{L}}(\llbracket a\mathbin{;}e\rrbracket,\llbracket
a\mathbin{;}f\rrbracket)$ (Def. of $d^{\mathcal{B}}$)
$\displaystyle=\Phi_{\mathcal{L}}(d_{L})(\llbracket
a\mathbin{;}e\rrbracket,\llbracket a\mathbin{;}f\rrbracket)$ ($d_{L}$ is a
fixpoint of $\Phi_{\mathcal{L}}$)
$\displaystyle=\max\\{d_{2}(o_{\mathcal{L}}(a\mathbin{;}e),o_{\mathcal{L}}(a\mathbin{;}f)),\lambda\cdot\max_{a^{\prime}\in
A}d_{\mathcal{L}}(\llbracket a\mathbin{;}e\rrbracket_{a^{\prime}},\llbracket
a\mathbin{;}f\rrbracket_{a^{\prime}})\\}$ $\displaystyle=\lambda\cdot
d_{\mathcal{L}}(\llbracket e\rrbracket,\llbracket f\rrbracket)$ (Def. of final
automaton) $\displaystyle\leq\lambda\cdot\epsilon\leq\varepsilon^{\prime}$
(Assumptions)

Finally, $(\mathsf{SL5})$ is derivable from other axioms222We included
$(\mathsf{SL5})$ as an axiom to highlight the similarity of our inference
system with axiomatisations of language equivalence of regular expressions
[29, 19] containing the axioms of semilattices with bottom. In the previous
work [22], $(\mathsf{SL1-SL5})$ are precisely the axioms of _Quantitative
Semilattices with zero_ axiomatising the Hausdorff distance.. If
$\varepsilon=\max(\varepsilon,\varepsilon^{\prime})$ then
$\\{e\equiv_{\epsilon}g\\}\vdash
e\equiv_{\max(\varepsilon,\varepsilon^{\prime})}g$ holds by
$(\textsf{Assum})$. If $\epsilon<\max(\varepsilon,\varepsilon^{\prime})$, then
we can derive the quantitative judgement above using $(\textsf{Max})$. By a
similar line of reasoning, we can show that
$\\{f\equiv_{\epsilon^{\prime}}h\\}\vdash
f\equiv_{\max(\varepsilon,\varepsilon^{\prime})}h$. Finally, using
$(\textsf{Cut})$ and $(\textsf{NExp})$, we can show that
$\\{e\equiv_{\varepsilon}g,f\equiv_{\varepsilon^{\prime}}h\\}\vdash
e+f\equiv_{\max(\varepsilon,\varepsilon^{\prime})}g+h$ as desired.

We now revisit the example from Section 1. Recall that states marked as
initial of the left and middle automata can be respectively represented as
$a^{*}$ and $a+1$. The shortest word distinguishing languages representing
those expressions is $aa$. If we fix $\lambda=\frac{1}{2}$, then
$d_{\mathcal{L}}(\llbracket a^{*}\rrbracket,\llbracket
a+1\rrbracket)=\frac{1}{4}=\left(\frac{1}{2}\right)^{|aa|}$. We can derive
this distance through the means of axiomatic reasoning using the quantitative
equational theory REG in the following way:

######  Example 4.5.

$\displaystyle\vdash a^{*}$ $\displaystyle\equiv_{1}0$ (Top)
$\displaystyle\vdash a\mathbin{;}a^{*}$
$\displaystyle\equiv_{\frac{1}{2}}a\mathbin{;}0$ ($\lambda$-Pref)
$\displaystyle\vdash a\mathbin{;}a^{*}+1$
$\displaystyle\equiv_{\frac{1}{2}}a\mathbin{;}0+1$ ($\vdash 1\equiv_{0}1$ and
SL5) $\displaystyle\vdash a^{*}$ $\displaystyle\equiv_{\frac{1}{2}}1$ (Triang,
Unroll, S0 and SL4) $\displaystyle\vdash a\mathbin{;}a^{*}$
$\displaystyle\equiv_{\frac{1}{4}}a\mathbin{;}1$ ($\lambda$-Pref)
$\displaystyle\vdash a\mathbin{;}a^{*}+1$
$\displaystyle\equiv_{\frac{1}{4}}a\mathbin{;}1+1$ ($\vdash 1\equiv_{0}1$ and
SL5) $\displaystyle\vdash a^{*}$ $\displaystyle\equiv_{\frac{1}{4}}a+1$
(Triang, Unroll and S1)

### (The lack of) the fixpoint axiom.

Traditionally, completeness of inference systems for behavioural equivalence
of languages of expressions featuring recursive constructs such as Kleene star
or $\mu$-recursion [24] rely crucially on fixpoint introduction rules. Those
allow showing that an expression is provably equivalent to a looping construct
if it exhibits some form of self-similarity, typically subject to productivity
constraints. As an illustration, Salomaa’s axiomatisation of language
equivalence of regular expressions incorporates the following inference rule:

$\inferrule{g\equiv e\mathbin{;}g+f\qquad\epsilon\notin\llbracket
e\rrbracket}{g\equiv e^{*}\mathbin{;}f}$ (2)

The side condition on the right states that the loop body is _productive_ ,
that is a deterministic automaton corresponding to an expression $e$ cannot
immediately reach acceptance without performing any transitions. This is
simply equivalent to the language $\llbracket e\rrbracket$ not containing the
empty word. It would be reasonable for one to expect REG to contain a similar
rule to be complete, especially since it should be able to prove language
equivalence of regular expressions (by proving that they are in distance zero
from each other). Furthermore, all axioms of Salomaa except Equation 2 are
contained in REG as rules for distance zero.

It turns out that in the presence of the infinitary continuity (Cont) rule of
quantitative deduction systems and the ($\lambda$-Pref) axiom of REG, the
Salomaa’s inference rule (Equation 2) becomes a derivable fact for distance
zero. First of all, one can show that ($\lambda$-Pref) can be generalised from
prepending single letters to prepending any regular expression satisfying the
side condition from Equation 2.

######  Lemma 4.6.

Let $e,f,g\in\mathsf{Exp}$, such that $\epsilon\notin\llbracket e\rrbracket$.
Then, $\\{f\equiv_{\varepsilon}g\\}\vdash
e\mathbin{;}f\equiv_{\varepsilon^{\prime}}e\mathbin{;}g$ is derivable using
the axioms of REG for all $\varepsilon^{\prime}\geq\lambda\cdot\varepsilon$.

With the above lemma in hand, one can inductively show that if
$g\equiv_{0}e\mathbin{;}g+f$ and $\epsilon\notin\llbracket e\rrbracket$, then
$g$ gets arbitrarily close to $e^{*}\mathbin{;}f$. Intuitively, the more we
unroll the loop in $e^{*}\mathbin{;}f$ using (Unroll) and the more we unroll
the definition of $g$, then the closer both expressions become.

######  Lemma 4.7.

Let $e,f,g\in\mathsf{Exp}$, such that $\epsilon\notin\llbracket e\rrbracket$
and let $n\in\mathbb{N}$. Then, $\\{g\equiv_{0}e\mathbin{;}g+f\\}\vdash
g\equiv_{\varepsilon}e^{*}\mathbin{;}f$ is derivable using the axioms of
$\mathsf{REG}$ for all $\varepsilon\geq\lambda^{n}$.

Having the result above, we can now use the infinitary (Cont) rule capturing
the limiting property of decreasing chain of overapproximations to the
distance and show the derivability of Salomaa’s inference rule.

######  Lemma 4.8.

Let $e,f,g\in\mathsf{Exp}$, such that $\epsilon\notin\llbracket e\rrbracket$.
Then, $\\{g\equiv_{0}e\mathbin{;}g+f\\}\vdash g\equiv_{0}e^{*}\mathbin{;}f$ is
derivable using the axioms of REG.

######  Proof 4.9.

To deduce that $\vdash g\equiv_{0}e^{*}\mathbin{;}f$ using (Cont) it suffices
to show that $\vdash g\equiv_{\varepsilon}e^{*}\mathbin{;}f$ for all
$\varepsilon>0$. To do so, pick an arbitrary $\varepsilon>0$ and let
$N=\lceil\log_{\lambda}\varepsilon\rceil$. Observe that
$\lambda^{N}=\lambda^{\lceil\log_{\lambda}\varepsilon\rceil}\leq\lambda^{\log_{\lambda}\varepsilon}=\varepsilon$.
Because of Lemma 4.7 we have that $\vdash
g\equiv_{\varepsilon}e^{*}\mathbin{;}f$, which completes the proof.

##  5 Completeness

We now move on to the central result of this paper, which is the completeness
of REG with respect to the shortest-distinguishing-word metric on languages
denoting regular expressions. We use the strategy from the proof of
completeness of quantitative axiomatisation of probabilistic bisimilarity
distance [2]. It turns out that the results from [2] rely on properties that
are not unique to the Kantorovich/Wassertstein lifting and can be also
established for instances of the abstract coalgebraic framework [5].

The heart of our argument relies on the fact that the distance between
languages denoting regular expressions can be calculated in a simpler way than
applying the Knaster-Tarski fixpoint theorem while looking at the infinite-
state final automaton of all formal languages over some fixed alphabet. In
particular, regular expressions denote the behaviour of finite-state
deterministic automata. Since automata homomorphisms are non-expansive
mappings, the distance between languages $\llbracket e\rrbracket$ and
$\llbracket f\rrbracket$ of some arbitrary regular expressions
$e,f\in\mathsf{Exp}$ is the same as the distance between states in some DFA
whose languages corresponds to $\llbracket e\rrbracket$ and $\llbracket
f\rrbracket$. To be precise, we will look at the finite subautomaton
$\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$
of the ${\mathrel{\dot{\equiv}}}$ quotient of the Brzozowski automaton. The
reason we care about deterministic finite automata is that it turns out that
one can calculate the behavioural distance between two states through
iterative approximation from above, which can be also derived axiomatically
using the (Cont) rule of quantitative deduction systems. We start by showing
how this simplification works and then we move on to establishing
completeness.

### Behavioural distance on finite-state automata.

Consider a deterministic automaton $\mathcal{M}=(M,\langle
o_{M},t_{M}\rangle)$. The least fixpoint of a monotone endomap
$\Phi_{\mathcal{M}}:D_{M}\to D_{M}$ on the complete lattice of
$1$-pseudometrics on the set $M$ results in $d_{\mathcal{M}}$, which is a
behavioural pseudometric on the states of the automaton $\mathcal{M}$. It is
noteworthy that $\Phi_{\mathcal{M}}$ exhibits two generic properties. Firstly,
$\Phi_{\mathcal{M}}$ behaves well within the Banach space structure defined by
the supremum norm.

######  Lemma 5.1.

$\Phi_{\mathcal{M}}:D_{M}\to D_{M}$ is nonexpansive with respect to the
supremum norm. In other words, for all $d,d^{\prime}\in D_{M}$ we have that
$\|\Phi_{\mathcal{M}}(d^{\prime})-\Phi_{\mathcal{M}}(d)\|\leq\|d^{\prime}-d\|$.

######  Proof 5.2.

We can safely assume that $d\sqsubseteq d^{\prime}$, as other case will be
symmetric. It sufices to show that for all $m,m^{\prime}\in M$,
$\Phi_{\mathcal{M}}(d^{\prime})(m,m^{\prime})-\Phi_{\mathcal{M}}(d)(m,m^{\prime})\leq\|d^{\prime}-d\|$.
First, let’s consider the case when $o_{M}(m)\neq o_{M}(m^{\prime})$ and hence
$d_{2}(m,m^{\prime})=1$. In such a scenario, it holds that
$\Phi_{\mathcal{M}}(d^{\prime})(m,m^{\prime})-\Phi_{\mathcal{M}}(d)(m,m^{\prime})=0\leq\|d^{\prime}-d\|$.
From now on, we will assume that $o_{M}(m)=o_{M}(m)$ and hence
$d_{2}(m,m^{\prime})=0$. We have the following

$\displaystyle\Phi_{\mathcal{M}}(d^{\prime})(m,m^{\prime})-\Phi_{\mathcal{M}}(d)(m,m^{\prime})$
$\displaystyle=\lambda\cdot\max_{a\in
A}d^{\prime}(m_{a},m^{\prime}_{a})-\lambda\cdot\max_{a\in
A}d(m_{a},m^{\prime}_{a})$ $\displaystyle=\lambda\cdot\left(\max_{a\in
A}d^{\prime}(m_{a},m^{\prime}_{a})-\max_{a\in
A}d(m_{a},m^{\prime}_{a})\right)$
$\displaystyle\leq\lambda\cdot\left(\max_{a\in
A}\\{d^{\prime}(m_{a},m^{\prime}_{a})-d(m_{a},m^{\prime}_{a})\\}\right)$
$\displaystyle\leq\lambda\cdot\sup_{n,n^{\prime}\in
M}\\{d^{\prime}(n,n^{\prime})-d(n,n^{\prime})\\}$
$\displaystyle=\lambda\cdot\|d^{\prime}-d\|\leq\|d^{\prime}-d\|$

Secondly, it turns out that $\Phi_{\mathcal{M}}$ has only one fixpoint. This
means that if we want to calculate $d_{\mathcal{M}}$ it suffices to look at
any fixpoint of $\Phi_{\mathcal{M}}$. This will enable a simpler
characterisation, than the one given by the Knaster-Tarski fixpoint theorem.

######  Lemma 5.3.

$\Phi_{\mathcal{M}}$ has a unique fixed point.

######  Proof 5.4.

Let $d,d^{\prime}\in D_{M}$ be two fixed points of $\Phi_{\mathcal{M}}$, that
is $\Phi_{\mathcal{M}}(d)=d$ and $\Phi_{\mathcal{M}}(d^{\prime})=d^{\prime}$.
We can safely assume that $d\sqsubseteq d^{\prime}$, as the other case is
symmetric. We wish to show that $d=d^{\prime}$ and to do so we will use proof
by contradiction.

Assume that $d\neq d^{\prime}$, and hence there exist $m,m^{\prime}\in M$,
such that $d(m,m^{\prime})<d^{\prime}(m,m^{\prime})$ and
$\|d^{\prime}-d\|=d^{\prime}(m,m^{\prime})-d(m,m^{\prime})\neq 0$. First,
consider the case when $o_{M}(m)\neq o_{M}(m^{\prime})$. In such a case both
$d(m,m^{\prime})$ and $d(m,m^{\prime})$ are equal to $1$ and hence
$\|d^{\prime}-d\|=0$, which leads to contradiction. From now, we can safely
assume that $o_{M}(m)=o_{M}(m^{\prime})$. Through an identical line of
reasoning to the proof of Lemma 5.1, we can show that
$\|\Phi_{\mathcal{M}}(d^{\prime})-\Phi_{\mathcal{M}}(d)\|\leq\lambda\cdot\|d^{\prime}-d\|$.
Since both $d$ and $d^{\prime}$ are fixed points, this would mean that
$\|d^{\prime}-d\|\leq\lambda\cdot\|d^{\prime}-d\|$. Since
$\lambda\in\left]0,1\right[$, this would imply that $\|d^{\prime}-d\|=0$
leading again to contradiction.

In particular, we will rely on the characterisation given by the Kleene
fixpoint theorem [30, Theorem 2.8.5], which allows to obtain the greatest
fixpoint of an endofunction on the lattice as the infimum of the decreasing
sequence of finer approximations obtained by repeatedly applying the function
to the top element of the lattice.

######  Theorem 5.5 (Kleene fixpoint theorem).

Let $(X,\sqsubseteq)$ be a complete lattice with a top element $\top$ and
$f:X\to X$ an endofunction that is $\omega$-cocontinuous or in other words for
any decreasing chain $\\{x_{i}\\}_{i\in\mathbb{N}}$ it holds that
$\inf_{i\in\mathbb{N}}\\{f(x_{i})\\}=f\left(\inf_{i\in\mathbb{N}}x_{i}\right)$.
Then, $f$ possesses a greatest fixpoint, given by
$\operatorname{gfp}(f)=\inf_{i\in\mathbb{N}}\\{f^{(i)}(\top)\\}$ where
$f^{(n)}$ denotes $n$-fold self-composition of $f$ given inductively by
$f^{(0)}(x)=x$ and $f^{(n+1)}(x)=f^{(n+1)}(f(x))$ for all $x\in X$.

The theorem above requires the endomap to be $\omega$-cocontinuous. Luckily,
it is the case for $\Phi_{\mathcal{M}}$ if we restrict our attention to DFA.
To show that, we directly follow the line of reasoning from [2, Lemma 5.6]
generalising the similar line of reasoning for $\omega$-continuity from [36,
Theorem 1]. First, using Lemma 2.6 we show that decreasing chains of
pseudometrics over a finite set converge to their infimum. That result is a
minor re-adaptation of [36, Theorem 1] implicitly used in [2, Lemma 5.6].

######  Lemma 5.6.

Let $\\{d_{i}\\}_{i\in\mathbb{N}}$ be an infinite descending chain in the
lattice $(D_{X},\sqsubseteq)$, where $X$ is a finite set. The sequence
$\\{d_{i}\\}_{i\in\mathbb{N}}$ converges (in the sense of convergence in the
Banach space) to $d(x,y)=\inf_{i\in\mathbb{N}}d_{i}(x,y)$.

######  Proof 5.7.

Let $\varepsilon>0$ and let $x,y\in X$. Since
$d(x,y)=\inf_{i\in\mathbb{N}}d_{i}(x,y)$ there exists an index
$m_{x,y}\in\mathbb{N}$ such that for all $n\geq m_{x,y}$,
$|d_{n}(x,y)-d(x,y)|<\varepsilon$. Now, let $N=\max\\{m_{x,y}\mid x,y\in
X\\}$. This is well-defined because $X$ is finite. Therefore, for all $n\geq
N$ and $x,y\in X$, $|d_{n}(x,y)-d(x,y)|<\varepsilon$ and hence
$\|d_{n}-d\|<\varepsilon$.

We can now use the above to show the desired property, by re-adapting [36,
Theorem 1].

######  Lemma 5.8.

If $\mathcal{M}$ is a deterministic finite automaton, then
$\Phi_{\mathcal{M}}$ is $\omega$-cocontinuous.

######  Proof 5.9.

By Lemma 5.6, the chain $\\{d_{i}\\}_{i\in\mathbb{N}}$ converges to
$\inf_{i\in\mathbb{N}}d_{i}$. Since $\Phi_{\mathcal{M}}$ is nonexpansive
(Lemma 5.1) it is also continuous (in the sense of the Banach space
continuity) and therefore $\\{\Phi_{\mathcal{M}}(d_{i})\\}_{i\in\mathbb{N}}$
converges to $\Phi_{\mathcal{M}}\left(\inf_{i\in\mathbb{N}}d_{i}\right)$.
Recall that $\Phi_{\mathcal{M}}$ is monotone, which makes
$\\{\Phi_{\mathcal{M}}(d_{i})\\}_{i\in\mathbb{N}}$ into a chain, which by
Lemma 2.6 and Lemma 5.6 converges to
$\inf_{i\in\mathbb{N}}\\{\Phi_{\mathcal{M}}(d_{i})\\}$. Since limit points are
unique,
$\inf_{i\in\mathbb{N}}\\{\Phi_{\mathcal{M}}(d_{i})\\}=\Phi_{\mathcal{M}}\left(\inf_{i\in\mathbb{N}}d_{i}\right)$.

We can combine the preceding results and provide a straightforward
characterisation of the distance between languages represented by arbitrary
regular expressions, denoted as $e,f\in\mathsf{Exp}$. Utilising a simple
argument based on Proposition 3.1, which asserts that automata homomorphisms
are nonexpansive, one can demonstrate that the distance between $\llbracket
e\rrbracket$ and $\llbracket f\rrbracket$ in the final automaton is equivalent
to the distance between $[e]_{{\mathrel{\dot{\equiv}}}}$ and
$[f]_{{\mathrel{\dot{\equiv}}}}$ in
$\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$.
This is the least subautomaton of $\mathcal{Q}$ that contains the derivatives
(modulo ${\mathrel{\dot{\equiv}}}$) reachable from
$[e]_{{\mathrel{\dot{\equiv}}}}$ and $[f]_{{\mathrel{\dot{\equiv}}}}$.
Importantly, this automaton is finite (Lemma 2.3), allowing us to apply the
Kleene fixpoint theorem to calculate the distance.

Let ${\Psi}_{e,f}^{(0)}$ denote the discrete metric on the set
$\langle[e]{{\mathrel{\dot{\equiv}}}},[f]{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$
(the top element of the lattice of pseudometrics over that set). Define
${\Psi}_{e,f}^{(n+1)}=\Phi_{\langle[e]{{\mathrel{\dot{\equiv}}}},[f]{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}}({\Psi}_{e,f}^{(n)})$.
Additionally, leveraging the fact that infima of decreasing chains are
calculated pointwise (Lemma 2.6), we can conclude with the following:

######  Lemma 5.10.

For all $e,f\in\mathsf{Exp}$, the underlying pseudometric of the quantitative
algebra $\mathcal{B}$ can be given by
$d^{\mathcal{B}}(e,f)=\inf_{i\in\mathbb{N}}\left\\{{\Psi}_{e,f}^{(i)}\left([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\right)\right\\}$

In simpler terms, we have demonstrated that the behavioural distance between a
pair of arbitrary regular expressions can be calculated as the infimum of
decreasing approximations of the actual distance from above. Alternatively,
one could calculate the same distance as the supremum of increasing
approximations from below using the Kleene fixpoint theorem for the least
fixpoint. We chose the former approach because our proof of completeness
relies on the (Cont) rule of quantitative deduction systems. This rule
essentially states that to prove two terms are at a specific distance, we
should be able to prove that for all approximations of that distance from
above. This allows us to replicate the fixpoint calculation through axiomatic
reasoning.

### Completeness result.

We start by recalling that regular expressions satisfy a certain decomposition
property, stating that each expression can be reconstructed from its small-
step semantics, up to $\equiv_{0}$. This property, often referred to as the
fundamental theorem of Kleene Algebra/regular expressions (in analogy with the
fundamental theorem of calculus and following the terminology of Rutten [27]
and Silva [32]) is useful in further steps of the proof of completeness.

######  Theorem 5.11.

(Fundamental Theorem) For any $e\in\mathsf{Exp}$, $\vdash
e_{i}\equiv_{0}\sum_{a\in A}a\mathbin{;}(e_{i})_{a}+o_{\mathcal{R}}(e_{i})$ is
derivable using the axioms of REG.

The theorem above makes use of the $n$-ary generalised sum operator, which is
well defined because of (SL1-SL4) axioms of REG. Let’s now say that we are
interested in the distance between some expressions $e,f\in\mathsf{Exp}$. As
mentioned before, we will rely on
$\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$,
the least subautomaton of the ${\mathrel{\dot{\equiv}}}$ quotient of the
Brzozowski automaton containing states reachable from
$[e]_{{\mathrel{\dot{\equiv}}}}$ and $[f]_{{\mathrel{\dot{\equiv}}}}$. Recall
that by Lemma 2.3 its state space is finite. It turns out that the
approximations from above (from Lemma 5.10) to the distance between any pair
of states in that automaton can be derived through the means of axiomatic
reasoning.

######  Lemma 5.12.

Let $e,f\in\mathsf{Exp}$ be arbitrary regular expressions and let
$[g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}}\in\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$.
For all $i\in\mathbb{N}$, and
$\varepsilon\geq{\Psi}_{e,f}^{(i)}\left([g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}}\right)$,
one can derive $\vdash g\equiv_{\varepsilon}h$ using the axioms of
$\mathsf{REG}$.

######  Proof 5.13.

We proceed by induction on $i$. For the base case, observe that
${\Psi}_{e,f}^{(0)}$ is the discrete $1$-pseudometric on the set
$\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$
such that
${\Psi}_{e,f}^{(0)}([g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}})=0$
if and only if $g{\mathrel{\dot{\equiv}}}h$, or otherwise
${\Psi}_{e,f}^{(0)}([g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}})=1$.
In the first case, we immediately have that $g\equiv_{0}h$, because
${\mathrel{\dot{\equiv}}}$ is contained in distance zero axioms of REG. In the
latter case, we can just use $(\textsf{Top})$, to show that $g\equiv_{1}h$.
Then, in both cases, we can apply $(\textsf{Max})$ to obtain $\vdash
g\equiv_{\varepsilon}h$, since
$\varepsilon\geq{\Psi}_{e,f}^{(0)}([g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}})$.
For the induction step, let $i=j+1$ and derive the following:

$\displaystyle\varepsilon\geq{\Psi}_{e,f}^{(j+1)}([g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}})\iff\varepsilon\geq\Phi_{\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}}\left({\Psi}_{e,f}^{(j)}\right)\left([g]_{{\mathrel{\dot{\equiv}}}},[h]_{{\mathrel{\dot{\equiv}}}}\right)$
(Def. of ${\Psi}_{e,f}^{j+1}$) $\displaystyle\iff$
$\displaystyle\varepsilon\geq\max\left\\{d_{2}(o_{\mathcal{Q}}({[g]}_{{\mathrel{\dot{\equiv}}}}),o_{\mathcal{Q}}([h]_{{\mathrel{\dot{\equiv}}}})),\lambda\cdot\max_{a\in
A}\left\\{{\Psi}_{e,f}^{(j)}\left({[g]_{{\mathrel{\dot{\equiv}}}}}_{a},{[h]_{{\mathrel{\dot{\equiv}}}}}_{a}\right)\right\\}\right\\}$
(Def. of $\Phi$) $\displaystyle\iff$
$\displaystyle\varepsilon\geq\max\left\\{d_{2}\left(o_{\mathcal{R}}(g),o_{\mathcal{R}}(h)\right),\lambda\cdot\max_{a\in
A}\left\\{\Phi_{\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}}^{(j)}\left({[{(g)}_{a}]_{{\mathrel{\dot{\equiv}}}}},{[{(h)}_{a}]_{{\mathrel{\dot{\equiv}}}}}\right)\right\\}\right\\}$
(Def. of $\mathcal{Q}$) $\displaystyle\iff$ $\displaystyle{\varepsilon\geq
d_{2}(o_{\mathcal{R}}(g),o_{\mathcal{R}}(h))}\text{ and for all $a\in
A$},\leavevmode\nobreak\
\varepsilon\cdot\lambda^{-1}\geq{\Psi}_{e,f}^{(j)}\left({[{(g)}_{a}]_{{\mathrel{\dot{\equiv}}}}},{[{(h)}_{a}]_{{\mathrel{\dot{\equiv}}}}}\right)$

Firstly, since $d_{2}$ is the discrete $1$-pseudometric on the set
$\\{0,1\\}$, we can use $(\textsf{Refl})$ or $(\textsf{Top})$ depending on
whether $o_{\mathcal{R}}(g)=o_{\mathcal{R}}(h)$ and then apply
$(\textsf{Max})$ to derive $\vdash
o_{\mathcal{R}}(g)\equiv_{\varepsilon}o_{\mathcal{R}}(h)$.

Let $a\in A$. We will show that $\vdash
a\mathbin{;}(g)_{a}\equiv_{\varepsilon}a\mathbin{;}(h)_{a}$. Since
$\varepsilon\cdot\lambda^{-1}$ is not guaranteed to be rational, we cannot
immediately apply the induction hypothesis. Instead, we rely on (Cont) rule.
First, pick an arbitrary rational $\varepsilon^{\prime}$ strictly greater than
$\varepsilon$ and fix $\\{r_{n}\\}_{n\in\mathbb{N}}$ to be any decreasing
sequence of rationals that converges to $\lambda^{-1}$. Let $r_{N}$ be an
element of that sequence such that
$\varepsilon^{\prime}\geq\lambda\cdot\varepsilon\cdot r_{N}$. It is always
possible to pick such element because $\\{\lambda\cdot
r_{n}\\}_{n\in\mathbb{N}}$ is a decreasing sequence that converges to $1$ and
$\varepsilon^{\prime}>\varepsilon$. Since $\epsilon\cdot
r_{N}\geq\epsilon\cdot\lambda^{-1}$ and $\varepsilon\cdot
r_{N}\in\mathbb{Q}^{+}$, we can use the induction hypothesis and derive
$\vdash(g)_{a}\equiv_{\epsilon\cdot r_{N}}(h_{a})$. Then, by
$(\textsf{$\lambda$-Pref})$ axiom we have that $\vdash
a\mathbin{;}(g)_{a}\equiv_{\varepsilon^{\prime}}a\mathbin{;}(h)_{a}$. Since we
have shown it for arbitrary $\varepsilon^{\prime}>\varepsilon$, by (Cont) rule
we have that $\vdash
a\mathbin{;}(g)_{a}\equiv_{\varepsilon}a\mathbin{;}(h)_{a}$. Using (SL5), we
can combine all subexpressions involving the output and transition derivatives
into the following:

$\vdash\sum_{a\in
A}a\mathbin{;}(g)_{a}+o_{\mathcal{R}}(g)\equiv_{\varepsilon}\sum_{a\in
A}a\mathbin{;}(h)_{a}+o_{\mathcal{R}}(h)$

Since both sides are normal forms of $g$ and $h$ existing because of Theorem
5.11, we can apply (Triang) on both sides and obtain $\vdash
g\equiv_{\varepsilon}h$ thus completing the proof.

At this point, we have done all the hard work, and establishing completeness
involves a straightforward argument that utilises the (Cont) rule and the
lemma above.

######  Theorem 5.14 (Completeness).

For any $e,f\in\mathsf{Exp}$ and $\varepsilon\in\mathbb{Q}^{+}$, if
$\models_{\mathcal{B}}e\equiv_{\varepsilon}f$, then $\vdash
e\equiv_{\varepsilon}f\in\mathsf{REG}$

######  Proof 5.15.

Assume that $\models_{\mathcal{B}}e\equiv_{\varepsilon}f$, which by the
definition of $\models_{\mathcal{B}}$ is equivalent to
$d^{\mathcal{B}}(e,f)\leq\varepsilon$. In order to use (Cont) axiom to derive
$\vdash e\equiv_{\varepsilon}f$, we need to be able to show $\vdash
e\equiv_{\varepsilon^{\prime}}f$ for all $\varepsilon^{\prime}>\varepsilon$.
Because of iterative characterisation of $d^{\mathcal{B}}$ from Lemma 5.10, we
have that $\inf_{i\in
I}\\{{\Psi}_{e,f}^{(i)}([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}})\\}<\varepsilon^{\prime}$.
Since $\varepsilon^{\prime}$ is strictly above the infimum of the descending
chain of approximants, there exists a point $i\in\mathbb{N}$, such that
$\varepsilon^{\prime}>{\Psi}_{e,f}^{(i)}\left([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\right)$.
We can show this by contradiction.

Assume that for all $i\in\mathbb{N}$,
$\varepsilon^{\prime}\leq{\Psi}_{e,f}^{(i)}\left([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\right)$.
This would make $\varepsilon^{\prime}$ into the lower bound of the chain
$\left\\{{\Psi}_{e,f}^{(i)}([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}})\right\\}_{i\in\mathbb{N}}$
and in such a case $\varepsilon^{\prime}$ would be less than or equal to the
infimum of that chain, which by assumption is less than or equal to
$\varepsilon$. By transitivity, we could obtain
$\varepsilon^{\prime}\leq\varepsilon$. Since
$\varepsilon^{\prime}>\varepsilon$, by antisymmetry we could derive that
$\varepsilon^{\prime}=\varepsilon$, which would lead to the contradiction.

Using the fact shown above, we can use Lemma 5.12 to obtain $\vdash
e\equiv_{\varepsilon^{\prime}}f\in\mathsf{REG}$ for any
$\varepsilon^{\prime}>\varepsilon$, which completes the proof.

In simpler terms, the (Cont) rule enables us to demonstrate that two terms are
at a specific distance by examining all strict overapproximations of that
distance. Due to the iterative nature outlined in Lemma 5.10, this implies
that we only need to consider finite approximants used in the Kleene fixpoint
theorem. Each of those finite approximants can be axiomatically derived using
Lemma 5.12.

##  6 Discussion

We have presented a sound and complete axiomatisation of the shortest-
distinguishing word distance between languages representing regular
expressions through a quantitative analogue of equational logic [22]. Before
our paper, only axiomatised behavioural distances of probabilistic/weighted
transition systems existed, through (variants of) the Kantorovich/Wasserstein
lifting [21, 12, 4, 2, 1], while we looked at a behavioural distance obtained
through a more general coalgebraic framework [5]. Outside of the coalgebra
community, the shortest-distinguishing word distance and its variants also
appear in the model checking [20] and in the automata learning [14]
literature.

We have followed the strategy for proving completeness from [2]. The
interesting insight about that strategy is that it relies on properties that
are not exclusive to distances obtained through the Kantorovich/Wasserstein
lifting and can be established for notions of behavioural distance for other
kinds of transition systems stemming from the coalgebraic framework. In
particular, one needs to show that the monotone map on the lattice of
pseudometrics used in defining the distance of finite-state systems is
nonexpansive with respect to the sup norm (and hence $\omega$-cocontinuous)
and has a unique fixpoint, thus allowing to characterise the behavioural
distance as the greatest fixpoint obtained through the Kleene fixpoint
theorem. This point of view allows one to reconstruct the fixpoint calculation
in terms of axiomatic manipulation involving the (Cont) rule, eventually
leading to completeness.

We have additionally observed that in the presence of the infinitary (Cont)
rule and the ($\lambda$-Pref) axiom, there is no need for a fixpoint rule,
which is common place in all axiomatisations of regular expressions but also
in other work on distances. In particular, the previous work on axiomatising a
discounted probabilistic bisimilarity distance from [2] includes both
($\lambda$-Pref) and the fixpoint introduction rule, but its proof of
completeness [2, Theorem 6.4] does not involve the fixpoint introduction rule
at any point. We are highly confident that in the case of that axiomatisation,
the fixpoint introduction rule could be derived from other axioms in a similar
fashion to the way we derived Salomaa’s rule for introducing the Kleene star
[29]. Additionally, we are interested in how much this argument relates to the
recent study of fixpoints in quantitative equational theories [23].

Moreover, the axiomatisations from [1, 2] rely on a slight modification of
quantitative equational theories, which drop the requirement of all operations
from the signature to be nonexpansive. This is dictated by the fact that the
interpretation of $\mu$-recursion in Stark and Smolka’s probabilistic process
algebra [34] can increase the behavioural distances in the case of unguarded
recursion, while in regular expressions recursive behaviour is introduced
through Kleene’s star, whose interpretation is non-expansive with respect to
the shortest-distinguishing-word distance. This allowed us to fit instantly
into the original framework of quantitative equational theories. The earlier
work [4] focusing on Markov processes [8] also relies on quantitative
equational theories, but its syntax does not involve any recursive primitives.
Instead, the recursive behaviour is introduced through Cauchy completion of a
pseudometric induced by the axioms. The earliest works on axiomatising
behavioural distances of weighted [21] and probabilistic [12] transition
systems, studied before the introduction of quantitative equational theories,
rely on ad-hoc inference systems that cannot be easily generalised.

The pioneering works [13, 38, 36, 39, 37, 3] laid foundations for behavioural
(pseudo)metrics of various flavours of probabilistic transition systems. The
coalgebraic point of view [5] allowed to generalise these ideas to a wide
range of transition systems by moving from the Kantorovich/Wasserstein lifting
to the abstract setting of lifting endofunctors from the category of sets to
the category of pseudometric spaces. Building upon this theory, further lines
of work were dedicated to asymmetric distances (called hemimetrics) through
the theory of quasi-lax liftings [43], fuzzy analogues of Hennessy-Milner
logic characterising behavioural distance [17, 6], fibrational generalisations
involving quantale-enriched categories [7], up-to techniques allowing for
efficient approximation of behavioural distances [9] and quantitative
analogues of van Glabbek’s linear-time branching-time spectrum [15].

In this paper, we have focused on the simplest and most intuitive
instantiation of the coalgebraic framework in the case of deterministic
automata, but the natural next step would be to generalise our results to a
wider class of transition systems. A good starting point could be to consider
coalgebras for _polynomial_ endofunctors, in the fashion of the framework of
_Kleene Coalgebra_ [32]. Alternatively, it would be interesting to look at
recent work on a family of process algebras parametric on an equational theory
representing the branching constructs [31] and study its generalisations to
quantitative equational theories. A related and interesting avenue for future
work are equational axiomatisations of behavioural equivalence of Guarded
Kleene Algebra with Tests (GKAT) [33, 31] and its probabilistic extension
(ProbGKAT) [28], whose completeness results rely on a powerful uniqueness of
solutions axiom (UA). The soundness of UA in both cases is shown through an
involved argument relying on equipping the transition systems giving the
operational semantics with a form of behavioural distance and showing that
recursive specifications describing finite-state systems correspond to certain
contractive mappings. It may be more sensible, particularly for ProbGKAT to
consider quantitative axiomatisations in the first place and give the proofs
of completeness through the pattern explored in this paper.

## References

  * [1] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  Complete axiomatization for the total variation distance of markov chains.  In Sam Staton, editor, Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pages 27–39. Elsevier, 2018.  URL: https://doi.org/10.1016/j.entcs.2018.03.014, doi:10.1016/J.ENTCS.2018.03.014.
  * [2] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  A complete quantitative deduction system for the bisimilarity distance on markov chains.  Log. Methods Comput. Sci., 14(4), 2018.  doi:10.23638/LMCS-14(4:15)2018.
  * [3] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  Converging from branching to linear metrics on markov chains.  Math. Struct. Comput. Sci., 29(1):3–37, 2019.  doi:10.1017/S0960129517000160.
  * [4] Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.  An algebraic theory of markov processes.  In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 679–688. ACM, 2018.  doi:10.1145/3209108.3209177.
  * [5] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Coalgebraic behavioral metrics.  Log. Methods Comput. Sci., 14(3), 2018.  doi:10.23638/LMCS-14(3:20)2018.
  * [6] Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing.  Hennessy-milner theorems via galois connections.  In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, pages 12:1–12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  URL: https://doi.org/10.4230/LIPIcs.CSL.2023.12, doi:10.4230/LIPICS.CSL.2023.12.
  * [7] Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild.  Expressive quantale-valued logics for coalgebras: an adjunction-based approach.  CoRR, abs/2310.05711, 2023.  URL: https://doi.org/10.48550/arXiv.2310.05711, arXiv:2310.05711, doi:10.48550/ARXIV.2310.05711.
  * [8] Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden.  Bisimulation for labelled markov processes.  In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 149–158. IEEE Computer Society, 1997.  doi:10.1109/LICS.1997.614943.
  * [9] Filippo Bonchi, Barbara König, and Daniela Petrisan.  Up-to techniques for behavioural metrics via fibrations.  In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 17:1–17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.  URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17, doi:10.4230/LIPICS.CONCUR.2018.17.
  * [10] Janusz A. Brzozowski.  Derivatives of regular expressions.  J. ACM, 11(4):481–494, 1964.  doi:10.1145/321239.321249.
  * [11] Stanley Burris and H P Sankappanavar.  A Course in Universal Algebra.  Lecture Notes in Statistics. Springer, New York, NY, November 1981.
  * [12] Pedro R. D’Argenio, Daniel Gebler, and Matias David Lee.  Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules.  In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 289–303. Springer, 2014.  doi:10.1007/978-3-642-54830-7\\_19.
  * [13] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled markov processes.  Theor. Comput. Sci., 318(3):323–354, 2004.  URL: https://doi.org/10.1016/j.tcs.2003.09.013, doi:10.1016/J.TCS.2003.09.013.
  * [14] Tiago Ferreira, Gerco van Heerdt, and Alexandra Silva.  Tree-based adaptive model learning.  In Nils Jansen, Mariëlle Stoelinga, and Petra van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, volume 13560 of Lecture Notes in Computer Science, pages 164–179. Springer, 2022.  doi:10.1007/978-3-031-15629-8\\_10.
  * [15] Jonas Forster, Lutz Schröder, and Paul Wild.  Quantitative graded semantics and spectra of behavioural metrics.  CoRR, abs/2306.01487, 2023.  URL: https://doi.org/10.48550/arXiv.2306.01487, arXiv:2306.01487, doi:10.48550/ARXIV.2306.01487.
  * [16] Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka.  Algebraic reasoning for probabilistic concurrent systems.  In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990, pages 443–458. North-Holland, 1990.
  * [17] Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild.  Kantorovich functors and characteristic logics for behavioural distances.  In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 46–67. Springer, 2023.  doi:10.1007/978-3-031-30829-1\\_3.
  * [18] John E. Hopcroft and Richard M. Karp.  A linear algorithm for testing equivalence of finite automata.  1971\.  URL: https://api.semanticscholar.org/CorpusID:120207847.
  * [19] Dexter Kozen.  A completeness theorem for kleene algebras and the algebra of regular events.  Inf. Comput., 110(2):366–390, 1994.  URL: https://doi.org/10.1006/inco.1994.1037, doi:10.1006/INCO.1994.1037.
  * [20] Marta Z. Kwiatkowska.  A metric for traces.  Inf. Process. Lett., 35(3):129–135, 1990.  doi:10.1016/0020-0190(90)90061-2.
  * [21] Kim G. Larsen, Uli Fahrenberg, and Claus R. Thrane.  Metrics for weighted transition systems: Axiomatization and complexity.  Theor. Comput. Sci., 412(28):3358–3369, 2011.  URL: https://doi.org/10.1016/j.tcs.2011.04.003, doi:10.1016/J.TCS.2011.04.003.
  * [22] Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.  Quantitative algebraic reasoning.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 700–709. ACM, 2016.  doi:10.1145/2933575.2934518.
  * [23] Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin.  Fixed-points for quantitative equational logics.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.  doi:10.1109/LICS52264.2021.9470662.
  * [24] Robin Milner.  A complete inference system for a class of regular behaviours.  J. Comput. Syst. Sci., 28(3):439–466, 1984.  doi:10.1016/0022-0000(84)90023-0.
  * [25] David Michael Ritchie Park.  Concurrency and automata on infinite sequences.  In Theoretical Computer Science, 1981.  URL: https://api.semanticscholar.org/CorpusID:206841958.
  * [26] Walter Rudin.  Functional Analysis.  International Series in Pure & Applied Mathematics. McGraw Hill Higher Education, Maidenhead, England, 2 edition, October 1990.
  * [27] Jan J. M. M. Rutten.  Universal coalgebra: a theory of systems.  Theor. Comput. Sci., 249(1):3–80, 2000.  doi:10.1016/S0304-3975(00)00056-6.
  * [28] Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva.  Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity.  In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 136:1–136:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.136, doi:10.4230/LIPICS.ICALP.2023.136.
  * [29] Arto Salomaa.  Two complete axiom systems for the algebra of regular events.  J. ACM, 13(1):158–169, 1966.  doi:10.1145/321312.321326.
  * [30] Davide Sangiorgi.  Coinduction and the duality with induction, page 28–88.  Cambridge University Press, 2011.
  * [31] Todd Schmid, Wojciech Rozowski, Alexandra Silva, and Jurriaan Rot.  Processes parametrised by an algebraic theory.  In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 132:1–132:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.132, doi:10.4230/LIPICS.ICALP.2022.132.
  * [32] A.M Silva.  Kleene coalgebra.  PhD thesis, Radboud Universiteit Nijmegen, 2010.
  * [33] Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva.  Guarded kleene algebra with tests: verification of uninterpreted programs in nearly linear time.  Proc. ACM Program. Lang., 4(POPL):61:1–61:28, 2020.  doi:10.1145/3371129.
  * [34] Eugene W. Stark and Scott A. Smolka.  A complete axiom system for finite-state probabilistic processes.  In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 571–596. The MIT Press, 2000.
  * [35] Alfred Tarski.  A lattice-theoretical fixpoint theorem and its applications.  Pacific Journal of Mathematics, 5(2):285 – 309, 1955.
  * [36] Franck van Breugel.  On behavioural pseudometrics and closure ordinals.  Inf. Process. Lett., 112(19):715–718, 2012.  URL: https://doi.org/10.1016/j.ipl.2012.06.019, doi:10.1016/J.IPL.2012.06.019.
  * [37] Franck van Breugel.  Probabilistic bisimilarity distances.  ACM SIGLOG News, 4(4):33–51, 2017.  doi:10.1145/3157831.3157837.
  * [38] Franck van Breugel and James Worrell.  Towards quantitative verification of probabilistic transition systems.  In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 421–432. Springer, 2001.  doi:10.1007/3-540-48224-5\\_35.
  * [39] Franck van Breugel and James Worrell.  Approximating and computing behavioural distances in probabilistic transition systems.  Theor. Comput. Sci., 360(1-3):373–385, 2006.  URL: https://doi.org/10.1016/j.tcs.2006.05.021, doi:10.1016/J.TCS.2006.05.021.
  * [40] Rob J. van Glabbeek.  The linear time-branching time spectrum (extended abstract).  In Jos C. M. Baeten and Jan Willem Klop, editors, CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, volume 458 of Lecture Notes in Computer Science, pages 278–297. Springer, 1990.  URL: https://doi.org/10.1007/BFb0039066, doi:10.1007/BFB0039066.
  * [41] Cédric Villani.  Optimal Transport.  Springer Berlin Heidelberg, 2009.  URL: http://dx.doi.org/10.1007/978-3-540-71050-9, doi:10.1007/978-3-540-71050-9.
  * [42] Jana Wagemaker, Marcello M. Bonsangue, Tobias Kappé, Jurriaan Rot, and Alexandra Silva.  Completeness and incompleteness of synchronous kleene algebra.  In Graham Hutton, editor, Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, pages 385–413. Springer, 2019.  doi:10.1007/978-3-030-33636-3\\_14.
  * [43] Paul Wild and Lutz Schröder.  Characteristic logics for behavioural hemimetrics via fuzzy lax extensions.  Log. Methods Comput. Sci., 18(2), 2022.  URL: https://doi.org/10.46298/lmcs-18(2:19)2022, doi:10.46298/LMCS-18(2:19)2022.

##  Appendix A Preliminaries

See 2.2

######  Proof A.1.

Let $\iota:\langle e\rangle_{{\mathcal{R}}}\hookrightarrow\mathsf{Exp}$ be the
canonical inclusion homomorphism. Composing it with $L_{\mathcal{R}}$ a unique
homomorphism from $\mathcal{R}$ into the final automaton $\mathcal{L}$ yields
a homomorphism $L_{\mathcal{R}}\circ\iota$ from $\langle
e\rangle_{{\mathcal{R}}}$ to the final automaton, which is the same as
$L_{\langle e\rangle_{{\mathcal{R}}}}$, since homomorphisms into the final
automaton are unique. Using Lemma 2.2 we can show the following:

$\llbracket
e\rrbracket=L_{\mathcal{R}}(e)=L_{\mathcal{R}}(\iota(e))=L_{\langle
e\rangle_{{\mathcal{R}}}}(e)$

##  Appendix B Behavioural distances

See 3.1

######  Proof B.1.

Follows from [5, Theorem 5.23] and [5, Lemma 6.1]

See 3.2

######  Proof B.2.

  1. 1.

Follows from [5, Example 5.33], [5, Lemma 5.24] and [5, Theorem 6.10].

  2. 2.

Let $m,m^{\prime}\in M$. Recall that by Proposition 3.1,
$d_{\mathcal{M}}(m,m^{\prime})=d_{\mathcal{L}}(L_{\mathcal{M}}(m),L_{\mathcal{M}}(m^{\prime}))$.
The implication $d_{\mathcal{M}}(m,m^{\prime})=0\implies
L_{\mathcal{M}}(m)=L_{\mathcal{M}}(m^{\prime})$ follows from the fact that
$d_{\mathcal{L}}$ is a metric. The converse holds because of [5, Lemma 6.6].

##  Appendix C Quantitative algebras

See 4.2

######  Proof C.1.

Since $d_{\mathcal{L}}$ is a pseudometric, then
$d^{\mathcal{B}}=d_{\mathcal{L}}\circ(\llbracket-\rrbracket\times\llbracket-\rrbracket)$
is also a pseudometric. We now verify the nonexpansivity of interpretations of
operations with non-zero arity. Let $e,f,g,h\in\mathsf{Exp}$,
$d^{\mathcal{B}}(e,g)\leq\varepsilon$ and
$d^{\mathcal{B}}(f,h)\leq\varepsilon$.

  1. 1.

We show that $d^{\mathcal{B}}(e+f,g+h)\leq\varepsilon$. In the case when
$\varepsilon=0$, the proof simplifies to showing that if $\llbracket
e\rrbracket=\llbracket g\rrbracket$ and $\llbracket f\rrbracket=\llbracket
h\rrbracket$ then $\llbracket e+f\rrbracket=\llbracket g+h\rrbracket$, which
holds immediately. For the remaining case, when $\varepsilon>0$, let
$n=\lceil\log_{\lambda}\varepsilon\rceil$. Observe that in such a case, we
have that $d^{\mathcal{B}}(e,g)\leq\lambda^{n}$ and
$d^{\mathcal{B}}(f,h)\leq\lambda^{n}$. Using it, we can deduce that
$\llbracket e\rrbracket$ and $\llbracket g\rrbracket$ (and similarly
$\llbracket f\rrbracket$ and $\llbracket h\rrbracket$) agree on all words of
length strictly below $n$ (because the shortest word for which they disagree
is at least of length $n$). To put that more formally:

$\forall w\in A^{\ast}\ldotp|w|<n\implies\left(w\in\llbracket e\rrbracket\iff
w\in\llbracket g\rrbracket\right)\wedge\left(w\in\llbracket f\rrbracket\iff
w\in\llbracket h\rrbracket\right)$

Let $w\in A^{\ast}$, such that $|w|<n$. We have that

$\displaystyle w\in\llbracket e+f\rrbracket$ $\displaystyle\iff w\in\llbracket
e\rrbracket\cup\llbracket f\rrbracket\iff\left(w\in\llbracket
e\rrbracket\right)\vee\left(w\in\llbracket f\rrbracket\right)$
$\displaystyle\iff\left(w\in\llbracket
g\rrbracket\right)\vee\left(w\in\llbracket h\rrbracket\right)$ ($|w|<n$)
$\displaystyle\iff w\in\llbracket g+h\rrbracket$

And thus $\llbracket e+f\rrbracket$ and $\llbracket g+h\rrbracket$ agree on
all words of the length below $n$ and therefore
$d^{\mathcal{B}}(e+f,g+h)\leq\lambda^{n}\leq\varepsilon$.

  2. 2.

The case for $\varepsilon=0$ holds immediately through the same line of
reasoning as before, relying on well-definedness of $\diamond$ (concatenation)
operation on languages. We focus on the remaining case, making the same
simplification as before, that is we assume that $\llbracket e\rrbracket$ and
$\llbracket g\rrbracket$ (as well as $\llbracket f\rrbracket$ and $\llbracket
h\rrbracket$) agree on all word of length strictly below $n$). We show that
$\llbracket e\mathbin{;}f\rrbracket$ and $\llbracket g\mathbin{;}h\rrbracket$
also agree on all words of the length strictly less than $n$. Let $w\in
A^{\ast}$, such that $|w|<n$. We have that:

$\displaystyle w\in\llbracket e\mathbin{;}f\rrbracket$ $\displaystyle\iff
w\in\llbracket e\rrbracket\diamond\llbracket f\rrbracket$
$\displaystyle\iff\left(\exists u,v\in A^{*}.w=uv\wedge w\in\llbracket
e\rrbracket\wedge v\in\llbracket f\rrbracket\right)$
$\displaystyle\iff\left(\exists u,v\in A^{*}.w=uv\wedge w\in\llbracket
g\rrbracket\wedge v\in\llbracket h\rrbracket\right)$ ( $|u|<n$ and $|v|<n$)
$\displaystyle\iff w\in\llbracket g\rrbracket\diamond\llbracket
h\rrbracket\iff w\in\llbracket g\mathbin{;}h\rrbracket$

  3. 3.

We use the same line of reasoning as before. Assume that $\llbracket
e\rrbracket$ and $\llbracket g\rrbracket$ agree on all words of length below
$n$. Let $w\in A^{*}$, such that $|w|<n$. We have the following:

$\displaystyle w\in\llbracket e^{*}\rrbracket$ $\displaystyle\iff
w\in\llbracket e\rrbracket^{*}$ $\displaystyle\iff
w=\varepsilon\vee\left(\exists k\geq 1\ldotp\exists u_{1},\dots,u_{k}\in
A^{*}\ldotp w=u_{1}\dots u_{k}\right.$ $\displaystyle\left.\qquad\qquad\wedge
u_{1}\in\llbracket e\rrbracket\wedge\dots\wedge u_{k}\in\llbracket
e\rrbracket\right)$ $\displaystyle\iff w=\varepsilon\vee\left(\exists k\geq
1\ldotp\exists u_{1},\dots,u_{k}\in A^{*}\ldotp w=u_{1}\dots u_{k}\right.$
$\displaystyle\left.\qquad\qquad\wedge u_{1}\in\llbracket
g\rrbracket\wedge\dots\wedge u_{k}\in\llbracket g\rrbracket\right)$
($|u_{1}|<n,\dots,|u_{k}|<n$ ) $\displaystyle\iff w\in\llbracket
g\rrbracket^{*}\iff w\in\llbracket g^{*}\rrbracket$

See 4.6

######  Proof C.2.

By induction on $e\in\mathsf{Exp}$. The cases when $e=1$ and $e=(e_{1})^{*}$
are not possible, because of the assumption that $\epsilon\notin\llbracket
e\rrbracket$.

$e=0$ Because of the $(\mathsf{0S})$ axiom, we can derive that
$e\mathbin{;}f\equiv_{0}0\equiv_{0}0\mathbin{;}g\equiv_{0}e\mathbin{;}g$. We
can show the desired conclusion, using $(\textsf{Max})$ axiom.

$e=a$ Holds immediately, because of $(\textsf{$\lambda$-Pref})$ axiom.

$e=e_{1}+e_{2}$ Because of the assumption, both $\epsilon\notin\llbracket
e_{1}\rrbracket$ and $\epsilon\notin\llbracket e_{2}\rrbracket$. Using the
induction hypothesis, we can derive that $\vdash
e_{1}\mathbin{;}f\equiv_{\varepsilon^{\prime}}e_{1}\mathbin{;}g$ and
$e_{2}\mathbin{;}f\equiv_{\varepsilon^{\prime}}e_{2}\mathbin{;}g$. We can
apply the $(\mathsf{SL5})$ axiom to derive that $\vdash
e_{1}\mathbin{;}f+e_{2}\mathbin{;}f\equiv_{\varepsilon^{\prime}}e_{1}\mathbin{;}g+s_{2}\mathbin{;}g$.
Finally, we can apply the $(\mathsf{D2})$ axiom to both sides through (Triang)
and derive
$\vdash(e_{1}+e_{2})\mathbin{;}f\equiv_{\varepsilon^{\prime}}(e_{1}+e_{2})\mathbin{;}g$
as desired.

$e=e_{1}\mathbin{;}e_{2}$ Because of the assumption, $\epsilon\notin\llbracket
e_{1}\rrbracket$ or $\epsilon\notin\llbracket e_{2}\rrbracket$. First, let’s
consider the subcase when both $\epsilon\notin\llbracket e_{1}\rrbracket$ and
$\epsilon\notin\llbracket e_{2}\rrbracket$. By induction hypothesis, we have
that $\vdash e_{2}\mathbin{;}f\equiv_{\varepsilon^{\prime}}e_{2}\mathbin{;}g$.
Since $\lambda\in]0,1[$, we have that
$\lambda\cdot\varepsilon^{\prime}<\varepsilon^{\prime}$. Because of that, we
can apply induction hypothesis again and obtain $\vdash
e_{1}\mathbin{;}e_{2}\mathbin{;}f\equiv_{\varepsilon^{\prime}}e_{1}\mathbin{;}e_{2}\mathbin{;}g$.
Now, let’s consider the subcase when $\epsilon\notin\llbracket
e_{1}\rrbracket$, but $\epsilon\in\llbracket e_{2}\rrbracket$. Using
$(\textsf{NExp})$, we can obtain $\vdash
e_{2}\mathbin{;}f\equiv_{\varepsilon}e_{2}\mathbin{;}g$. Then, since
$\epsilon\notin\llbracket e_{1}\rrbracket$, we can apply the induction
hypothesis and obtain $\vdash
e_{1}\mathbin{;}e_{2}\mathbin{;}f\equiv_{\varepsilon^{\prime}}e_{1}\mathbin{;}e_{2}\mathbin{;}g$
as desired. The remaining subcase, when $\epsilon\notin\llbracket
e_{2}\rrbracket$ but $\epsilon\in\llbracket e_{1}\rrbracket$ is symmetric and
therefore omitted.

See 4.7

######  Proof C.3.

By induction. If $n=0$, then using $(\textsf{Top})$, we can immediately
conclude that $\vdash g\equiv_{1}e^{*}\mathbin{;}f$. Since by the assumption
$\varepsilon\geq\lambda^{0}=1$, we can apply (Max) and obtain $\vdash
g\equiv_{\varepsilon}e^{*}\mathbin{;}f$.

For the inductive cases, we have that $\varepsilon\geq\lambda^{n+1}$ and hence
$\varepsilon\cdot\lambda^{-1}\geq\lambda^{n}$. We cannot instantly apply the
induction hypothesis, as $\varepsilon\cdot\lambda^{-1}$ is not guaranteed to
be rational. Instead, we will use (Cont) of quantitative deduction systems.
Let $\varepsilon^{\prime}$ be an arbitrary rational number strictly greater
than $\varepsilon$ and let $\\{r_{n}\\}_{n\in\mathbb{N}}$ be any decreasing
sequence of rationals that converges to $\lambda^{-1}$. Pick element $r_{N}$
of that sequence that satisfies that
$\varepsilon^{\prime}\geq\varepsilon\cdot\lambda\cdot r_{N}$. We can always
pick such an element, as $\\{r_{n}\\}_{n\in\mathbb{N}}$ gets arbitrarily close
to $\lambda^{-1}$, so $\\{\lambda\cdot r_{n}\\}_{n\in\mathbb{N}}$ is a
decreasing sequence that converges to $1$ and additionally we have that
$\varepsilon^{\prime}>\varepsilon$, so
$\frac{\varepsilon^{\prime}}{\varepsilon}>1$. From the definition of the
limit, we know that there exists large enough $N\in\mathbb{N}$, such that
$|\lambda\cdot r_{N}-1|\leq\frac{\varepsilon^{\prime}}{\varepsilon}-1$. We can
simplify the above relying on the fact that $\lambda\cdot r_{n}\geq 1$ for all
$n\in\mathbb{N}$ and obtain that indeed
$\varepsilon^{\prime}\geq\varepsilon\cdot\lambda\cdot r_{N}$ as desired.

Since $\varepsilon\cdot r_{N}\geq\varepsilon\cdot\lambda^{-1}\geq\lambda^{n}$,
we can apply induction hypothesis and obtain that $\vdash
e\equiv_{\varepsilon\cdot r_{N}}g^{*}\mathbin{;}f$. Since
$\epsilon\notin\llbracket e\rrbracket$, we can now use Lemma 4.6 to derive
that
$e\mathbin{;}g\equiv_{\varepsilon^{\prime}}e\mathbin{;}e^{*}\mathbin{;}f$.
Since we have shown it for arbitrary $\varepsilon^{\prime}>\varepsilon$, we
can use (Cont) rule of the quantitative deduction systems and conclude that
$\vdash e\mathbin{;}g\equiv_{\varepsilon}e\mathbin{;}e^{*}\mathbin{;}f$, as
desired.

Then, because of $(\textsf{Refl})$, we have that $\vdash f\equiv_{0}f$. We can
combine those two quantitative inferences using $(\mathsf{SL5})$ axiom in
order to get $\vdash
e\mathbin{;}g+f\equiv_{\varepsilon}e\mathbin{;}e^{*}\mathbin{;}f+f$. By
assumption, the left hand side satisfies that $\vdash
g\equiv_{0}e\mathbin{;}g+f$. Now, consider the right hand side of that
quantitative inference:

$\displaystyle\vdash e\mathbin{;}e^{*}\mathbin{;}f+f$
$\displaystyle\equiv_{0}e\mathbin{;}e^{*}\mathbin{;}f+1\mathbin{;}f$
($\mathsf{1S}$) $\displaystyle\equiv_{0}(e\mathbin{;}e^{*}+1)\mathbin{;}f$
($\mathsf{D2}$) $\displaystyle\equiv_{0}e^{*}\mathbin{;}f$ ($\mathsf{Unroll}$)

We can combine the reasoning above and conclude (using Triang) that $\vdash
g\equiv_{\varepsilon}e^{*}\mathbin{;}f$.

##  Appendix D Completeness

See 5.10

######  Proof D.1.

Recall that
$d^{\mathcal{B}}=d_{\mathcal{L}}\circ(\llbracket-\rrbracket\times\llbracket-\rrbracket)$.
Moreover, the canonical quotient map
$[-]_{{\mathrel{\dot{\equiv}}}}:\mathsf{Exp}\to{\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}$
is an automaton homomorphism from $\mathcal{R}$ to $\mathcal{Q}$. Composing it
with a language assigning homomorphism
$L_{\mathcal{Q}}:{\mathsf{Exp}}/{{\mathrel{\dot{\equiv}}}}\to\mathcal{P}(A^{\ast})$
yields an automaton homomorphism
$L_{\mathcal{Q}}\circ[-]_{{\mathrel{\dot{\equiv}}}}:\mathsf{Exp}\to\mathcal{P}(A^{\ast})$,
which by finality must be the same as
$L_{\mathcal{R}}:\mathsf{Exp}\to\mathcal{P}(A^{\ast})$, and thus (by Lemma
2.2) the same as $\llbracket-\rrbracket$. Using the fact that automata
homomorphisms are isometric mappings between pseudometric spaces obtained
through constructing behavioural pseudometrics (Proposition 3.1), we can
derive the following:

$\displaystyle d^{\mathcal{B}}$
$\displaystyle=d_{\mathcal{L}}\circ(\llbracket-\rrbracket\times\llbracket-\rrbracket)$
$\displaystyle=d_{\mathcal{L}}\circ((L_{\mathcal{Q}}\circ([-]_{{\mathrel{\dot{\equiv}}}})\times(L_{\mathcal{Q}}\circ([-]_{{\mathrel{\dot{\equiv}}}}))$
$\displaystyle=d_{\mathcal{L}}\circ(L_{\mathcal{Q}}\times
L_{\mathcal{Q}})\circ([-]_{{\mathrel{\dot{\equiv}}}}\times[-]_{{\mathrel{\dot{\equiv}}}})$
$\displaystyle=d_{\mathcal{Q}}\circ([-]_{{\mathrel{\dot{\equiv}}}}\times[-]_{{\mathrel{\dot{\equiv}}}})$
(Proposition 3.1)

Additionally, since
$\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$
is the subautomaton of $\mathcal{Q}$ containing all the derivatives (modulo
${\mathrel{\dot{\equiv}}}$) of $e$ and $f$, the canonical inclusion map
$\iota:\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}\hookrightarrow\mathcal{Q}$
is an automaton homomorphism. Because
$\iota([e]_{{\mathrel{\dot{\equiv}}}})=[e]_{{\mathrel{\dot{\equiv}}}}$ and
$\iota([f]_{{\mathrel{\dot{\equiv}}}})=[f]_{{\mathrel{\dot{\equiv}}}}$, we can
again use Proposition 3.1 to show that

$d^{\mathcal{B}}(e,f)=d_{\mathcal{Q}}([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}})=d_{\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}}([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}})$

Because of the fact that
$([e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}})$ has finitely
many states (Lemma 2.3) then by Lemma 5.3, Lemma 5.8 and Theorem 5.5 one can
use the simplified iterative formula to calculate the behavioural pseudometric
on
$\langle[e]_{{\mathrel{\dot{\equiv}}}},[f]_{{\mathrel{\dot{\equiv}}}}\rangle_{{\mathcal{Q}}}$.

See 5.11

######  Proof D.2.

We proceed by induction on $e\in\mathsf{Exp}$. The base cases are trivial, so
we just demonstrate the case when $e=a$ for $a\in A$.

$e=a$

$\displaystyle\vdash a$ $\displaystyle\equiv_{0}a\mathbin{;}1$ ($\mathsf{S1}$)
$\displaystyle\equiv_{0}a\mathbin{;}1+0$ ($\mathsf{SL4}$)
$\displaystyle\equiv_{0}a\mathbin{;}(a)_{a}+o_{\mathcal{R}}(a)$ (Def. of
derivatives)

Now, observe that for all $a^{\prime}\in A\setminus\\{a\\}$, we have that
$(a)_{a}^{\prime}=0$. Using axiom ($\mathsf{S0}$),
$a^{\prime}\mathbin{;}(a)_{a^{\prime}}\equiv_{0}0$. Through induction on the
size of $A\setminus\\{a\\}$, using axioms ($\mathsf{SL1}$) and
($\mathsf{SL4}$), one can show that $\sum_{a^{\prime}\in
A\setminus\\{a\\}}a^{\prime}\mathbin{;}(a)_{a^{\prime}}\equiv_{0}0$. We can
now combine the intermediate results into the following:

$\displaystyle\vdash a$
$\displaystyle\equiv_{0}a\mathbin{;}(a)_{a}+o_{\mathcal{R}}(a)$ (Previous
derivations) $\displaystyle\equiv_{0}a\mathbin{;}(a)_{a}+o_{\mathcal{R}}(a)+0$
($\mathsf{SL1}$)
$\displaystyle\equiv_{0}a\mathbin{;}(a)_{a}+0+o_{\mathcal{R}}(a)$
($\mathsf{SL2}$)
$\displaystyle\equiv_{0}a\mathbin{;}(a)_{a}+\sum_{a^{\prime}\in
A\setminus\\{a\\}}a^{\prime}\mathbin{;}(a)_{a^{\prime}}+o_{\mathcal{R}}(a)$
(Previous inductive argument) $\displaystyle\equiv_{0}\sum_{a^{\prime}\in
A}a^{\prime}\mathbin{;}(a)_{a^{\prime}}+o_{\mathcal{R}}(a)$ (Def. of $n$-ary
sum)

$e=f+g$

$\displaystyle\vdash f+g$ $\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}+o_{\mathcal{R}}(f)\right)+\left(\sum_{a\in
A}a\mathbin{;}(g)_{a}+o_{\mathcal{R}}(g)\right)$ (Induction hypothesis)
$\displaystyle\equiv_{0}\sum_{a\in
A}\left(a\mathbin{;}(f)_{a}+a\mathbin{;}(g)_{a}\right)+\left(o_{\mathcal{R}}(f)+o_{\mathcal{R}}(g)\right)$
($\mathsf{S3}$) $\displaystyle\equiv_{0}\sum_{a\in
A}\left(a\mathbin{;}\left((f)_{a}+(g)_{a}\right)\right)+\left(o_{\mathcal{R}}(f)+o_{\mathcal{R}}(g)\right)$
($\mathsf{D1}$) $\displaystyle\equiv_{0}\sum_{a\in
A}\left(a\mathbin{;}\left((f+g)_{a}\right)\right)+o_{\mathcal{R}}(f+g)$ (Def.
of derivatives)

$e=f\mathbin{;}g$

$\displaystyle\vdash f\mathbin{;}g$ $\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}+o_{\mathcal{R}}(f)\right)\mathbin{;}g$ (Induction
hypothesis) $\displaystyle\equiv_{0}\sum_{a\in
A}a\mathbin{;}(f)_{a}\mathbin{;}g+o_{\mathcal{R}}(f)\mathbin{;}g$
($\mathsf{D2}$) $\displaystyle\equiv_{0}\sum_{a\in
A}a\mathbin{;}(f)_{a}\mathbin{;}g+o_{\mathcal{R}}(f)\mathbin{;}\left(\sum_{a\in
A}a\mathbin{;}(g)_{a}+o_{\mathcal{R}}(g)\right)$ (Induction hypothesis)
$\displaystyle\equiv_{0}\sum_{a\in
A}a\mathbin{;}(f)_{a}\mathbin{;}g+\left(\sum_{a\in
A}o_{\mathcal{R}}(f)\mathbin{;}a\mathbin{;}(g)_{a}+o_{\mathcal{R}}(f)\mathbin{;}o_{\mathcal{R}}(g)\right)$
($\mathsf{D1}$) $\displaystyle\equiv_{0}\sum_{a\in
A}a\mathbin{;}(f)_{a}\mathbin{;}g+\left(\sum_{a\in
A}a\mathbin{;}o_{\mathcal{R}}(f)\mathbin{;}(g)_{a}+o_{\mathcal{R}}(f)\mathbin{;}o_{\mathcal{R}}(g)\right)$
(($\mathsf{1S}$) and ($\mathsf{S1}$) if $o_{\mathcal{R}}(f)=1$ or
($\mathsf{0S}$) and ($\mathsf{S0}$) if $o_{\mathcal{R}}(f)=0$)
$\displaystyle\equiv_{0}\sum_{a\in
A}\left(a\mathbin{;}(f)_{a}\mathbin{;}g+a\mathbin{;}o_{\mathcal{R}}(f)\mathbin{;}(g)_{a}\right)+o_{\mathcal{R}}(f)\mathbin{;}o_{\mathcal{R}}(g)$
($\mathsf{SL3}$) $\displaystyle\equiv_{0}\sum_{a\in
A}a\mathbin{;}\left((f)_{a}\mathbin{;}g+o_{\mathcal{R}}(f)\mathbin{;}(g)_{a}\right)+o_{\mathcal{R}}(f)\mathbin{;}o_{\mathcal{R}}(g)$
($\mathsf{D1}$) $\displaystyle\equiv_{0}\sum_{a\in
A}a\mathbin{;}\left(f\mathbin{;}g\right)_{a}+o_{\mathcal{R}}(f\mathbin{;}g)$
(Def. of derivatives)

$e=f^{\ast}$

$\displaystyle\vdash f^{\ast}$ $\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}+o_{\mathcal{R}}(f)\right)^{\ast}$ (Induction hypothesis)
$\displaystyle\equiv_{0}\left(\sum_{a\in A}a\mathbin{;}(f)_{a}\right)^{\ast}$
(($\mathsf{Tight}$) if $o_{\mathcal{R}}=1$ or ($\mathsf{SL4}$) if
$o_{\mathcal{R}}=0$) $\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}\right)\mathbin{;}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}\right)^{\ast}+1$ ($\mathsf{Unroll}$)
$\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}\right)\mathbin{;}f^{\ast}+1$ (Steps 1-2 and
$(\textsf{NExp})$) $\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}(f)_{a}\mathbin{;}f^{\ast}\right)+1$ ($\mathsf{D2}$)
$\displaystyle\equiv_{0}\left(\sum_{a\in
A}a\mathbin{;}\left(f^{\ast}\right)_{a}\right)+o_{\mathcal{R}}\left(f^{\ast}\right)$
(Def. of derivatives)