University College, London<EMAIL_ADDRESS>St. Mary’s College of
California<EMAIL_ADDRESS>Indiana University<EMAIL_ADDRESS>Todd Schmid and Victoria Noquez and Lawrence S. Moss [500]Theory of
computation Process Calculi Paolo Baldan and Valeria de Paiva 2 10th
Conference on Algebra and Coalgebra in Computer Science (CALCO 2023) CALCO
2023 CALCO 2023 June 19–22, 2023 Bloomington IN, USA 211

# Fractals from Regular Behaviours

Todd Schmid  Victoria Noquez  Lawrence S. Moss

###### Abstract

We are interested in connections between the theory of fractal sets obtained
as attractors of iterated function systems and process calculi. To this end,
we reinterpret Milner’s expressions for processes as contraction operators on
a complete metric space. When the space is, for example, the plane, the
denotations of fixed point terms correspond to familiar fractal sets. We give
a sound and complete axiomatization of fractal equivalence, the congruence on
terms consisting of pairs that construct identical self-similar sets in all
interpretations. We further make connections to labelled Markov chains and to
invariant measures. In all of this work, we use important results from process
calculi. For example, we use Rabinovich’s completeness theorem for trace
equivalence in our own completeness theorem. In addition to our results, we
also raise many questions related to both fractals and process calculi.

###### keywords:

fixed-point terms, labelled transition system, fractal, final coalgebra,
equational logic, completeness

##  1 Introduction

Hutchinson noticed in [14] that many familiar examples of fractals can be
captured as the set-wise fixed-point of a finite family of contraction (i.e.,
distance shrinking) operators on a metric space. He called these spaces
_(strictly) self-similar_ , since the intuition behind the contraction
operators is that they are witnesses for the appearance of the fractal in a
proper (smaller) subset of itself. For example, the famous Sierpiński gasket
is the unique nonempty compact subset of the plane left fixed by the union of
the three operators
$\sigma_{a},\sigma_{b},\sigma_{c}:\mathbb{R}^{2}\to\mathbb{R}^{2}$ in Figure
1. The Sierpiński gasket is a scaled-up version of each of its thirds.

$\begin{gathered}\leavevmode\hbox to70.44pt{\vbox to25.4pt{\pgfpicture\makeatletter\hbox{\hskip 57.74333pt\lower-12.70001pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {{}\pgfsys@rect{-12.50002pt}{-12.50002pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85764pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{} {{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}} {{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{}{}{}}{}{}{}{}{{}}{}{{ {\pgfsys@beginscope{} {} {} {} \pgfsys@moveto{1.99997pt}{0.0pt}\pgfsys@lineto{-1.19998pt}{1.59998pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{-1.19998pt}{-1.59998pt}\pgfsys@fill\pgfsys@endscope}} }{}{}{{}}\pgfsys@moveto{-12.70001pt}{-3.4025pt}\pgfsys@curveto{-33.21121pt}{-8.89923pt}{-33.21121pt}{8.89923pt}{-15.59776pt}{4.17903pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.96593}{-0.25885}{0.25885}{0.96593}{-15.59776pt}{4.17903pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-54.41032pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a,b,c$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\ \\\ \sigma_{a}\begin{bmatrix}r\\\ s\end{bmatrix}=\begin{bmatrix}\frac{1}{2}r+\frac{1}{4}\\\ \frac{1}{2}s+\frac{\sqrt{3}}{4}\end{bmatrix}\qquad\sigma_{b}\begin{bmatrix}r\\\ s\end{bmatrix}=\begin{bmatrix}\frac{1}{2}r\\\ \frac{1}{2}s\end{bmatrix}\\\ \sigma_{c}\begin{bmatrix}r\\\ s\end{bmatrix}=\begin{bmatrix}\frac{1}{2}r+\frac{1}{2}\\\ \frac{1}{2}s\end{bmatrix}\end{gathered}$ |
---|---
Figure 1:  The Sierpiński gasket is the unique nonempty compact subset
$\mathbf{S}$ of $\mathbf{R}^{2}$ such that
$\mathbf{S}=\sigma_{a}(\mathbf{S})\cup\sigma_{b}(\mathbf{S})\cup\sigma_{c}(\mathbf{S})$.
Each of its points corresponds to a stream emitted by the state $x$.

The self-similarity of Hutchinson’s fractals hints at an algorithm for
constructing them: Each point in a self-similar set is the limit of a sequence
of points obtained by applying the contraction operators one after the other
to an initial point. In the Sierpiński gasket, the point $(1/4,1/2)$ is the
limit of the sequence

$p,\ \sigma_{b}(p),\ \sigma_{b}\sigma_{a}(p),\
\sigma_{b}\sigma_{a}\sigma_{a}(p),\
\sigma_{b}\sigma_{a}\sigma_{a}\sigma_{a}(p),\ \dots$ (1)

where the initial point $p$ is an arbitrary element of $\mathbf{R}^{2}$ (note
that $\sigma_{b}$ is applied last). Hutchinson showed in [14] that the self-
similar set corresponding to a given family of contraction operators is
precisely the collection of points obtained in the manner just described. The
limit of the sequence in (1) does not depend on the initial point $p$ because
$\sigma_{a},\sigma_{b},\sigma_{c}$ are contractions. Much like digit
expansions to real numbers, every stream of $a$’s, $b$’s, and $c$’s
corresponds to a unique point in the Sierpiński gasket. The point
$(1/4,\sqrt{3}/4)$, for example, corresponds to the stream $(b,a,a,a,\dots)$
ending in an infinite sequence of $a$’s. Conversely, every point in the
Sierpiński gasket comes from (in general more than one) corresponding stream.

From a computer science perspective, the languages of streams considered by
Hutchinson are the _traces_ observed by one-state labelled transition systems,
like the one in Figure 1. We investigate whether one could achieve a similar
effect with languages of streams obtained from labelled transition systems
having more than one state. Observe, for example, Figure 2. This twisted
version of the Sierpiński gasket is constructed from a two-state labelled
transition system. Each point in the twisted Sierpiński gasket corresponds to
a stream of $a$’s, $b$’s, and $c$’s, but not every stream corresponds to a
point in the set: The limit corresponding to $(c,a,b,c,c,c,\dots)$ is
$(3/4,\sqrt{3}/8)$, for example.

$\begin{gathered}\leavevmode\hbox to109.84pt{\vbox to41.37pt{\pgfpicture\makeatletter\hbox{\hskip 40.2353pt\lower-13.67578pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {{}\pgfsys@rect{-12.50002pt}{-12.50002pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.85764pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {{}\pgfsys@rect{44.4055pt}{-12.50002pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{} {{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}} {{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{}{}{}}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{12.70001pt}{7.33017pt}\pgfsys@curveto{23.3402pt}{13.47578pt}{33.56532pt}{13.47578pt}{42.47366pt}{8.33044pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.86594}{-0.50015}{0.50015}{0.86594}{42.47365pt}{8.33046pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.92091pt}{17.41681pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b,c$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{} {{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}} {{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{}{}{}}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{-12.70001pt}{-3.4025pt}\pgfsys@curveto{-33.21121pt}{-8.89923pt}{-33.21121pt}{8.89923pt}{-15.59776pt}{4.17903pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.96593}{-0.25885}{0.25885}{0.96593}{-15.59776pt}{4.17903pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.9023pt}{-2.15277pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{} {{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}} {{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{}{}{}}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{44.2055pt}{-7.33017pt}\pgfsys@curveto{33.56532pt}{-13.47578pt}{23.3402pt}{-13.47578pt}{14.43185pt}{-8.33044pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-0.86594}{0.50015}{-0.50015}{-0.86594}{14.43187pt}{-8.33046pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.92091pt}{-6.46191pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b,c$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\ \\\ \sigma_{a}\begin{bmatrix}r\\\ s\end{bmatrix}=\begin{bmatrix}\frac{1}{2}r+\frac{1}{4}\\\ \frac{1}{2}s+\frac{\sqrt{3}}{4}\end{bmatrix}\qquad\sigma_{b}\begin{bmatrix}r\\\ s\end{bmatrix}=\begin{bmatrix}\frac{r}{2}\\\ \frac{s}{2}\end{bmatrix}\\\ \sigma_{c}\begin{bmatrix}r\\\ s\end{bmatrix}=\begin{bmatrix}\frac{r}{2}+\frac{1}{2}\\\ \frac{s}{2}\end{bmatrix}\end{gathered}$ |
---|---
Figure 2:  A twisted Sierpińksi gasket, depicted in red. In the construction
of this set, $\sigma_{b}$ and $\sigma_{c}$ are applied twice to a single copy
of $\sigma_{a}$ applied to the set. This has the effect of systematically
removing the “top” part of the Sierpiński gasket from its bottom thirds.

A labelled transition system paired with an interpretation of its labels as
contractions on a complete metric space is the same data as a _directed-graph
iterated function system_ (GIFS), a generalization of iterated function
systems introduced by Mauldin and Williams [19]. GIFSs generate their own kind
of self-similar set, and much work has been done to understand the geometric
properties of fractal sets generated by GIFSs [19, 10, 9, 8, 7]. We take this
work in a slightly different direction by presenting a coalgebraic perspective
on GIFSs, seeing each labelled transition system as a “recipe” for
constructing fractal sets.

In analogy with the theory of regular languages, we call the fractals
generated by finite labelled transition systems _regular subfractals_ , and
give a logic for deciding if two labelled transition systems represent the
same recipe under all interpretations of the labels. By identifying points in
the fractal set generated by a labelled transition system with traces observed
by the labelled transition system, it is reasonable to suspect that two
labelled transition systems represent equivalent fractal recipes—i.e., they
represent the same fractal under every interpretation—if and only if they are
trace equivalent. This is the content of Theorem 4.9, which allows us to
connect the theory of fractal sets to mainstream topics in computer science.

Labelled transition systems are a staple of theoretical computer science,
especially in the area of process algebra [1], where a vast array of different
notions of equivalence and axiomatization problems have been studied. We
specifically use a syntax introduced by Milner in [23] to express labelled
transition systems as terms in an expression language with recursion. This
leads us to a fragment of Milner’s calculus consisting of just the terms that
constitute recipes for fractal constructions. Using a logic of Rabinovich [26]
for deciding trace equivalence in Milner’s calculus, we obtain a complete
axiomatization of fractal recipe equivalence.

In his study of self-similar sets, Hutchinson also makes use of probability
measures supported on self-similar sets, called _invariant measures_. Each
invariant measure is specified by a probability distribution on the set of
contractions generating its support. In the last technical section of the
paper, we adapt the construction of invariant measures to a probabilistic
version of labelled transition systems called _labelled Markov chains_ , which
allows us to give a measure-theoretic semantics to terms in a probabilistic
version of Milner’s specification language, the calculus introduced by Stark
and Smolka [28]. Our measure-theoretic semantics of probabilistic process
terms can be seen as a generalization of the trace measure semantics of
Kerstan and König [15]. We offer a sound axiomatization of equivalence under
this semantics and pose completeness as an open problem.

In sum, the contributions of this paper are as follows.

  * •

In Section 3, we give a fractal recipe semantics to process terms using a
generalization of iterated function systems.

  * •

In Section 4, we show that two process terms agree on all fractal
interpretations if and only if they are trace equivalent. This implies that
fractal recipe equivalence is decidable for process terms, and it allows us to
derive a complete axiomatization of fractal recipe equivalence from
Rabinovich’s axiomatization [26] of trace equivalence of process terms.

  * •

Finally, we adapt the fractal semantics of process terms to the probabilistic
setting in Section 5 and propose an axiomatization of probabilistic fractal
recipe equivalence.

We start with a brief overview of trace semantics in process algebra and
Rabinovich’s Theorem (Theorem 2.5) in Section 2.

##  2 Labelled Transition Systems and Trace Semantics

Labelled transition systems are a widely used model of nondeterminism. Given a
fixed finite set $A$ of _action labels_ , a _labelled transition system_ (LTS)
is a pair $(X,\alpha)$ consisting of a set $X$ of _states_ and a _transition
function_ $\alpha:X\to\mathcal{P}(A\times X)$. We generally write
$x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}_{\alpha}y$ if
$(a,y)\in\alpha(x)$, or simply
$x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y$ if $\alpha$ is clear from
context, and say that _$x$ emits $a$ and transitions to $y$_.

Given a state $x$ of an LTS $(X,\alpha)$, we write $\langle x\rangle_{\alpha}$
for the LTS obtained by restricting the relations
$\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}$ to the set of states
_reachable_ from $x$, meaning there exists a _path_ of the form
$x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a_{1}}$}}x_{1}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{}$}}\cdots\mathrel{\raisebox{-1.0pt}{$\xrightarrow{}$}}x_{n-1}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a_{n}}$}}x_{n}$.
We refer to $\langle x\rangle_{\alpha}$ as either the LTS _generated by $x$_,
or as the _process starting at $x$_. An LTS $(X,\alpha)$ is _locally finite_
if $\langle x\rangle_{\alpha}$ is finite for all states $x$.

### Traces

In the context of the current work, nondeterminism occurs when a process
branches into multiple threads that execute in parallel. Under this
interpretation, to an outside observer (without direct access to the
implementation details of an LTS), two processes that emit the same set of
sequences of action labels are indistinguishable.

Formally, let $A^{*}$ be the set of words formed from the alphabet $A$. Given
a state $x$ of an LTS $(X,\alpha)$, the set $\operatorname{tr}_{\alpha}(x)$ of
_traces emitted by $x$_ is the set of words $a_{1}\dots a_{n}\in A^{*}$ such
that there is a path of the form
$x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a_{1}}$}}x_{1}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{}$}}\cdots\mathrel{\raisebox{-1.0pt}{$\xrightarrow{}$}}x_{n-1}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a_{n}}$}}x_{n}$
through $(X,\alpha)$. Two states $x$ and $y$ are called _trace equivalent_ if
$\operatorname{tr}(x)=\operatorname{tr}(y)$. Each trace language
$\operatorname{tr}(x)$ is _prefix-closed_ , which for a language $L$ means
that $w\in L$ whenever $wa\in L$.

Trace equivalence is a well-documented notion of equivalence for processes
[12, 3], and we shall see it in our work on fractals as well.

######  Definition 2.1.

A _stream_ is an infinite sequence $(a_{1},a_{2},\dots)$ of letters from $A$.
A state $x$ in an LTS $(X,\alpha)$ _emits_ a stream $(a_{1},\dots)$ if for any
$n>0$, $a_{1}\cdots a_{n}\in\operatorname{tr}(x)$. We write
$\operatorname{str}(x)$ for the set of streams emitted by $x$.

In our construction of fractals from LTSs, points are represented only by
(infinite) streams. We therefore focus primarily on LTSs with the property
that for all states $x$, $\operatorname{tr}(x)$ is precisely the set of finite
prefixes of streams emitted by $x$. We refer to an LTS $(X,\alpha)$ satisfying
this condition as _productive_. Productivity is equivalent to the absence of
_deadlock_ states, states with no outgoing transitions.

######  Lemma 2.2.

Let $(X,\alpha)$ be an LTS. Then the following are equivalent: (i) for any
$x,y\in X$, $\operatorname{str}(x)=\operatorname{str}(y)$ if and only if
$\operatorname{tr}(x)=\operatorname{tr}(y)$, and (ii) for any $x\in X$,
$\alpha(x)\neq\emptyset$.

### Specification

We use the following language for specifying processes: Starting with a fixed
countably infinite set $\\{v_{1},v_{2},\dots\\}$ of _variables_ , the set of
_terms_ is given by the grammar

$v\mid ae\mid e_{1}+e_{2}\mid\mu v\leavevmode\nobreak\ e$

where $v$ is $v_{i}$ for some $i\in\mathbb{N}$, $a\in A$, and $e,e_{1},e_{2}$
are terms.

Intuitively, the process $ae$ emits $a$ and then turns into $e$, and
$e_{1}+e_{2}$ is the process that nondeterministically branches into $e_{1}$
and $e_{2}$. The process $\mu v\leavevmode\nobreak\ e$ is like $e$, but with
instances of $v$ that appear free in $e$ acting like goto expressions that
return the process to $\mu v\leavevmode\nobreak\ e$.

######  Definition 1.

A _(process) term_ is a term $e$ in which every occurrence of a variable $v$
appears both within the scope of a $\mu v\leavevmode\nobreak\ (-)$ ($e$ is
_closed_) and within the scope of an $a(-)$ ($e$ is _guarded_). The set of
process terms is written $\mathsf{Term}$. The set of process terms themselves
form the LTS $(\mathsf{Term},\gamma)$ defined in Figure 3.

ae $\xrightarrow{a}$ e e_1 $\xrightarrow{a}$ fe_1 + e_2 $\xrightarrow{a}$ f
e_2 $\xrightarrow{a}$ fe_1 + e_2 $\xrightarrow{a}$ f e[μv e/x]
$\xrightarrow{a}$ fμv e $\xrightarrow{a}$ f

Figure 3:  The relation
${\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}}\subseteq\mathsf{Term}\times\mathsf{Term}$
defining $(\mathsf{Term},\gamma)$.

In Figure 3, we use the notation $e[g/v]$ to denote the expression obtained by
replacing each _free_ occurrence of $v$ in $e$ (one which does not appear
within the scope of a $\mu v\leavevmode\nobreak\ (-)$ operator) with the
expression $g$. Given $e\in\mathsf{Term}$, the process _specified by $e$_ is
the LTS $\langle e\rangle_{\gamma}$.

######  Remark 2.3.

The set of process terms, as we have named them, is the fragment of Milner’s
fixed-point calculus from [23] consisting of only the terms that specify
productive LTSs.

Labelled transition systems specified by process terms are finite and
productive, and conversely, every finite productive process is trace-
equivalent to some process term.

######  Lemma 2.4 ([23, Proposition 5.1]).

For any $e\in\mathsf{Term}$, the set of terms reachable from $e$ in
$(\mathsf{Term},\gamma)$ is finite. Conversely, if $x$ is a state in a finite
productive LTS $(X,\alpha)$, then there is a process term $e$ such that
$\operatorname{tr}(e)=\operatorname{tr}_{\alpha}(x)$.

### Axiomatization of trace equivalence

Given an interpretation of process terms as states in an LTS, and given the
notion of trace equivalence, one might ask if there is an algebraic or proof-
theoretic account of trace equivalence of process terms. Rabinovich showed in
[26] that a complete inference system for trace equivalence can be obtained by
adapting earlier work of Milner [23]. The axioms of the complete inference
system include equations like $e_{1}+e_{2}=e_{2}+e_{1}$ and
$a(e_{1}+e_{2})=ae_{1}+ae_{2}$, which are intuitively true for trace
equivalence.

To be more precise, given any function with domain $\mathsf{Term}$, say
$\sigma:\mathsf{Term}\to Z$, call an equivalence relation $\sim$ _sound with
respect to $\sigma$_ if $e\sim f$ implies $\sigma(e)=\sigma(f)$, and _complete
with respect to $\sigma$_ if $\sigma(e)=\sigma(f)$ implies $e\sim f$. Then the
smallest equivalence relation $\equiv$ on $\mathsf{Term}$ containing all the
pairs derivable from the axioms and inference rules appearing in Figure 4 is
sound and complete with respect to
$\operatorname{tr}=\operatorname{tr}_{\gamma}\colon\mathsf{Term}\to\mathcal{P}(A^{*})$.

######  Definition 2.

Given $e_{1},e_{2}\in\mathsf{Term}$, we say that $e_{1}$ and $e_{2}$ are
_provably equivalent_ if $e_{1}\equiv e_{2}$, and call $\equiv$ _provable
equivalence_.

######  Theorem 2.5 (Rabinovich [26]).

Let $e_{1},e_{2}\in\mathsf{Term}$. Then $e_{1}\equiv e_{2}$ iff
$\operatorname{tr}(e_{1})=\operatorname{tr}(e_{2})$.

$\displaystyle\begin{aligned} (\axiom{ID})\hskip 2.0pt&&e+e&\equiv e\\\
(\axiom{CM})&&e_{2}+e_{1}&\equiv e_{1}+e_{2}\\\ (\axiom{AS})\hskip
1.5pt&&e_{1}+(e_{2}+e_{3})&\equiv(e_{1}+e_{2})+e_{3}\\\ (\axiom{DS})\hskip
1.5pt&&a(e_{1}+e_{2})&\equiv ae_{1}+ae_{2}\\\ (\axiom{FP})\hskip 1.5pt&&\mu
v\leavevmode\nobreak\ e&\equiv e[\mu v\leavevmode\nobreak\
e/v]\end{aligned}\qquad\begin{array}[]{r c}(\axiom{CN})&\infer{(\forall
i)\leavevmode\nobreak\ e_{i}\equiv f_{i}}{g[\vec{e}/\vec{v}]\equiv
g[\vec{f}/\vec{v}]}\\\ (\axiom{AE})&\infer{\ }{\mu w\leavevmode\nobreak\
e\equiv\mu v\leavevmode\nobreak\ e[v/w]}\\\ (\axiom{UA})&\infer{g\equiv
e[g/v]}{g\equiv\mu v\leavevmode\nobreak\ e}\end{array}$ Figure 4:  The axioms
and rules of the provable equivalence relation in addition to those of
equational logic (not shown). Here, $e,e_{i},f,f_{i},g\in\mathsf{Term}$ for
all $i$. In $($, $g$ has precisely the free variables $v_{1},\dots,v_{n}$, and
no variable that appears free in $f_{i}$ is bound in $g$ for any $i$. In $($,
$v$ does not appear free in $e$.

######  Example 2.6.

Consider the processes specified by $e_{1}=\mu w\leavevmode\nobreak\ \mu
v\leavevmode\nobreak\ (a_{1}a_{2}v+a_{1}a_{3}w)$ and $e_{2}=\mu
v\leavevmode\nobreak\ (a_{1}(a_{2}v+a_{3}v))$. The traces emitted by both
$e_{1}$ and $e_{2}$ are those that alternate between $a_{1}$ and either
$a_{2}$ or $a_{3}$. We can show these expressions are trace equivalent via the
formal deduction in Figure 5.

$\begin{aligned}
e_{1}&\stackrel{{\scriptstyle\phantom{\text{($\axiom{FP}$)}}}}{{=}}\mu
w\leavevmode\nobreak\ \mu v\leavevmode\nobreak\ (a_{1}a_{2}v+a_{1}a_{3}w)\\\
&\stackrel{{\scriptstyle\text{($\axiom{FP}$)}}}{{\equiv}}f_{1}\\\
&\stackrel{{\scriptstyle\text{($\axiom{FP}$)}}}{{\equiv}}a_{1}a_{2}e_{1}+a_{1}a_{3}e_{1}\\\
&\stackrel{{\scriptstyle\text{($\axiom{DS}$)}}}{{\equiv}}a_{1}(a_{2}e_{1}+a_{3}e_{1})\\\
&\stackrel{{\scriptstyle\text{($\axiom{UA}$)}}}{{\equiv}}\mu
v\leavevmode\nobreak\
(a_{1}(a_{2}v+a_{3}v))\end{aligned}\quad\begin{gathered}\leavevmode\hbox
to110.68pt{\vbox to82.86pt{\pgfpicture\makeatletter\hbox{\hskip
26.88683pt\lower-69.88152pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-12.50002pt}{-12.50002pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.72813pt}{-1.25055pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$e_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-12.50002pt}{-69.40553pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.77107pt}{-58.15607pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{3}e_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{44.4055pt}{-12.50002pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{48.47644pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{2}f_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{44.4055pt}{-69.40553pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{52.5194pt}{-59.40552pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{7.32765pt}{-12.70001pt}\pgfsys@curveto{13.47075pt}{-23.3402pt}{13.47075pt}{-33.56532pt}{8.32764pt}{-42.47348pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.5}{-0.86603}{0.86603}{-0.5}{8.32764pt}{-42.47348pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.46794pt}{-29.70328pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{12.70001pt}{0.0pt}\pgfsys@lineto{42.20554pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{42.20554pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.40982pt}{5.33745pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{-7.32765pt}{-44.2055pt}\pgfsys@curveto{-13.47075pt}{-33.56532pt}{-13.47075pt}{-23.3402pt}{-8.32764pt}{-14.43204pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.5}{0.86603}{-0.86603}{0.5}{-8.32764pt}{-14.43204pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.55382pt}{-29.70328pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{64.23317pt}{-12.70001pt}\pgfsys@curveto{70.37627pt}{-23.3402pt}{70.37627pt}{-33.56532pt}{65.23315pt}{-42.47348pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.5}{-0.86603}{0.86603}{-0.5}{65.23315pt}{-42.47348pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{72.37346pt}{-29.70328pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{49.57787pt}{-44.2055pt}\pgfsys@curveto{43.43477pt}{-33.56532pt}{43.43477pt}{-23.3402pt}{48.57788pt}{-14.43204pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.5}{0.86603}{-0.86603}{0.5}{48.57788pt}{-14.43204pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.35164pt}{-29.70328pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{44.2055pt}{-56.90552pt}\pgfsys@lineto{14.69998pt}{-56.90552pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{14.69998pt}{-56.90552pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.40982pt}{-64.74406pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qquad\leavevmode\hbox
to66.3pt{\vbox to82.31pt{\pgfpicture\makeatletter\hbox{\hskip
39.41713pt\lower-69.60553pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-12.50002pt}{-12.50002pt}{25.00003pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.72813pt}{-1.25055pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$e_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}
{{}\pgfsys@rect{-23.87515pt}{-69.40553pt}{47.7503pt}{25.00003pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-20.54214pt}{-58.91995pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$a_{2}e_{2}+a_{3}e_{2}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{7.32765pt}{-12.70001pt}\pgfsys@curveto{13.47075pt}{-23.3402pt}{13.47075pt}{-33.56532pt}{8.32764pt}{-42.47348pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.5}{-0.86603}{0.86603}{-0.5}{8.32764pt}{-42.47348pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.46794pt}{-29.70328pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{ {}{}{}}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}}
}{{{{}}{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}{}{}{}{{}}\pgfsys@moveto{-7.32765pt}{-44.2055pt}\pgfsys@curveto{-13.47075pt}{-33.56532pt}{-13.47075pt}{-23.3402pt}{-8.32764pt}{-14.43204pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.5}{0.86603}{-0.86603}{0.5}{-8.32764pt}{-14.43204pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.08412pt}{-29.63329pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{2},a_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\end{gathered}$
Figure 5:  Deducing $e_{1}\equiv e_{2}$. Above, $f_{1}=\mu
v\leavevmode\nobreak\ (a_{1}a_{2}v+a_{1}a_{3}e_{1})$.

Rabinovich’s theorem tells us that, up to provable equivalence, our
specification language consisting of process terms is really a specification
language for languages of traces. In what follows, we are going to give an
alternative semantics to process terms by using LTSs to generate fractal
subsets of metric spaces. The main result of our paper is that these two
semantics coincide: Two process terms are trace equivalent if and only if they
generate the same fractals. This is the content of Sections 3 and 4 below.

##  3 Fractals from Labelled Transition Systems

In the Sierpiński gasket $\mathbf{S}$ from Figure 1, every point of
$\mathbf{S}$ corresponds to a stream of letters from the alphabet
$\\{a,b,c\\}$, and every stream corresponds to a unique point. To obtain the
point corresponding to a particular stream $(a_{1},a_{2},a_{3},\dots)$ with
each $a_{i}\in\\{a,b,c\\}$, start with any $p\in\mathbb{R}^{2}$ and compute
the limit $\lim_{n\in\mathbb{N}}\sigma_{a_{1}}\cdots\sigma_{a_{n}}(p)$. The
point in the fractal corresponding to $(a_{1},a_{2},a_{3},\dots)$ does not
depend on $p$ because $\sigma_{a},\sigma_{b},\sigma_{c}$ in Figure 1 are
_contraction operators_.

######  Definition 20.

Given a metric space $(M,d)$, a _contraction operator_ on $(M,d)$ is a
function $h:M\to M$ such that for some $r\in[0,1)$, $d(h(x),h(y))\leq
r\leavevmode\nobreak\ d(x,y)$ for any $x,y\in M$. The number $r$ is called a
_contraction coefficient_ of $h$. The set of contraction operators on $(M,d)$
is written $\operatorname{Con}(M,d)$.

For example, with the Sierpiński gasket (Figure 1) associated to the
contractions $\sigma_{a}$, $\sigma_{b}$, and $\sigma_{c}$, $r=1/2$ is a
contraction coefficient for all three maps. Now, given $p,q\in\mathbb{R}^{2}$,

$d(\sigma_{a_{1}}\cdots\sigma_{a_{n}}(p),\sigma_{a_{1}}\cdots\sigma_{a_{n}}(q))\leq\frac{1}{2^{n}}\leavevmode\nobreak\
d(p,q)$

for all $n$, so it follows that
$\lim_{n\in\mathbb{N}}\sigma_{a_{1}}\cdots\sigma_{a_{n}}(p)=\lim_{n\in\mathbb{N}}\sigma_{a_{1}}\cdots\sigma_{a_{n}}(q)$.
For any finite set of contraction operators
$\\{\sigma_{a_{1}},\dots,\sigma_{a_{n}}\\}$ indexed by $A$ and acting on a
complete metric space $(M,d)$, every stream from $A$ corresponds to a unique
point in $M$.

######  Definition 21.

A _contraction operator interpretation_ is a function
$\sigma:A\to\operatorname{Con}(M,d)$. We usually write $\sigma_{a}=\sigma(a)$.
Given $\sigma\colon A\to\operatorname{Con}(M,d)$ and a stream $(a_{1},\dots)$
from $A$, define

$\sigma_{\omega}\colon A^{\omega}\to
M\qquad\sigma_{\omega}(a_{1},\dots)=\lim_{n\in\mathbb{N}}\sigma_{a_{1}}\cdots\sigma_{a_{n}}(x)$
(2)

where $x\in M$ is arbitrary. The _self-similar set_ corresponding to a
contraction operator interpretation $\sigma$ is the set
$\mathbf{S}_{\sigma}=\\{\sigma_{\omega}(a_{1},\dots)\mid(a_{1},\dots)\text{ is
a stream from }A\\}$.

######  Remark 3.1.

Note that in (2), the contraction operators corresponding to the initial trace
$(a_{1},\dots,a_{n})$ are applied in _reverse_ order. That is,
$\sigma_{a_{n}}$ is applied before $\sigma_{a_{n-1}}$, $\sigma_{a_{n-2}}$ is
applied before $\sigma_{a_{n-1}}$, and so on.

### Regular Subfractals

Generalizing the fractals of Mandelbrot [18], Hutchinson introduced self-
similar sets in [14] and gave a comprehensive account of their theory. In op.
cit., Hutchinson defines a self-similar set to be the invariant set of an
_iterated function system_. In our terminology, an iterated function system is
equivalent to a contraction operator interpretation of a finite set $A$ of
actions, and the invariant set is the total set of points obtained from
streams from $A$. The fractals constructed from a LTS paired with a
contraction operator interpretation generalize Hutchinson’s self-similar sets
to nonempty compact sets of points obtained from certain subsets of the
streams, namely the subsets emitted by the LTS.

Write $\operatorname{\textbf{K}}(M,d)$ for the set of nonempty compact subsets
of $(M,d)$. Given a state $x$ of a productive LTS $(X,\alpha)$ and a
contraction operator interpretation $\sigma:A\to\operatorname{Con}(M,d)$, we
define $\left\llbracket{-}\right\rrbracket_{\alpha,\sigma}\colon
X\to\operatorname{\textbf{K}}(M,d)$ by

$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}=\left\\{\sigma_{\omega}(a_{1},\dots)\mid\text{$(a_{1},\dots)$
emitted by $x$}\right\\}$ (3)

and call this the set _generated by the state $x$_ or the _$x$ -component of
the solution_. As we will see,
$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ is always nonempty and
compact.

######  Definition 22.

Given a process term $e\in\mathsf{Term}$ and a contraction operator
interpretation $\sigma:A\to\operatorname{Con}(M,d)$, the _regular subfractal
semantics of $e$_ corresponding to $\sigma$ is
$\left\llbracket{e}\right\rrbracket_{\sigma}=\left\llbracket{e}\right\rrbracket_{\gamma,\sigma}$.

For example, the set of points depicted in Figure 2 is the regular subfractal
semantics of $\mu v\leavevmode\nobreak\ (av+b(bv+cv)+c(bv+cv))$ corresponding
to the interpretation $\sigma$ given in that figure. The regular subfractal
semantics of $e$ is a proper subset of the Sierpiński Gasket, and in
particular does not contain the point corresponding to $(c,a,b,c,c,c,\dots)$.

### Systems and Solutions

Self-similar sets are often characterized as the unique nonempty compact sets
that solve systems of equations of the form

$K=\sigma_{1}(K)\cup\cdots\cup\sigma_{n}(K)$

with each $\sigma_{i}$ a contraction operator on a complete metric space. For
example, the Sierpiński gasket is the unique nonempty compact solution to
$K=\sigma_{a}(K)\cup\sigma_{b}(K)\cup\sigma_{c}(K)$. In this section, we are
going to provide a similar characterization for regular subfractals that will
play an important role in the completeness proof in Section 4.

One way to think of an $n$-state LTS $(X,\alpha)$ is as a system of formal
equations

$x_{i}=a_{k_{1}}x_{j_{1}}+\cdots+a_{k_{m}}x_{j_{m}}$

indexed by $X=\\{x_{1},\dots,x_{n}\\}$, where
$x_{i}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a_{k_{l}}}$}}_{\alpha}x_{j_{l}}$
for $k_{1},\dots,k_{m},j_{1},\dots,j_{l}\leq n$.

######  Definition 23.

Given a contraction operator interpretation
$\sigma:A\to\operatorname{Con}(M,d)$, and an LTS $(X,\alpha)$, we call a
function $\varphi:X\to\operatorname{\textbf{K}}(M,d)$ a _( $\sigma$-)solution_
to $(X,\alpha)$ if for any $x\in X$,

$\varphi(x)=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(\varphi(y))$

######  Example 3.2.

Let $\mathbf{S}$ be the Sierpiński gasket as a subset of $\mathbb{R}^{2}$. Let
$(X,\alpha)$ be the LTS in Figure 1. Then we have a single state, $x$, with
$x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a,b,c}$}}x$. The function
$\varphi\colon X\to\operatorname{\textbf{K}}(\mathbb{R}^{2},d)$ given by
$\varphi(s)=\mathbf{S}$ is a solution to $(X,\alpha)$, because
$\mathbf{S}=\sigma_{a}(\mathbf{S})\cup\sigma_{b}(\mathbf{S})\cup\sigma_{c}(\mathbf{S})$.

Finite productive LTSs have unique solutions.

######  Lemma 3.3.

Let $(M,d)$ be a complete metric space, $\sigma:A\to\operatorname{Con}(M,d)$,
and $(X,\alpha)$ be a finite productive LTS. Then $(X,\alpha)$ has a unique
solution $\varphi_{\alpha}$.

The proof of Lemma 3.3 makes use of the _Hausdorff metric_ on
$\operatorname{\textbf{K}}(M,d)$, defined

$d(K_{1},K_{2})=\max\left\\{\sup_{u\in K_{1}}\inf_{v\in
K_{2}}d(u,v),\sup_{v\in K_{2}}\inf_{u\in K_{1}}d(u,v)\right\\}$ (4)

This equips $\operatorname{\textbf{K}}(M,d)$ with the structure of a metric
space. If $M$ is complete, so is $\operatorname{\textbf{K}}(M,d)$.
Incidentally, we need to restrict to _nonempty_ sets in (4). This is the
primary motivation for the guardedness condition which we imposed on our
terms. We also recall the _Banach fixed-point theorem_ , which allows for the
computation of fixed-points by iteration.

######  Theorem 3.4 (Banach [2]).

Let $(M,d)$ be a complete nonempty metric space and $f\colon M\to M$ a
contraction map. Then $\lim_{n\in\mathbb{N}}f^{n}(q)$ is the unique fixed-
point of $f$.

Fix a complete nonempty metric space $(M,d)$, a productive finite LTS
$(X,\alpha)$, and a contraction operator interpretation
$\sigma:A\to\operatorname{Con}(M,d)$. To compute the solution to $(X,\alpha)$,
we iteratively apply a matrix-like operator to the set
$\operatorname{\textbf{K}}(M,d)^{X}$ of vectors $[K_{x_{1}},\dots,K_{x_{n}}]$
with entries in $\operatorname{\textbf{K}}(M,d)$ indexed by $X$. Formally, we
define

${\left[\alpha\right]_{\sigma}}\colon\operatorname{\textbf{K}}(M,d)^{X}\to\operatorname{\textbf{K}}(M,d)^{X}\qquad({\left[\alpha\right]_{\sigma}}\vec{K})_{x}=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(K_{y})$

for each $x\in X$. Intuitively, ${\left[\alpha\right]_{\sigma}}$ acts like an
$X\times X$-matrix of unions of contractions.

######  Proof 3.5 (Proof of Lemma 3.3.).

Every fixed-point of ${\left[\alpha\right]_{\sigma}}$ corresponds to a
solution of $(X,\alpha)$. Given a fixed-point $\vec{F}$, i.e.,
${\left[\alpha\right]_{\sigma}}\vec{F}=\vec{F}$, and defining $\varphi\colon
X\to\operatorname{\textbf{K}}(M,d)^{X}$ by $\varphi(x)=F_{x}$, we see that

$\varphi(x)=F_{x}=({\left[\alpha\right]_{\sigma}}\vec{F})_{x}=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(F_{y})=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(\varphi(y))$

Conversely, if $\varphi:X\to\operatorname{\textbf{K}}(M,d)$ is a solution to
$(X,\alpha)$, then defining $F_{x}=\varphi(x)$ we have

$F_{x}=\varphi(x)=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(\varphi(y))=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(F_{y})=({\left[\alpha\right]_{\sigma}}\vec{F})_{x}$

for each $x\in X$. Thus, it suffices to show that
${\left[\alpha\right]_{\sigma}}$ has a unique fixed-point. By the Banach
Fixed-Point Theorem, we just need to show that
${\left[\alpha\right]_{\sigma}}$ is a contraction operator. That is,
${\left[\alpha\right]_{\sigma}}\in\operatorname{Con}(\operatorname{\textbf{K}}(M),d)$,
where $d$ is the Hausdorff metric. This point is standard in the fractals
literature; cf. [14].

### Fractal Semantics and Solutions

Recall that the fractal semantics of a process term $e$ with respect to a
contraction operator interpretation $\sigma\colon A\to\operatorname{Con}(M,d)$
is the set $\left\llbracket{e}\right\rrbracket_{\sigma}$ of limits of streams
applied to points in the complete metric space $(M,d)$.

######  Theorem 3.6.

Let $(X,\alpha)$ be a finite productive LTS and let $x\in X$. Given
$e\in\mathsf{Term}$, a complete metric space $(M,d)$, and $\sigma\colon
A\to\operatorname{Con}(M,d)$,

  1. 1.

$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}\in\operatorname{\textbf{K}}(M,d)$,
i.e., $\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ is nonempty and
compact.

  2. 2.

$\left\llbracket{-}\right\rrbracket_{\alpha,\sigma}\colon
X\to\operatorname{\textbf{K}}(M,d)$ is the unique solution to $(X,\alpha)$.

######  Proof 3.7.

To see _1._ , let $A^{\omega}$ be the set of streams from $A$ and define the
metric space $(A^{\omega},d)$ by

$d((a_{1},\dots),(b_{1},\dots))=\prod_{i=1}^{n}c_{a_{i}}$

if $n+1$ is the first index at which $a_{i}\neq b_{i}$ and $c_{a_{i}}$ is a
given nonzero contraction coefficient of $\sigma_{a_{i}}$. Since $A$ is
finite, the space $(A^{\omega},d)$ is a compact metric space111It is the
Cantor set on $A$-many symbols., within which $\operatorname{str}(e)$ is
compact. The function $\sigma^{\omega}\colon A^{\omega}\to M$ is continuous
(in fact, $D$-Lipschitz where $D$ is the diameter of $\mathbf{S}_{\sigma}$),
so $\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ is the continuous
image of a compact set and is therefore compact.

For _2._ , it suffices to see that
$\left\llbracket{-}\right\rrbracket_{\alpha,\sigma}$ is a solution to
$(X,\alpha)$, since $(X,\alpha)$ is finite and thus has a unique solution by
Lemma 3.3. Given $x\in X$, let
$p\in\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ and suppose
$p=\sigma^{\omega}(a_{1},a_{2},\dots)$ for some stream $(a_{1},a_{2},\dots)$
emitted by $x$. Then for some $y\in X$,
$x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a_{1}}$}}y$ and $y$ emits
$(a_{2},\dots)$. If $q=\sigma^{\omega}(a_{2},\dots)$, then
$q\in\left\llbracket{y}\right\rrbracket_{\alpha,\sigma}$ and by continuity of
$\sigma_{a_{1}}$, $p=\sigma_{a}(q)$. It follows that
$p\in\sigma_{a}(\left\llbracket{y}\right\rrbracket_{\alpha,\sigma})$.
Conversely, if $x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y$, and
$q\in\left\llbracket{f}\right\rrbracket$, let $q=\sigma_{\omega}(a_{1},\dots)$
for some trace $(a_{1},\dots)\in\operatorname{str}(y)$. Then
$(a,a_{1},\dots)\in\operatorname{str}(x)$, so
$\sigma_{a}(q)\in\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$. Since
$a,a_{1}$ and $y$ were arbitrary,

$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(\left\llbracket{y}\right\rrbracket_{\sigma})$

In particular, $(\mathsf{Term},\gamma)$ is locally finite, and so by Lemma 3.3
has a unique solution. Theorem 3.6 therefore implies that this solution is
$\left\llbracket{-}\right\rrbracket_{\sigma}$.

We obtain the following, which can be seen as an analogue of Kleene’s theorem
for regular expressions [16], as a direct consequence of Theorem 3.6.

######  Theorem 3.8.

A subset of a self-similar set is a regular subfractal if and only if it is a
component of a solution to a finite productive LTS.

##  4 Fractal Equivalence is Traced

We have seen that finite productive LTSs (LTSs that only emit infinite
streams) can be specified by process terms. We also introduced a family of
fractal sets called regular subfractals, those subsets of self-similar sets
obtained from the streams emitted by a finite productive LTS. An LTS itself is
representative of a certain system of equations, and set-wise the system of
equations is solved by the regular subfractals corresponding to it. Going from
process terms to LTSs to regular subfractals, we see that a process term is
representative of a sort of _uninterpreted fractal recipe_ , which tells us
how to obtain a regular subfractal from an interpretation of action symbols as
contractions on a complete metric space.

######  Definition 4.1.

Given $e,f\in\mathsf{Term}$, we write $e\approx f$ if for every complete
metric space $(M,d)$ and every contraction operator interpretation
$\sigma:A\to\operatorname{Con}(M,d)$,
$\left\llbracket{e}\right\rrbracket_{\sigma}=\left\llbracket{f}\right\rrbracket_{\sigma}$.
We say that $e$ and $f$ are _fractal equivalent_ or that they are _equivalent
fractal recipes_.

######  Theorem 4.2.

Let $e,f\in\mathsf{Term}$. Then $e\approx f$ if and only if
$\operatorname{str}(e)=\operatorname{str}(f)$.

In essence, this is a soundness/completeness theorem for our version of
Rabinovich’s logic with respect to its fractal semantics that we presented.
Our proof relies on the logical characterization of trace equivalence that we
saw in Theorem 2.5.

######  Lemma 4.3 (Soundness).

For any $e,f\in\mathsf{Term}$, if $e\equiv f$, then $e\approx f$.

Our proof essentially consists of two parts. First, we observe that LTS
homomorphisms (coalgebra homomorphisms) preserve fractal equivalence.

######  Lemma 4.4.

Let $(M,d)$ be a complete metric space and
$\sigma:A\to\operatorname{Con}(M,d)$ be a contraction operator interpretation.
Let $(X,\alpha)$ and $(Y,\beta)$ be productive LTSs, let their solutions be
$\varphi_{\alpha}$ and $\varphi_{\beta}$, and let
$f\colon(X,\alpha)\to(Y,\beta)$ be a morphism. Then
$\varphi_{\alpha}=\varphi_{\beta}\circ f$.

######  Proof 4.5.

Recall the notation $\operatorname{str}(x)$ and $\operatorname{tr}{x}$ and
Lemma 2.2. In the notation of this result, it is easy to see that
$\operatorname{tr}(x)=\operatorname{tr}(f(x))$ for all $x\in X$. Thus,
$\operatorname{str}(x)=\operatorname{str}(f(x))$. Now this preservation result
follows from the definition of
$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ in (3) and Theorem 3.6.

This is a step towards soundness because it connects to known process theory
literature: Two states of an LTS are said to be _bisimilar_ if they are
identified by an LTS homomorphism, and _bisimilarity_ is the equivalence
relation consisting of all pairs of bisimilar states [3]. It was shown by
Milner in [23] that all but (DS) from our axiom set in Figure 4 are sound
equivalences with respect to bisimilarity. This concludes the first step of
soundness.

The second step is a near-direct consequence of a basic fact about function
images: Under a function, the image of a union is the union of its images.

######  Lemma 4.6.

Let $e,f\in\mathsf{Term}$ and $a\in A$. For any contraction operator
interpretation $\sigma:A\to\operatorname{Con}(M,d)$, and any $a\in A$,

$\displaystyle\left\llbracket{e+f}\right\rrbracket_{\sigma}$
$\displaystyle=\left\llbracket{e}\right\rrbracket_{\sigma}\cup\left\llbracket{f}\right\rrbracket_{\sigma}$
(5) $\displaystyle\left\llbracket{ae}\right\rrbracket_{\sigma}$
$\displaystyle=\sigma_{a}(\left\llbracket{e}\right\rrbracket_{\sigma})$ (6)

######  Proof 4.7.

Applying Lemma 2.2 to the LTS $\mathsf{Term}$, we see that for all process
terms $e$ and $f$, $\operatorname{str}(e)=\operatorname{str}(f)$ if and only
if $\operatorname{tr}(e)=\operatorname{tr}(f)$. Now the structure of
$\mathsf{Term}$ as an LTS implies that
$\operatorname{str}(e+f)=\operatorname{str}(e)\cup\operatorname{str}(f)$.
Equation 5 follows easily from this. We argue similarly for (6):
$\operatorname{str}(ae)$ is exactly the set $\operatorname{str}(e)$ with all
streams in it prefixed by $a$. To see that
$\left\llbracket{ae}\right\rrbracket_{\sigma}\subseteq\sigma_{a}(\left\llbracket{e}\right\rrbracket_{\sigma})$,
let $p\in\left\llbracket{ae}\right\rrbracket_{\sigma}$. There is a stream
$(a,a_{1},\dots)\in\operatorname{str}(e)$ such that
$p=\lim_{n\in\mathbb{N}}\sigma_{a}\sigma_{a_{1}}\dots\sigma_{a_{n}}(q)$ (for
arbitrary $q\in M$). Since $\sigma_{a}$ is continuous,
$p=\sigma_{a}\left(\lim_{n\in\mathbb{N}}\sigma_{a_{1}}\dots\sigma_{a_{n}}(q)\right)$,
so $p\in\sigma_{a}(\left\llbracket{e}\right\rrbracket_{\sigma})$. The converse
is similar.

######  Proof 4.8 (Proof of Lemma 4.3.).

By induction on derivations using the axioms in Figure 4 together with the
rules of equational logic. Milner’s work in [23] covers all of the axioms
except for the distributivity axiom (DS), so it suffices to check that (DS) is
sound with respect to fractal equivalence and that fractal equivalence is a
congruence.

Fix an interpretation $\sigma:A\to\operatorname{Con}(M,d)$. Using Lemma 4.6,
we have

$\left\llbracket{a(e+f)}\right\rrbracket=\sigma_{a}\left\llbracket{e+f}\right\rrbracket=\sigma_{a}(\left\llbracket{e}\right\rrbracket\cup\left\llbracket{f}\right\rrbracket)={\left[a\right]_{\sigma}}\left\llbracket{e}\right\rrbracket\cup{\left[a\right]_{\sigma}}\left\llbracket{f}\right\rrbracket=\left\llbracket{ae}\right\rrbracket\cup\left\llbracket{af}\right\rrbracket=\left\llbracket{ae+af}\right\rrbracket$

This establishes the soundness of (DS). Lastly, we need to check that fractal
equivalence is a congruence, meaning that it is preserved by the algebraic
operations. More precisely, if $e_{i}\approx f_{i}$ for $i\leq n$ and $g$ is a
term with free variables $v_{1},\dots,v_{n}$, then

$g[\vec{e}/\vec{v}]\approx g[\vec{f}/\vec{v}]$ (7)

We proceed by induction on $g$.

  1. 1.

If $g=v_{1}\in V$, then $g[e_{1}/v_{1}]=e_{1}\approx f_{1}=g[f_{1}/v_{1}]$.

  2. 2.

If $g=ag^{\prime}$ and (7) is true of $g^{\prime}$, then by Lemma 4.6,

$\displaystyle\left\llbracket{g[\vec{e}/\vec{v}]}\right\rrbracket=\left\llbracket{ag^{\prime}[\vec{e}/\vec{v}]}\right\rrbracket=\sigma_{a}\left\llbracket{g^{\prime}[\vec{e}/\vec{v}]}\right\rrbracket=\sigma_{a}\left\llbracket{g^{\prime}[\vec{f}/\vec{v}]}\right\rrbracket=\left\llbracket{g[\vec{f}/\vec{v}]}\right\rrbracket$

  3. 3.

If $g=g_{1}+g_{2}$ and (7) holds for $g_{1},g_{2}$, then again use Lemma 4.6.

  4. 4.

If $g=\mu w\leavevmode\nobreak\ g^{\prime}$, it suffices to consider the case
where $w\neq v_{i}$ for any $i\leq n$. Assume (7) for $g^{\prime}$. Then by
soundness of (FP),

$\displaystyle\left\llbracket{g[\vec{e}/\vec{v}]}\right\rrbracket$
$\displaystyle=\left\llbracket{\mu w\leavevmode\nobreak\
g^{\prime}[\vec{e}/\vec{v}]}\right\rrbracket$
$\displaystyle=\left\llbracket{g^{\prime}[\vec{e}/\vec{v},\mu
w\leavevmode\nobreak\ g^{\prime}[\vec{e}/\vec{v}]/w]}\right\rrbracket$
$\displaystyle=\left\llbracket{g^{\prime}[\vec{f}/\vec{v},\mu
w\leavevmode\nobreak\ g^{\prime}[\vec{e}/\vec{v}]/w]}\right\rrbracket$
$\displaystyle=\left\llbracket{\mu w\leavevmode\nobreak\
g^{\prime}[\vec{f}/\vec{v}]}\right\rrbracket$

The last equation holds by soundness of (UA).

This completes the proof.

######  Theorem 4.9 (Completeness).

For any $e,f\in\mathsf{Term}$,if $e\approx f$, then $e\equiv f$.

######  Proof 4.10.

Consider the space $(A^{\omega},d)$ of streams from $A$ with the metric below:

$d((a_{1},\dots),(b_{1},\dots))=\inf\left\\{2^{-n}\leavevmode\nobreak\
\middle|\leavevmode\nobreak\ (\forall i\leq n)\leavevmode\nobreak\
a_{i}=b_{i}\right\\}$

This space is the _Cantor set on $A$ symbols_, a compact metric space. For any
productive LTS $(X,\alpha)$ and $x\in X$, $\operatorname{str}(x)$ is a
nonempty closed subset of $(A^{\omega},d)$, for the following reason: Given a
Cauchy sequence $\\{(a_{1}^{(i)},\dots)\\}_{i\in\mathbb{N}}$ in
$\operatorname{str}(x)$, let $(a_{1},\dots)$ be its limit in $(A^{\omega},d)$.
Then $x$ emits every finite initial segment of $(a_{1},\dots)$, because for
any $N\in\mathbb{N}$ there is an $m\in\mathbb{N}$ such that
$(a_{1},\dots,a_{m},a_{m+1}^{(m)},\dots)\in\operatorname{str}(x)$ for $m>N$.
By compactness of $(A^{\omega},d)$, we therefore have
$\operatorname{str}(x)\in\operatorname{\textbf{K}}(A^{\omega},d)$, so
$\operatorname{str}\colon X\to\operatorname{\textbf{K}}(A^{\omega},d)$.

For each $a\in A$, let $\sigma_{a}:A^{\omega}\to A^{\omega}$ be the map
$\sigma_{a}(a_{1},\dots)=(a,a_{1},\dots)$. Then
$\sigma:A\to\operatorname{Con}(A^{\omega},d)$. By construction,
$\operatorname{str}(x)=\bigcup_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{a}$}}y}\sigma_{a}(\operatorname{str}(y))$
for any $x\in X$. By the uniqueness of fixed points we saw in Lemma 3.3, we
therefore have
$\operatorname{str}(x)=\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$.

To finish the proof, consider $(\mathsf{Term},\gamma)$. If
$e,f\in\mathsf{Term}$ and $e\approx f$, then in particular,
$\operatorname{str}(e)=\operatorname{str}(f)$, because
$\operatorname{str}=\left\llbracket{-}\right\rrbracket_{\gamma,\sigma}$ with
$\sigma\colon A\to\operatorname{Con}(A^{\omega},d)$ as above. Since
$(\mathsf{Term},\gamma)$ is productive,
$\operatorname{tr}(e)=\operatorname{str}(e)$ and
$\operatorname{tr}(f)=\operatorname{str}(f)$, so in particular, $e$ and $f$
are trace equivalent. By Rabinovich’s Theorem, Theorem 2.5, $e\equiv f$, as
desired.

##  5 A Calculus of Subfractal Measures

Aside from showing the existence of self-similar sets and their correspondence
with contraction operator interpretations (in Hutchinson’s terminology,
iterated function systems), Hutchinson also shows that every probability
distribution on the contractions corresponds to a unique measure, called the
_invariant measure_ , that satisfies a certain recursive equation and whose
support is the self-similar set. In this section, we replay the story up to
this point, but with Hutchinson’s invariant measure construction instead of
the invariant (self-similar) set construction. We make use of a probabilistic
version of LTSs called _labelled Markov chains_ , as well as a probabilistic
version of Milner’s specification language introduced by Stark and Smolka [28]
to specify fractal measures. Similar to how fractal equivalence coincides with
trace equivalence, _fractal measure equivalence_ is equivalent to a
probabilistic version of trace equivalence due to Kerstan and König [15].

### Invariant measures

Recall that a _Borel probability measure_ on a metric space $(M,d)$ is a
$[0,\infty]$-valued function $\rho$ defined on the Borel subsets of $M$ (the
smallest $\sigma$-algebra containing the open balls of $(M,d)$) that is
countably additive and assigns $\rho(\emptyset)=0$ and $\rho(M)=1$.

Hutchinson shows in [14] that, given $\sigma\colon
A\to\operatorname{Con}(M,d)$, each probability distribution $\rho\colon
A\to[0,1]$ on $A$ gives rise to a unique Borel probability measure
$\hat{\rho}$, called the _invariant measure_ , satisfying the equation below
and supported by the self-similar set $\mathbf{S}_{\sigma}$:

$\hat{\rho}(B)=\sum_{a\in A}\rho(a)\leavevmode\nobreak\
\sigma_{a}^{\\#}\hat{\rho}(B)$

Here and elsewhere, the _pushforward measure_ $f^{\\#}\hat{\rho}$ with respect
to a continuous map $f$ is defined by
$f^{\\#}\hat{\rho}(B)=\hat{\rho}(f^{-1}(B))$ for any Borel subset $B$ of
$(M,d)$.

We can view the specification $\rho$ of the invariant measure $\hat{\rho}$ as
a one-state Markov process with a loop labelled with each letter from $A$,
similar to how self-similar sets are specified with a one-state productive
LTS. We can adapt this construction to multiple states by moving from
probability distributions on $A$ to _labelled Markov chains_ , where again,
the labels are interpreted as contraction maps.

### Labelled Markov Chains

Let ${\mathcal{D}}$ denote the finitely supported probability distribution
functor on the category of sets.

######  Definition 5.1.

A _labelled Markov chain_ (LMC) is a pair $(X,\beta)$ consisting of a set $X$
of _states_ and a function $\beta\colon X\to{\mathcal{D}}(A\times X)$. A
_homomorphism_ of LMCs $h\colon(X,\beta_{X})\to(Y,\beta_{Y})$ is a function
$h:X\to Y$ such that ${\mathcal{D}}(h)\circ\beta_{X}=\beta_{Y}\circ h$. We
write $x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid a}$}}_{\beta}y$ if
$\beta(x)(a,y)=r$, often dropping the symbol $\beta$ if it is clear form
context.

As we have already seen, given a contraction operator interpretation
$\sigma\colon A\to\operatorname{Con}(M,d)$, every state $x$ of a productive
LTS $(X,\alpha)$ with labels in $A$ corresponds to a regular subfractal
$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ of $\mathbf{S}_{\sigma}$.
This regular subfractal is defined to be the continuous image of the set
$\operatorname{str}(x)$ under the map
$\sigma_{\omega}\colon(A^{\omega},d_{\sigma})\to(M,d)$, where $d_{\sigma}$ is
determined by the contraction coefficients of the $\sigma_{a}$’s as follows:
Given a nonzero contraction coefficient $c_{a}$ of $\sigma_{a}$ for each $a\in
A$, define $d_{\sigma}((a_{1},\dots),(b_{1},\dots))=\prod_{i=1}^{n}c_{a_{i}}$,
where $n$ is the least index such that $a_{n+1}\neq b_{n+1}$. The family
$\left\llbracket{x}\right\rrbracket_{\alpha,\sigma}$ is characterized by its
satisfaction of the equations representing the LTS $(X,\alpha)$.

Every LMC $(X,\beta)$ has an _underlying_ LTS $(X,\bar{\beta})$, where
$\bar{\beta}(x)=\\{(a,y)\mid\beta(x)(a,y)>0\\}$. For each $x\in X$, we are
going to define a probability measure $\hat{\beta}_{\sigma}(x)$ on
$\mathbf{S}_{\sigma}$ whose support is
$\left\llbracket{x}\right\rrbracket_{\bar{\beta},\sigma}$, and that satisfies
a recursive system of equations represented by the LMC $(X,\beta)$. Roughly,
$\hat{\beta}_{\sigma}(x)$ is the pushforward of a certain Borel probability
measure $\hat{\beta}(x)$ on $A^{\omega}$ that does not depend on the
contraction operator interpretation $\sigma$.

We begin by topologizing $A^{\omega}$, using as a basis the sets of the form

$B_{a_{1}\cdots a_{n}}=\\{(a_{1},\dots,a_{n},b_{1},\dots)\mid(b_{1},\dots)\in
A^{\omega}\\}$

Given a state $x$ of a LMC $(X,\beta)$ and a word $w=a_{1}\cdots a_{n}$, we
follow Kerstan and König [15] and define the _trace measure_ of the basic open
set $B_{w}$ by

$\hat{\beta}(x)(B_{w})=\sum\\{r_{1}\cdots r_{n}\mid
x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r_{1}\mid
a_{1}}$}}x_{1}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{\
}$}}\cdots\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r_{n}\mid
a_{n}}$}}x_{n}\\}$ (8)

where $\hat{\beta}(B_{\epsilon})=\hat{\beta}(A^{\omega})=1$. This defines a
unique Borel probability measure on $(A^{\omega},d)$.

######  Proposition 5.2.

Let $j\colon A^{*}\to[0,1]$ satisfy $j(w)=\sum_{a\in A}j(wa)$ for any $w\in
A^{*}$ and $j(\epsilon)=1$, where $\epsilon$ is the empty word. Then there is
a unique Borel probability measure $\rho$ on $(A^{\omega},d)$ such that for
any $w\in A^{*}$, $\rho(B_{w})=j(w)$.

######  Proof 5.3.

This is an easy consequence of the Identity and Extension Theorems for
$\sigma$-finite premeasures. See Propositions 2.3 to 2.5 of [15].

In particular, given any LMC $(X,\beta)$, $\hat{\beta}(x)(B_{w})=\sum_{a\in
A}\hat{\beta}(x)(B_{wa})$, so there is a unique Borel probability measure
$\hat{\beta}(x)$ on $A^{\omega}$ such that (8) holds for any basic open set
$B_{w}$.

######  Definition 5.4.

Let $(X,\beta)$ be a LMC, and $\sigma\colon A\to\operatorname{Con}(M,d)$ be a
contraction operator interpretation in a complete metric space. For each $x\in
X$, we define the _regular subfractal measure_ corresponding to $x$ to be
$\hat{\beta}_{\sigma}(x)=\sigma_{\omega}^{\\#}\hat{\beta}(x)$.

Intuitively, the regular subfractal measure of a state in a LMC under a
contraction operator interpretation computes the probability that, if run
stochastically according to the probabilities labelling the edges, the
sequence of points of $M$ observed in the run eventually lands within a given
Borel subset of $(M,d)$.

### Systems of Probabilistic Equations

Given a complete metric space $(M,d)$, let $\mathbf{P}(M,d)$ be the set of
Borel probability measures on $(M,d)$. In previous sections, we made use of
the fact that, when $\sigma\colon A\to\operatorname{Con}(M,d)$, we can see
$\operatorname{\textbf{K}}(M,d)$ as a _semilattice with operators_ , i.e.,
union acts as a binary operation
$\cup\colon\operatorname{\textbf{K}}(M,d)^{2}\to\operatorname{\textbf{K}}(M,d)$
and each
$\sigma_{a}\colon\operatorname{\textbf{K}}(M,d)\to\operatorname{\textbf{K}}(M,d)$
distributes over $\cup$. Analogously, equipped with $\sigma\colon
A\to\operatorname{Con}(M,d)$, $\mathbf{P}(M,d)$ is a _convex algebra with
operators_. Formally, for any $r\in[0,1]$, there is a binary operation
$\oplus_{r}\colon\mathbf{P}(M,d)^{2}\to\mathbf{P}(M,d)$ defined
$(\rho_{1}\oplus_{r}\rho_{2})(B)=r\rho_{1}(B)+(1-r)\rho_{2}(B)$, over which
each $\sigma_{a}^{\\#}$ distributes, i.e.,

$\sigma_{a}^{\\#}(\rho_{1}\oplus_{r}\rho_{2})=\sigma_{a}^{\\#}\rho_{1}\oplus_{r}\sigma_{a}^{\\#}\rho_{2}$

We also make use of a summation notation defined by

$r_{1}\cdot\rho_{1}\oplus\cdots\oplus
r_{n}\cdot\rho_{n}=\rho_{n}\oplus_{r_{n}}\left(\frac{r_{1}}{1-r_{n}}\cdot\rho_{i}\oplus\cdots\oplus\frac{r_{n-1}}{1-r_{n}}\cdot\rho_{i}\right)$

for any $r_{1},\dots,r_{n}\in[0,1)$.

Given a contraction operator interpretation, an LMC $(X,\beta)$ can be thought
of as a system of equations with one side a polynomial term in a convex
algebra with operators,

$x_{i}=r_{i1}\cdot a_{i1}x_{k_{1}}\oplus r_{i2}\cdot
a_{i2}x_{k_{2}}\oplus\cdots\oplus r_{im}\cdot a_{im}x_{k_{m}}$

where $X=\\{x_{1},\dots,x_{n}\\}$ and
$x_{i}\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r_{ij}\mid a_{ij}}$}}x_{k_{m}}$
for each $i,j\leq m$.

######  Definition 5.5.

Let $(X,\beta)$ be a LMC, and let $\sigma\colon A\to\operatorname{Con}(M,d)$.
A _solution_ to $(X,\beta)$ is a function $\varphi\colon X\to\mathbf{P}(M,d)$
such that for any $x\in X$ and any Borel set $B$,

$\varphi(x)(B)=\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}r\leavevmode\nobreak\ \sigma_{a}^{\\#}(\varphi(y))(B)$

Every finite LMC admits a unique solution, and moreover, the unique solution
is the regular subfractal measure from Definition 5.4.

######  Theorem 5.6.

Let $(X,\beta)$ be a LMC, $x\in X$, and $\sigma\colon
A\to\operatorname{Con}(M,d)$. Then the map $\hat{\beta}_{\sigma}\colon
X\to\mathbf{P}(M,d)$ is the unique solution to $(X,\beta)$.

######  Proof 5.7.

We begin by showing that $(X,\beta)$ has a unique solution, and end by showing
that $\hat{\beta}_{\sigma}$ is a solution.

To see that $(X,\beta)$ has a unique solution, we show that every solution is
the fixed point of a contraction operator on the $X$-fold product of the
complete metric space $(\mathbf{P}(M,d),L)$, where $L$ is the _Kantorovich
metric_ [11]

$L(\rho,\theta)=\sup\left\\{\int_{M}\varphi\leavevmode\nobreak\
d\rho-\int_{M}\varphi\leavevmode\nobreak\ d\theta\leavevmode\nobreak\
\middle|\leavevmode\nobreak\ \text{$\varphi\colon M\to\mathbb{R}$
nonexpanding}\right\\}$

Hutchinson shows that $(\mathbf{P}(M,d),L)$ is a complete metric space in
[14], and that $\sigma_{a}^{\\#}\colon\mathbf{P}(M,d)\to\mathbf{P}(M,d)$ is a
contraction with the same coefficient as $\sigma_{a}$.

Now define the operator
$[\beta]_{\sigma}\colon\mathbf{P}(M,d)^{X}\to\mathbf{P}(M,d)^{X}$ by setting

$[\beta]_{\sigma}(\vec{\rho})_{x}(B)=\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}r\leavevmode\nobreak\ \sigma_{a}^{\\#}\rho_{y}(B)$

We need to show that $[\beta]_{\sigma}$ is a contraction in the product
metric. To this end, let $\vec{\rho},\vec{\theta}\in\mathbf{P}(M,d)^{X}$, and
suppose that for any $x\in X$, $L(\rho_{x},\rho_{x})\leq\delta$ for some
$\delta>0$. Let $c$ be the maximum contraction coefficient of the
$\sigma_{a}$s. Then, given $x,y\in X$,

$\displaystyle
L([\beta]_{\sigma}(\vec{\rho})_{x},[\beta]_{\sigma}(\vec{\theta})_{x})$
$\displaystyle=\sup\left\\{\int_{M}\varphi\leavevmode\nobreak\
d[\beta]_{\sigma}(\rho)_{x}-\int_{M}\varphi\leavevmode\nobreak\
d[\beta]_{\sigma}(\theta)_{x}\leavevmode\nobreak\ \middle|\leavevmode\nobreak\
\text{$\varphi\colon M\to\mathbb{R}$ nonexp.}\right\\}$
$\displaystyle=\sup\left\\{\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}r(\int_{M}\varphi\leavevmode\nobreak\
d\sigma_{a}^{\\#}\rho_{y}-\int_{M}\varphi\leavevmode\nobreak\
d\sigma_{a}^{\\#}\theta_{y})\leavevmode\nobreak\ \middle|\leavevmode\nobreak\
\text{$\varphi\colon M\to\mathbb{R}$ nonexp.}\right\\}$
$\displaystyle\leq\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}rc\sup\left\\{\int_{M}\varphi\leavevmode\nobreak\
d\rho_{y}-\int_{M}\varphi\leavevmode\nobreak\ d\theta_{y}\leavevmode\nobreak\
\middle|\leavevmode\nobreak\ \text{$\varphi\colon M\to\mathbb{R}$
nonexp.}\right\\}$
$\displaystyle=\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}rcL(\rho_{y},\theta_{y})$ $\displaystyle\leq c\delta$

It follows that $[\beta]_{\sigma}$ is a contraction in the product metric, and
therefore has a unique fixed-point. Equivalently, $(X,\beta)$ has a unique
solution.

Now we check that $\hat{\beta}_{\sigma}$ is a solution to $(X,\delta)$. Let
$B$ be any Borel subset of $A^{\omega}$. We begin with an observation. Let
$C\subseteq A^{*}$ be a prefix closed language, and set $C_{n}=\\{w\in
C\mid|w|=n\\}$ for each $n\in\mathbb{N}$. Suppose $C$ satisfies the following
property: (*) for any $n\in\mathbb{N}$ and $u\in C_{n}$,
$B\subseteq\bigcup_{w\in C_{n}}B_{w}$ but $B\not\subseteq\bigcup_{w\in
C_{n}\setminus u}B_{w}$. Then $B=\bigcap_{n\in\mathbb{N}}\bigcup_{w\in
C_{n}}B_{w}$, and in particular, for any Borel measure $\rho$ on $A^{\omega}$,
$\rho(B)=\lim_{n\in\mathbb{N}}\sum_{w\in C_{n}}\rho(B_{m})$.

Now let $U$ be a Borel subset of $(M,d)$ and take $B=\sigma_{\omega}^{-1}(U)$.
Let $x\in X$, and recall that
$\hat{\beta}_{\sigma}(x)(U)=\sigma_{\omega}^{\\#}\hat{\beta}(x)(U)=\hat{\beta}(x)(B)$.
Let $C=\\{w\mid(\exists\vec{a}\in\operatorname{str}(x))\leavevmode\nobreak\
\sigma_{\omega}(w\vec{a})\in B\\}$, and observe that $C$ satisfies (*) above.
We have

$\displaystyle\hat{\beta}_{\sigma}(x)(U)$
$\displaystyle=\lim_{n\in\mathbb{N}}\sum_{w\in C_{n}}\hat{\beta}(x)(B_{w})$
$\displaystyle=\lim_{n\in\mathbb{N}}\sum_{w\in
C_{n}}\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}}r\hat{\beta}(x)(a^{-1}B_{w})$
$\displaystyle=\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}r\lim_{n\in\mathbb{N}}\sum_{w\in C_{n}}\hat{\beta}(y)(a^{-1}B_{w})$
$\displaystyle=\sum_{x\mathrel{\raisebox{-1.0pt}{$\xrightarrow{r\mid
a}$}}y}r\hat{\beta}(y)(U)$

as desired.

Since the support of $\hat{\beta}(x)$ is precisely $\operatorname{str}(x)$,
the support of $\hat{\beta}_{\sigma}(x)$ is precisely
$\sigma_{\omega}(\operatorname{str}(x))$, which we have already seen is the
regular subfractal determined by the state $x$ of the underlying LTS of
$(X,\beta)$.

### Probabilistic Process Algebra

Finally, we introduce a syntax for specifying LMCs. Our specification language
is essentially the _productive_ fragment of Stark and Smolka’s process
calculus [28], meaning that the expressions do not involve deadlock and all
variables are guarded.

######  Definition 5.8.

The set of _probabilistic terms_ is given by the grammar

$v\mid ae\mid e_{1}\oplus_{r}e_{2}\mid\mu v\leavevmode\nobreak\ e$

Here $r\in[0,1]$, and otherwise we make the same stipulations as in 1. The set
of _probabilistic process terms_ $\mathsf{PTerm}$ consists of the closed and
guarded probabilistic terms.

Instead of _languages_ of streams, the analog of trace semantics appropriate
for probabilistic process terms is a measure-theoretic semantics consisting of
trace measures introduced earlier in this section (Equation 8).

######  Definition 5.9.

We define the LMC $(\mathsf{PTerm},\delta)$ in Figure 6 and call it the
_syntactic LMC_. The _trace measure semantics_ $\operatorname{trm}(e)$ of a
probabilistic process term $e$ is defined to be
$\operatorname{trm}(e)=\hat{\delta}(x)$. Given $\sigma\colon
A\to\operatorname{Con}(M,d)$, the _subfractal semantics of
$e\in\mathsf{PTerm}$ corresponding to $\sigma$_ is $\hat{\delta}_{\sigma}(e)$.

$\displaystyle\delta(ae)(b,f)$ $\displaystyle=\begin{cases}1&f=e\text{ and
}b=a\\\ 0&\text{otherwise}\end{cases}$
$\displaystyle\delta(e_{1}\oplus_{r}e_{2})(b,f)$
$\displaystyle=r\delta(e_{1})(b,f)+(1-r)\delta(e_{2})(b,f)$
$\displaystyle\delta(\mu v\leavevmode\nobreak\ e)(b,f)$
$\displaystyle=\delta(e[\mu v\leavevmode\nobreak\ e/v])(b,f)$ Figure 6:  The
LMC structure $(\mathsf{PTerm},\delta)$. Above, $a,b\in A$, $\sum r_{i}=1$,
and $e,e_{i},f\in\mathsf{PTerm}$.

Intuitively, the trace measure semantics of a process term $e$ assigns a Borel
set of streams $B$ the probability that $e$ eventually emits a word in $B$.
Trace measure semantics can be computed inductively as follows.

######  Lemma 5.10.

For any $w\in A^{*}$, $a\in A$, $e,e_{i}\in\mathsf{PTerm}$, and $r\in[0,1]$,
$\operatorname{trm}(e)(A^{\omega})=1$ and

$\displaystyle\operatorname{trm}(ae)(B_{w})$
$\displaystyle=\begin{cases}\operatorname{trm}(e)(B_{u})&\text{$w=au$}\\\
0&\text{otherwise}\end{cases}$
$\displaystyle\operatorname{trm}(e_{1}\oplus_{r}e_{2})(B_{w})$
$\displaystyle=r\operatorname{trm}(e_{1})(B_{w})+(1-r)\operatorname{trm}(e_{2})(B_{w})$
$\displaystyle\operatorname{trm}(\mu v\leavevmode\nobreak\ e)(B_{w})$
$\displaystyle=\operatorname{trm}(e[\mu v\leavevmode\nobreak\ e/v])(B_{w})$

Similar to the situation with trace semantics and regular subfractals, trace
measure semantics and subfractal measure semantics identify the same
probabilistic process terms.

######  Theorem 5.11.

Let $e,f\in\mathsf{PTerm}$. Then $\operatorname{trm}(e)=\operatorname{trm}(f)$
if and only if for any contraction operator interpretation $\sigma\colon
A\to\operatorname{Con}(M,d)$,
$\hat{\delta}_{\sigma}(e)=\hat{\delta}_{\sigma}(f)$.

### Axiomatization

Figure 7 outlines an inference system for determining when the subfractal
measures corresponding to two expressions coincide.

######  Definition 5.12.

Given $e,f\in\mathsf{PTerm}$, write $e\equiv f$ and say that $e$ and $f$ are
_provably equivalent_ if the equation $e=f$ can be derived from inference
rules in Figure 7.

$\displaystyle\begin{aligned} (\axiom{ID})\hskip 2.0pt&&e\oplus_{r}e&\equiv
e\\\ (\axiom{CM})&&e_{1}\oplus_{r}e_{2}&\equiv e_{2}\oplus_{1-r}e_{1}\\\
(\axiom{AS})\hskip 1.5pt&&(e_{1}\oplus_{r}e_{2})\oplus_{s}e_{3}&\equiv
e_{1}\oplus_{rs}(e_{2}\oplus_{\frac{s(1-r)}{1-rs}}e_{3})\\\ (\axiom{DS})\hskip
1.5pt&&a(e_{1}\oplus_{r}e_{2})&\equiv ae_{1}\oplus_{r}ae_{2}\\\
(\axiom{FP})\hskip 1.5pt&&\mu v\leavevmode\nobreak\ e&\equiv e[\mu
v\leavevmode\nobreak\ e/v]\end{aligned}\qquad\begin{array}[]{r
c}(\axiom{CN})&\infer{(\forall i)\leavevmode\nobreak\ e_{i}\equiv
f_{i}}{g[\vec{e}/\vec{v}]\equiv g[\vec{f}/\vec{v}]}\\\ (\axiom{AE})&\infer{\
}{\mu w\leavevmode\nobreak\ e\equiv\mu v\leavevmode\nobreak\ e[v/w]}\\\
(\axiom{UA})&\infer{g\equiv e[g/v]}{g\equiv\mu v\leavevmode\nobreak\
e}\end{array}$ Figure 7:  Axioms for probabilistic trace equivalence Above,
$e,e_{1},e_{2}\in\mathsf{PTerm}$, $a\in A$, $r,s\in[0,1]$, and $rs\neq 1$.
Also, in (), $v$ is not free in $e$.

######  Theorem 5.13 (Soundness).

For any $e,f\in\mathsf{PTerm}$, if $e\equiv f$, then for any complete metric
space $(M,d)$ and any $\sigma\colon A\to\operatorname{Con}(M,d)$,
$\hat{\delta}_{\sigma}(e)=\hat{\delta}_{\sigma}(f)$.

Unlike the situation with trace equivalence, it is not known if these axioms
are complete with respect to subfractal measure semantics. We leave this as a
conjecture.

######  Conjecture 5.14 (Completeness).

Figure 7 is a complete axiomatization of trace measure semantics. That is, for
any $e,f\in\mathsf{PTerm}$, if for any complete metric space $(M,d)$ and any
$\sigma\colon A\to\operatorname{Con}(M,d)$ we have
$\hat{\delta}_{\sigma}(e)=\hat{\delta}_{\sigma}(f)$, then $e\equiv f$.

We expect that 5.14 can be proven in a similar manner to Theorem 4.9.

##  6 A Question about Regular Subfractals

Certain regular subfractals that have been generated by LTSs with multiple
states happen to coincide with self-similar sets using a different alphabet of
action symbols and under a different contraction operator interpretation. For
example, the twisted Sierpiński gasket in Figure 2 is the self-similar set
generated by the iterated function system consisting of the compositions
$\sigma_{a},\sigma_{b}\sigma_{b},\sigma_{b}\sigma_{c},\sigma_{c}\sigma_{b}$,
and $\sigma_{c}\sigma_{c}$.

######  Question 6.1.

Is every regular subfractal a self-similar set? In other words, are there
regular subfractals which can only be generated by a multi-state LTS?

######  Example 6.2.

To illustrate the subtlety of this question, consider the following LTS.

$x$$b$$a$$b$

The state $x$ emits $(a,a,\ldots)$ (an infinite stream of $a$’s) and
$(a,\ldots,a,b,b,\ldots)$, a stream with some finite number (possibly $0$) of
$a$’s followed by an infinite stream of $b$’s. Now let $M=\mathbb{R}$ with
Euclidean distance and consider the contraction operator interpretation
$\sigma_{a}(r)=\frac{1}{2}r$ and $\sigma_{b}(r)=\frac{1}{2}r+\frac{1}{2}$. Let
$K=\\{0\\}\cup\\{\frac{1}{2^{n}}|n\geq 0\\}$. Then $K$ is the component of the
solution at $x$. This example is interesting because unlike the Twisted
Sierpiński gasket in Figure 2, there is no obvious finite set of compositions
$\sigma_{a}$ and $\sigma_{b}$ such that $K$ is the self-similar set generated
by that iterated function system.

There is an LTS $(X,\alpha)$ with $X$ a singleton set $\\{x\\}$, and a
contraction operator interpretation $\sigma_{x}$ whose solution is $K$. We
take the set of action labels underlying $X$ to be $B=\\{f,g,h\\}$ and use the
contraction operator interpretation $\sigma_{f}(r)=0$, $\sigma_{g}(r)=1$ and
$\sigma_{h}(r)=\frac{1}{2}r$. It is easy to verify that
$K=\bigcup_{i\in\\{f,g,h\\}}\sigma_{i}(K)$.

But we claim that $K$ is not obtainable using a single-state LTS and _the same
contractions_ $\sigma_{a}(r)=\frac{1}{2}r$ and
$\sigma_{b}(r)=\frac{1}{2}r+\frac{1}{2}$, or using _any (finite) compositions_
of $\sigma_{a}$ and $\sigma_{b}$. Indeed, suppose there were such a finite
collection $\sigma_{1},\ldots\sigma_{n}$ consisting of (finite) compositions
of $\sigma_{a}$ and $\sigma_{b}$ such that $K=\bigcup_{i=1}^{n}\sigma_{i}(K)$.
Since $1\in K$, we must be using the stream $(b,b,b,\ldots)$ (since if there
is an $a$ at position $n$, the number obtained would be $\leq
1-\frac{1}{2^{n}}<1$), so some $\sigma_{i}$ must consist of a composition of
$\sigma_{b}$ some number $m\geq 1$ of times with itself. Similarly, the only
way to obtain $0$ is with $(a,a,a,\ldots)$, so there must be some $\sigma_{j}$
which is a composition of $\sigma_{a}$ some number of times $p\geq 1$ with
itself. But then
$\lim_{n\rightarrow\infty}\sigma_{i}\circ\sigma_{j}\circ\sigma^{n}_{i}(r)=1-(\frac{2^{p}-1}{2^{m+p}})>\frac{1}{2}$,
since $m,p\geq 1$. That point must be in the subset of $\mathbb{R}$ generated
by this LTS. However, it is not in $K$, since
$\frac{1}{2}<1-(\frac{2^{p}-1}{2^{m+p}})<1$.

More generally, we cannot obtain $K$ using a single-state LTS even if we
allowed finite sums of compositions of $\sigma_{a}$ and $\sigma_{b}$.

Once again, it is possible to find a single state LTS whose corresponding
subset of $\mathbb{R}$ is $K$, but to do this we needed to _change the
alphabet and also the contractions_. Perhaps un-coincidentally, the constant
operators are exactly the limits of the two contractions from the original
interpretation. Our question is whether this can always be done.

On the other hand, the thesis of Boore [7] may contain an answer to 6.1. Boore
presents a (family) of $2$-state GIFS whose _attractors_ , total unions of
their regular subfractals, are not self-similar. Attractors of GIFSs are not
precisely the same as regular subfractals, so additional work is required to
adapt Boore’s work to answer 6.1.

##  7 Related Work

This paper is part of a larger effort of examining topics in continuous
mathematics from the standpoint of coalgebra and theoretical computer science.
The topic itself is quite old, and originates perhaps with Pavlovic and
Escardó’s paper “Calculus in Coinductive Form” [24]. Another early
contribution is Pavlovic and Pratt [25]. These papers proposed viewing some
structures in continuous mathematics—the real numbers, for example, and power
series expansions—in terms of final coalgebras and streams. The next stage in
this line of work was a set of papers specifically about fractal sets and
final coalgebras. For example, Leinster [17] offered a very general theory of
self-similarity that used categorical modules in connection with the kind of
gluing that is prominent in constructions of self-similar sets. In a different
direction, papers like [4] showed that for some very simple fractals (such as
the Sierpiński gasket treated here), the final coalgebras were Cauchy
completions of the initial algebras.

Generalizations of IFSs. Many generalizations of Hutchinson’s self-similar
sets have appeared in the literature. The generalization that most closely
resembles our own is that of an attractor for a _directed-graph iterated
function system_ (GIFS) [19]. A LTS paired with a contraction operator
interpretation is equivalent data to that of a GIFS, and equivalent statements
to Lemma 3.3 can be found for example in [19, 9, 20]. As opposed to the
regular subfractal corresponding to one state, as we have studied above, the
geometric object studied in the GIFSs literature is typically the union of the
regular subfractals corresponding to all the states (in our terminology), and
properties such as Hausdorff dimension and connectivity are emphasized. We
also distinguish our structures from GIFSs because we need to allow the
interpretations of the labels to vary in our semantics.

Another generalization is Mihail and Miculescu’s notion of attractor for a
_generalized iterated function system_ [20]. A generalized IFS is essentially
that of Hutchinson’s IFS with multi-arity contractions—equivalent to a single-
state labelled transition system where labels have ‘higher arity’. A common
generalization of GIFSs and generalized IFSs could be achieved by considering
coalgebras of the form $X\to\mathcal{P}(\coprod_{n\in\mathbb{N}}A_{n}\times
X^{n})$ and interpreting each $a\in A_{n}$ as an $n$-ary contraction. We
suspect that a similar story to the one we have outlined in this paper is
possible for this common generalization.

Process algebra. The process terms we use to specify labelled transition
systems and labelled Markov chains are fragments of known specification
languages. Milner used process terms to specify LTSs in [23], and we have
repurposed his small-step semantics here. Stark and Smolka use probabilistic
process terms to specify labelled Markov chains (in our terminology) in [28],
and we have used them for the same purpose. Both of these papers also include
complete axiomatizations of bisimilarity, and we have also repurposed their
axioms.

However, fractal semantics is strictly coarser than bisimilarity, and in
particular, bisimilarity of process terms is trace equivalence. Rabinovich
added a single axiom to Milner’s axiomatization to obtain a sound and complete
axiomatization of trace equivalence of expressions [26], which allowed us to
derive Theorem 4.9. In contrast, the axiomatization of trace equivalence for
probabilistic processes is only well-understood for _finite_ traces, see Silva
and Sokolova’s [27], which our probabilistic process terms do not exhibit. We
use the trace semantics of Kerstan and König [15] because it takes into
account infinite traces. Infinite trace semantics has yet to see a complete
axiomatization in the literature.

Other types of syntax. In this paper, we used the specification language of
$\mu$-terms as our basic syntax. As it happens, there are two other flavors of
syntax that we could have employed. These are _iteration theories_ [5], and
terms in the Formal Language of Recursion $FLR$, especially its $FLR_{0}$
fragment. The three flavors of syntax for fixed point terms are compared in a
number of papers: In [13], it was shown that there is an equivalence of
categories between $FLR_{0}$ structures and iteration theories, and Bloom and
Ésik make a similar connection between iteration theories and the
$\mu$-calculus in [6]. Again, these results describe general matters of
equivalence, but it is not completely clear that for a specific space or class
of spaces that they are equally powerful or equally convenient specification
languages. We feel this matter deserves some investigation.

Equivalence under hypotheses. A specification language fairly close to
iteration theories was used by Milius and Moss to reason about fractal
constructions in [22] under the guise of _interpreted solutions_ to recursive
program schemes [21]. Moreover, [22] contains important examples of reasoning
about the equality of fractal sets under assumptions about the contractions.
Based on the general negative results on reasoning from hypotheses in the
logic of recursion [13], we would not expect a completeness theorem for
fractal equivalence under hypotheses. However, we do expect to find sound
logical systems which account for interesting phenomena in the area.

##  8 Conclusion

This paper connects fractals to trace semantics, a topic originating in
process algebra. This connection is our main contribution, because it opens up
a line of communication between two very different areas of study. The study
of fractals is a well-developed area, and like most of mathematics it is
pursued without a special-purpose specification language. When we viewed
process terms as recipes for fractals, we provided a specification language
that was not present in the fractals literature. Of course, one also needs a
contraction operator interpretation to actually define a fractal, but the
separation of syntax (the process terms) and semantics (the fractals obtained
using contraction operator interpretations of the syntax) is something that
comes from the tradition of logic and theoretical computer science. Similarly,
the use of a logical system and the emphasis on soundness and completeness is
a new contribution here.

All of the above opens questions about fractals and their specifications. Our
most concrete question was posed in Section 6. We would also like to know if
we can obtain completeness theorems allowing for extra equations in the
axiomatization. Lastly, and most speculatively, since LTSs (and other
automata) appear so frequently in decision procedures from process algebra and
verification, we would like to know if our semantics perspective on fractals
can provide new complexity results in fractal geometry.

We hope we have initiated a line of research where questions and answers come
from both the analytic side and from theoretical computer science.

### Acknowledgements

Todd Schmid was partially funded by ERC Grant Autoprobe (grant agreement
10100269). Lawrence Moss was supported by grant #586136 from the Simons
Foundation. We would like to thank Alexandra Silva and Dylan Thurston for
helpful discussions. The images in Figures 1 and 2 were made using SageMath
and GIMP.

## References

  * [1] Jos C. M. Baeten.  A brief history of process algebra.  Theor. Comput. Sci., 335(2-3):131–146, 2005.  doi:10.1016/j.tcs.2004.07.036.
  * [2] Stefan Banach.  Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales.  Fundamenta Mathematicae, 3:133–181, 1922.
  * [3] Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors.  Handbook of Process Algebra.  North-Holland / Elsevier, 2001.  doi:10.1016/b978-0-444-82830-9.x5017-6.
  * [4] Prasit Bhattacharya, Lawrence S. Moss, Jayampathy Ratnayake, and Robert Rose.  Fractal sets as final coalgebras obtained by completing an initial algebra.  In Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten, editors, Horizons of the Mind. A Tribute to Prakash Panangaden \- Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, volume 8464 of Lecture Notes in Computer Science, pages 146–167. Springer, 2014.
  * [5] Stephen L. Bloom and Zoltán Ésik.  Iteration Theories - The Equational Logic of Iterative Processes.  EATCS Monographs on Theoretical Computer Science. Springer, 1993.  doi:10.1007/978-3-642-78034-9.
  * [6] Stephen L. Bloom and Zoltán Ésik.  Solving polynomial fixed point equations.  In Mathematical foundations of computer science 1994 (Košice, 1994), volume 841 of Lecture Notes in Comput. Sci., pages 52–67. Springer, Berlin, 1994.
  * [7] Graeme C. Boore.  Directed graph iterated function systems.  PhD thesis, University of St. Andrews, 2011.  URL: http://hdl.handle.net/10023/2109.
  * [8] G. A. Edgar and R. Daniel Mauldin.  Multifractal decompositions of digraph recursive fractals.  Proceedings of the London Mathematical Society, s3-65(3):604–628, 1992.  URL: https://londmathsoc.onlinelibrary.wiley.com/doi/abs/10.1112/plms/s3-65.3.604, arXiv:https://londmathsoc.onlinelibrary.wiley.com/doi/pdf/10.1112/plms/s3-65.3.604, doi:https://doi.org/10.1112/plms/s3-65.3.604.
  * [9] Gerald A. Edgar.  Measure, Topology, and Fractal Geometry.  Springer New York, NY, 1 edition, 1990.  doi:10.1007/978-1-4757-4134-6.
  * [10] Kenneth J. Falconer.  The Geometry of Fractal Sets.  Cambridge Tracts in Mathematics. Cambridge University Press, 1986.  URL: https://www.cambridge.org/us/academic/subjects/mathematics/abstract-analysis/geometry-fractal-sets.
  * [11] Alison L. Gibbs and Francis Edward Su.  On choosing and bounding probability metrics.  International Statistical Review / Revue Internationale de Statistique, 70(3):419–435, 2002.  URL: http://www.jstor.org/stable/1403865, doi:10.2307/1403865.
  * [12] C. A. R. Hoare.  Communicating sequential processes.  Commun. ACM, 21(8):666–677, 1978.  doi:10.1145/359576.359585.
  * [13] A. J. C. Hurkens, Monica McArthur, Yiannis N. Moschovakis, Lawrence S. Moss, and Glen T. Whitney.  Erratum: “The logic of recursive equations”.  J. Symbolic Logic, 64, 1999.
  * [14] John E. Hutchinson.  Fractals and self similarity.  Indiana University Mathematics Journal, 30(5):713–747, 1981.  URL: http://www.jstor.org/stable/24893080.
  * [15] Henning Kerstan and Barbara König.  Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems.  Logical Methods in Computer Science, Volume 9, Issue 4, December 2013.  URL: https://lmcs.episciences.org/859, doi:10.2168/LMCS-9(4:16)2013.
  * [16] S. C. Kleene.  Representation of events in nerve nets and finite automata.  In Claude Shannon and John McCarthy, editors, Automata Studies, pages 3–41. Princeton University Press, Princeton, NJ, 1956.
  * [17] Tom Leinster.  A general theory of self-similarity.  Adv. Math., 226(4):2935–3017, 2011.
  * [18] Benoit B. Mandelbrot.  Fractals: Form, Chance, and Dimension.  Mathematics Series. W. H. Freeman, 1977.  URL: https://books.google.com/books?id=avw_AQAAIAAJ.
  * [19] R Daniel Mauldin and S. C. Williams.  Hausdorff dimension in graph directed constructions.  Transactions of the American Mathematical Society, 309(2):811–829, 1988.  doi:10.1090/S0002-9947-1988-0961615-4.
  * [20] Alexandru Mihail and Radu Miculescu.  Generalized ifss on noncompact spaces.  Fixed Point Theory and Applications, 1(584215), 2010.  doi:10.1155/2010/584215.
  * [21] Stefan Milius and Lawrence S. Moss.  The category-theoretic solution of recursive program schemes.  Theor. Comput. Sci., 366(1-2):3–59, 2006.  doi:10.1016/j.tcs.2006.07.002.
  * [22] Stefan Milius and Lawrence S. Moss.  Equational properties of recursive program scheme solutions.  Cah. Topol. Géom. Différ. Catég., 50(1):23–66, 2009\.
  * [23] 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.
  * [24] Dusko Pavlovic and Martín Hötzel Escardó.  Calculus in coinductive form.  In Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998, pages 408–417. IEEE Computer Society, 1998.
  * [25] Dusko Pavlovic and Vaughan R. Pratt.  The continuum as a final coalgebra.  Theor. Comput. Sci., 280(1-2):105–122, 2002.
  * [26] Alexander Moshe Rabinovich.  A complete axiomatisation for trace congruence of finite state behaviors.  In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 530–543. Springer, 1993.  doi:10.1007/3-540-58027-1\\_25.
  * [27] Alexandra Silva and Ana Sokolova.  Sound and complete axiomatization of trace semantics for probabilistic systems.  In Michael W. Mislove and Joël Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 291–311. Elsevier, 2011.  doi:10.1016/j.entcs.2011.09.027.
  * [28] 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.