Fast Computations on Ordered Nominal Sets

TL;DR

This paper introduces an efficient method for computing with ordered nominal sets by directly representing orbits, leading to a new library that improves performance in automata minimization and learning over infinite alphabets.

Contribution

It develops a direct orbit-based representation for ordered nominal sets, enabling more accurate complexity analysis and practical efficiency improvements.

Findings

ONS library performs competitively in automata minimization.

ONS outperforms existing tools on certain input classes.

The approach enables efficient computations with ordered nominal sets.

Abstract

We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis. The approach is implemented as the library ONS (Ordered Nominal Sets). Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets. We evaluate ONS in two applications: minimisation of automata and active automata learning. In both cases, ONS is competitive compared to existing implementations and outperforms them for certain classes of inputs.

Tables

Table 1. Table 1 : Overview of representation.

Object	Representation
Single orbit $O$	Natural number $n=dim\left(O\right)$
Nominal set $X={\bigcup }_i{O}_i$	Multiset of these numbers
Map from single orbit $f:O\to Y$	The orbit $f\left(O\right)$ and a bit string $F$
Equivariant map $f:X\to Y$	Set of tuples $(O,F,f\left(O\right))$, one for each orbit
Orbit in a product $O\subseteq X\times Y$	The corresponding orbits of $X$ and $Y$, and a string $P$ relating their supports
Product $X\times Y$	Set of tuples $(P,O_X,O_Y)$, one for each orbit

Table 2. Table 2 : Running times for Algorithm  1 . N N \operatorname{N} ( dim dimension \dim ) is the size (resp. dimension) of the input. The column L 𝐿 L denotes the number of locations, if the automaton can be expressed symbolically. The first two sets of automata (‘Random’ and ‘Formula’) are the randomly generated automata. Each rows consists of 10 automata and we report the average runtime. If one of the runs times out, the cell indicates > > 2h.

Model	$N$	$L$	$dim$	Ons (s)	Ons-hs (s)	N$\lambda$ (s)	Lois (s)
Random	5		$\le$ 1	0.00	0.00	0.05	0.71
Random	10		$\le$ 1	0.00	0.00	0.93	12.31
Random	10		$\le$ 2	0.01	0.00	26.60	$>$ 2h
Random	15		$\le$ 1	0.00	0.00	5.01	41.31
Random	15		$\le$ 2	0.01	0.00	61.98	$>$ 2h
Random	15		$\le$ 3	0.04	0.02	418.22	$>$ 2h
Formula		5	$\le$ 2	0.00	0.01	0.25
Formula		10	$\le$ 2	0.01	0.02	1.52
Formula		10	$\le$ 3	0.62	0.57	1.52
Formula		25	$\le$ 2	0.06	0.05	48.81
Formula		25	$\le$ 3	2.89	1.58	108.46
Formula		25	$\le$ 5	$>$ 2h	2176.83	255.39
FIFO($1$)	4	4	1	0.02	0.00	0.01	0.03
FIFO($2$)	13	7	2	0.01	0.01	1.03	0.24
FIFO($3$)	65	11	3	0.35	0.70	9.32	2.44
FIFO($4$)	440	16	4	37.60	39.77	68.44	15.33
FIFO($5$)	3686	22	5	$>$ 2h	3027.54	382.33	71.59
$ww\left(1\right)$	4	4	1	0.02	0.00	0.01	0.03
$ww\left(2\right)$	8	6	2	0.00	0.00	0.12	0.03
$ww\left(3\right)$	24	8	3	0.16	0.17	0.75	0.16
$ww\left(4\right)$	112	10	4	23.71	30.51	2.85	0.60
$ww\left(5\right)$	728	12	5	5880.04	$>$ 2h	9.27	1.83
${ℒ}_{\text{max}}$	5		2	0.02	0.00	1.08	0.06
${ℒ}_{\text{int}}$	5		2	0.01	0.00	1.71	0.04

Equations

$$\{(q_1,q_2)\mid q_1<q_2\},\{(q_1,q_2)\mid q_1>q_2\},\{(q_1,q_2)\mid q_1=q_2\}.$$

$${\mathcal{P}}_n(X)=\{Y\subseteq X\mid |Y|=n\}.$$

$$\dim (X)=\max \{\dim (x)\mid x\in X\}.$$

$${\mathcal{L}}_{\text{int}}=\{a_1{b}_1\cdots a_n{b}_n\mid a_i,b_i\in \mathbb{Q},a_i<a_{i+1}<b_{i+1}<b_i\text{ for all }i\}.$$

$$S=\{q_0,q_4\}\cup \{q_1(a)\mid a\in \mathbb{Q}\}\cup \{q_2(a,b)\mid a<b\in \mathbb{Q}\}\cup \{q_3(a,b)\mid a<b\in \mathbb{Q}\}$$

$$\delta (q_2(a,b),c)=q_3(c,b)\text{for all }a<c<b\in \mathbb{Q}.$$

$$F=\{q_2(a,b)\mid a<b\in \mathbb{Q}\},$$

$${\mathcal{L}}_{\text{max}}=\{wa\in {\mathbb{Q}}^{\ast }\mid a=\max (w_1,\dots ,w_n)\}$$

$$G{|}_C=\{\pi {|}_C\mid \pi \in G,C\pi =C\},$$

$${\mathrm{ext}}_G(S)=\{\pi \in G\mid \pi {|}_C\in S\}.$$

$$[C,S{]}^{ec}=G/{\mathrm{ext}}_G(S)=\{\{sg\mid s\in {\mathrm{ext}}_G(S)\}\mid g\in G\}.$$

$$\pi (x)=\{\begin{array}{ll}x-C(1)+C^{\prime }(1)& \text{if }x<C(1)\\ (x-C(i))\frac{C^{\prime }(i+1)-C^{\prime }(i)}{C(i+1)-C(i)}+C^{\prime }(i)& \text{if }C(i)\le x<C(i+1)\\ x-C(n)+C^{\prime }(n)& \text{if }C(n)\le x\end{array}$$

$${\pi }^{-1}(x)=\{\begin{array}{ll}x-C^{\prime }(1)+C(1)& \text{if }x{<}^{\prime }C(1)\\ (x-C^{\prime }(i))\frac{C(i+1)-C(i)}{C^{\prime }(i+1)-C^{\prime }(i)}+C(i)& \text{if }{C}^{\prime }(i)\le x<C^{\prime }(i+1)\\ x-C^{\prime }(n)+C(n)& \text{if }{C}^{\prime }(n)\le x\end{array}$$

$$X\cong [C,I{]}^{ec}\cong {\mathcal{P}}_{|C|}(\mathbb{Q}).$$

$$[[f]]=\bigcup _{\begin{array}{c}n\in \mathbb{N}\\ 1\le i\le f(n)\end{array}}\{i\}\times {\mathcal{P}}_n(\mathbb{Q}).$$

$$X_i=\bigcup _{1\le j\le k_i}{O}_{i,j}.$$

$$[[f]]=\bigcup _{\begin{array}{c}i\in \mathbb{N}\\ 1\le j\le f(i)\end{array}}\{j\}\times {\mathcal{P}}_i(\mathbb{Q})\cong \bigcup _{\begin{array}{c}i\in \mathbb{N}\\ 1\le j\le k_i\end{array}}{O}_{i,j}=X.$$

$$\begin{array}[]{ll}\{(a,(b,c))\mid a,b,c\in\mathbb{Q},a<b<c\},&\{(a,(a,b))\mid a,b\in\mathbb{Q},a<b\},\\ \{(b,(a,c))\mid a,b,c\in\mathbb{Q},a<b<c\},&\{(b,(a,b))\mid a,b\in\mathbb{Q},a<b\},\\ \{(c,(a,b))\mid a,b,c\in\mathbb{Q},a<b<c\}.\end{array}$$

$$[[(P,O_1,O_2)]]=({\mathcal{P}}_{|P|}(\mathbb{Q}),f_{H_1},f_{H_2}),$$

$$[[(P,O_1,O_2)]]=(O^{\prime },f,g)\cong (⟨f,g⟩(O^{\prime }),{\pi }_1{|}_{⟨f,g⟩(O^{\prime })},{\pi }_2{|}_{⟨f,g⟩(O^{\prime })}).\text{qed}$$

$$[[(P,O_1,O_2)]]\cong (O,{\pi }_1{|}_O,{\pi }_2{|}_O).$$

$$P(i)=\{\begin{array}{ll}L& \text{ if }{F}_1(i)=1\text{ and }{F}_2(i)=0\\ R& \text{ if }{F}_1(i)=0\text{ and }{F}_2(i)=1\\ B& \text{ if }{F}_1(i)=F_2(i)=1\end{array}$$

$$(O,{\pi }_1{|}_O,{\pi }_2{|}_O)\cong [[(P,O_1,O_2)]].$$

$$(O,{\pi }_1{|}_O,{\pi }_2{|}_O)\cong ({\mathcal{P}}_{|F_1|}(\mathbb{Q}),f_{\{({\mathcal{P}}_{|F_1|}(\mathbb{Q}),F_1,O_1)\}},f_{\{({\mathcal{P}}_{|F_2|}(\mathbb{Q}),F_2,O_2)\}}).$$

$$\begin{array}[]{rcl}f_{\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{1},O_{1})\}}(x)&=&f_{\{(\mathcal{P}_{|P^{\prime}|}(\mathbb{Q}),F_{1}^{\prime},O_{1}^{\prime})\}}(x^{\prime})\,,\text{ and }\\ f_{\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{2},O_{2})\}}(x)&=&f_{\{(\mathcal{P}_{|P^{\prime}|}(\mathbb{Q}),F_{2}^{\prime},O_{2}^{\prime})\}}(x^{\prime})\,.\end{array}$$

$$h(n)=\sum _{\begin{array}{c}0\le i,j\le n\\ i+j\ge n\end{array}}f(i)g(j)\left(\genfrac{}{}{0ex}{}{n}{j}\right)\left(\genfrac{}{}{0ex}{}{j}{n-i}\right).$$

$$\{(q,q^{\prime })\in R\mid \forall a\in A:(f(q,a),f(q^{\prime },a))\in R\}.$$

$${\{\text{{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{fromList}}}}}} }[x_{0},x_{1},x_{2}]\mid x_{0}<x_{1}\wedge x_{1}<x_{2}\}.$$

$$\{(x_0,x_1,x_2)\mid \top \}$$

Full text

††journal: Theoretical Computer Science

1 Introduction

Automata over infinite alphabets are natural models for programs with unbounded data domains. Such automata, often formalised as register automata [2], are applied in the modelling and analysis of communication protocols, hardware, and software systems (see [3, 4, 5, 2, 6, 7] and references therein). Typical infinite alphabets include sequence numbers, timestamps and identifiers. This means that one can model data flow in such automata beyond the basic control flow provided by ordinary automata. Recently, it has been shown in a series of papers that such models are amenable to learning [8, 9, 10, 11, 12, 13] with the verification of (closed source) implementations of the Transmission Control Protocol (TCP) as a prominent example [14].

A foundational approach to infinite alphabets is provided by the algebraic notion of nominal set. In computer science, nominal sets were originally introduced as an elegant formalism for name binding [15, 16]. They have been used in a variety of applications in semantics, computation and concurrency theory; see [17] for an overview.

In particular, Bojańczyk et al. introduce nominal automata, which allow one to model languages over infinite alphabets modelled as nominal sets [3]. Nominal automata are defined as ordinary automata by replacing finite sets with “orbit-finite nominal sets”. This means that the state space of a nominal automaton is finite up to renaming of the infinite data occuring in the alphabet. As a consequence of orbit-finiteness, one can represent these automata finitely and compute with them—for instance, emptiness and equivalence of deterministic automata can be decided with a slight adaptation of the classical algorithms. Nominal automata are equally expressive as register automata: the connection between these models is well exposed by Bojańczyk [18]. Nominal automata thereby provide an elegant mathematical foundation of register automata and automata over infinite alphabets.

Important for applications of nominal sets and automata are implementations. A couple of tools exist to compute with nominal sets. Notably, N$\lambda$ [19] and Lois [20, 21] provide a general purpose programming language to manipulate infinite sets.222Other implementations of nominal techniques that are less directly related to our setting (Mihda, Fresh OCaml and Nominal Isabelle) are discussed in Section 10. Both tools are based on SMT solvers and use logical formulas to represent the infinite sets. These implementations are very flexible, and the SMT solver does most of the heavy lifting, which makes the implementations themselves relatively straightforward. Unfortunately, this comes at a cost as SMT solving is in general PSPACE-hard. Since the formulas used to describe sets tend to grow as more calculations are done, running times can become unpredictable.

The overall aim of the current paper is to provide a library for computing with nominal sets that avoids this implicit representation and allows for a precise complexity analysis of algorithms based on it. The key idea is to represent a nominal set explicitly in terms of its orbits, which then also provides a natural notion of size—e.g., in a nominal automaton, the number of states is typically taken to be the number of orbits of the state space. Towards this aim, we will focus on a specific variant of nominal sets, which we recall first.

The approach of Bojańczyk et al. is based on nominal sets over different “symmetries”, which stipulate the way in which data values can be compared. As a consequence, their results on nominal automata are parametric in the structure of the data values. Two important such structures on data values are:

Data values that can only be compared for equality, referred to as nominal sets over the equality symmetry.

• 2.

Ordered data values, where data values are rational numbers and can be compared for their order; referred to as the total order symmetry.

Most of the classical theory and applications of nominal sets are based on the equality symmetry. In particular, this is the data domain which is most relevant to capture name binding and it was the first data domain considered for register automata.

In this paper, however, we focus specifically on nominal sets over the total order symmetry, for the following reasons. First, the total order symmetry is of interest on its own: allowing to compare data values allows for interesting examples such as data structures (priority queues and search trees use order) [10] and data nets with a dense linear order [22]. Second, it is a natural example of a homogeneous structure, which is a property needed for many decidability problems. For instance, various problems on data nets are decidable for (strongly) homogeneous structures [23], and automata learning of register automata is feasible for $\infty$-extendable words [10] (a notion related to homogeneity). Without homogeneity, these results are not know to hold. Third, nominal sets over the total order symmetry are fairly general: they subsume nominal sets over the equality symmetry. Note however that representing nominal sets over the equality symmetry this way requires more orbits in general. Fourth, as we will show, nominal sets over the total order symmetry allow for a remarkably simple representation. The key insight is that the representation of nominal sets from [3] (and also [24]) simplifies as follows; the “local symmetries” are trivial, so that each orbit is presented solely by a natural number, indicating the number of variables or registers.

Our main contributions include the following.

We develop the representation theory of nominal sets over the total order symmetry. We give concrete representations of nominal sets, their products and equivariant maps.

• 2.

We provide time complexity bounds for operations on nominal sets such as intersections and membership. Using those results we give the time complexity of Moore’s minimisation algorithm (generalised to nominal automata) and prove that it is polynomial in the number of orbits.

• 3.

Using the representation theory, we are able to implement nominal sets in a C++ library Ons. The library includes all the results from the representation theory (sets, products and maps).

We also developed a Haskell implementation, called Ons-hs. This allows us to give a more comprehensive evaluation than with the C++ implementation alone, avoiding results that are caused by specific implementation details. Further, the Haskell implementation is generic, meaning that nominal computations are possible even with custom data types.

• 4.

We evaluate the performance of Ons(-hs), and compare it to N$\lambda$ and Lois, using two algorithms on nominal automata: minimisation [25] and automata learning [12]. We use randomly generated automata as well as concrete, logically structured models such as FIFO queues. For random automata, our methods are considerably faster in most cases than the other tools. On the other hand, Lois and N$\lambda$ are faster in minimising the structured automata as they exploit their logical structure. In automata learning, the logical structure is not available a-priori, and Ons(-hs) is faster in most cases.

The structure of the paper is as follows. The first three sections contain background material: Section 2 on nominal sets, Section 3 on nominal automata, and Section 4 on representation of nominal sets. Next, Section 5 describes the concrete representation of nominal sets, equivariant maps and products in the total order symmetry. The implementations in C++ and Haskell are presented in Sections 6 and 7 respectively. Complexity results are presented in Section 8. Section 9 reports on the evaluation of Ons on algorithms for nominal automata. Related work is discussed in Section 10, and future work in Section 11.

The current paper extends the conference version (ICTAC 2018 [1]) with proofs of all results, new experiments for evaluating Ons based on randomly generated formulas, and an implementation in Haskell, Ons-hs.

2 Nominal sets

Nominal sets are infinite sets that carry certain symmetries, allowing a finite representation in many interesting cases. We recall their formalisation in terms of group actions, following [3, 17], to which we refer for an extensive introduction.

2.1 Group actions.

Let $G$ be a group, with the multiplication denoted by juxtaposition and the unit by $1$. Given a set $X$, a (right) $G$-action is a function ${\cdot}\colon X\times G\to X$ satisfying $x\cdot 1=x$ and $(x\cdot g)\cdot h=x\cdot(gh)$ for all $x\in X$ and $g,h\in G$. A set $X$ with a $G$-action is called a $G$-set and we often write $xg$ instead of $x\cdot g$. The orbit of an element $x\in X$ is the set $\{xg\mid g\in G\}$. A $G$-set is always a disjoint union of its orbits (in other words, the orbits partition the set). We say that $X$ is orbit-finite if it has finitely many orbits, and we denote the number of orbits by $\operatorname{N}(X)$.

A map $f\colon X\rightarrow Y$ between $G$-sets is called equivariant if it preserves the group action, i.e., for all $x\in X$ and $g\in G$ we have $f(xg)=f(x)g$. If an equivariant map $f$ is bijective, then $f$ is an isomorphism and we write $X\cong Y$. A subset $Y\subseteq X$ is called equivariant if for all $y\in Y$ and $g\in G$, we have $yg\in Y$. The product of two $G$-sets $X$ and $Y$ is given by the Cartesian product $X\times Y$ with the pointwise group action on it, i.e., $(x,y)g=(xg,yg)$. Union and intersection of $X$ and $Y$ are well-defined if the two actions agree on their common elements.

2.2 Nominal sets.

A data symmetry is a pair $(\mathcal{D},G)$ where $\mathcal{D}$ is a set and $G$ is a subgroup of $\operatorname{Sym}(\mathcal{D})$, the group of bijections on $\mathcal{D}$. Note that the group $G$ acts on $\mathcal{D}$ by defining $xg=g(x)$.333This is a well-defined action if we use the group multiplication $f\cdot g=g\circ f$. In the most studied instance, called the equality symmetry, $\mathcal{D}$ is a countably infinite set and $G=\operatorname{Sym}(\mathcal{D})$. In this paper, we will mostly focus on the total order symmetry given by $\mathcal{D}=\mathbb{Q}$ and $G=\{\pi\mid\pi\in\operatorname{Sym}(\mathbb{Q}),\pi\text{ is monotone}\}$.

Let $(\mathcal{D},G)$ be a data symmetry and $X$ be a $G$-set. A finite set of data values $S\subseteq\mathcal{D}$ is called a support of an element $x\in X$ if for all $g\in G$ with $\forall s\in S\colon sg=s$ we have $xg=x$. A $G$-set $X$ is called nominal if every element $x\in X$ has a (necessarily finite) support.

Example 2.1**.**

We list several examples for the total order symmetry $(\mathbb{Q},G)$. The set $\mathbb{Q}^{2}$ is a $G$-set, with the action defined by $(q_{1},q_{2})g=(g(q_{1}),g(q_{2}))$ for all $g\in G$. It is nominal, as each element $(q_{1},q_{2})\in\mathbb{Q}^{2}$ has the finite set $\{q_{1},q_{2}\}$ as a support. Indeed, if a monotone bijection $g\in G$ is the identity on $q_{1}$ and $q_{2}$ then we have $(q_{1},q_{2})g=(g(q_{1}),g(q_{2}))=(q_{1},q_{2})$ as required. The set $\mathbb{Q}^{2}$ has the following three orbits:

[TABLE]

To see this, note that each of these sets is closed under monotone permutations, and their union is the full set $\mathbb{Q}^{2}$.

For a set $X$, the set of all subsets of size $n\in\mathbb{N}$ is denoted by

[TABLE]

The set $\mathcal{P}_{n}(\mathbb{Q})$ is a single-orbit nominal set for each $n$, with the action defined by direct image: $Yg=\{yg\mid y\in Y\}$. Every set $Y\in\mathcal{P}_{n}(X)$ is a support of itself.

The group of monotone bijections also acts by direct image on the full power set $\mathcal{P}(\mathbb{Q})$, but this is not a nominal set. For instance, the set $\mathbb{Z}\in\mathcal{P}(\mathbb{Q})$ of integers has no finite support.

If $S\subseteq\mathcal{D}$ is a support of an element $x\in X$, then any finite set $S^{\prime}\subseteq\mathcal{D}$ such that $S\subseteq S^{\prime}$ is also a support of $x$. A set $S\subseteq\mathcal{D}$ is a least support of $x\in X$ if it is a support of $x$ and $S\subseteq S^{\prime}$ for any support $S^{\prime}$ of $x$. The existence of least supports is crucial for representing orbits. Unfortunately, even when elements have a finite support, in general they do not always have a least support. A data symmetry $(\mathcal{D},G)$ is said to admit least supports if every element of every nominal set has a least support. Both the equality and the total order symmetry admit least supports. For other (counter)examples of data symmetries admitting least supports, see [3]. Having least supports is useful for a finite representation.

Given a nominal set $X$, the size of the least support of an element $x\in X$ is denoted by $\dim(x)$, the dimension of $x$. We note that all elements in the orbit of $x$ have the same dimension. For an orbit-finite nominal set $X$, we define

[TABLE]

For a single-orbit nominal set $O$, observe that $\dim(O)=\dim(x)$ where $x$ is any element $x\in O$.

3 Automata over Nominal Sets

In this section we recall the notion of nominal automata, which allow to recognise languages over infinite alphabets. Nominal automata are defined as ordinary automata by replacing the finite state space and finite alphabet by orbit-finite nominal sets.

The theory of nominal automata is developed in [3], where it is shown that many algorithms from automata theory transfer to nominal automata. For instance, emptiness and equivalence of deterministic automata can be decided with a slight adaptation of the classical algorithms. Nonetheless, not all algorithms generalise: equivalence of non-deterministic automata is undecidable in the nominal setting. Below, we also briefly describe minimisation and learning of nominal automata. We start with an introductory example of a language over the rational numbers.

Example 3.1**.**

Consider the following language on rational numbers:

[TABLE]

We call this language the interval language as a word $w\in\mathbb{Q}^{\ast}$ is in the language when it denotes a sequence of nested intervals. For instance, the word $w=0\,2\,1\,\frac{3}{2}$ is in $\mathcal{L}_{\text{int}}$, but $w^{\prime}=0\,2\,1\,1$ is not. This language contains arbitrarily long words. For this language it is crucial to work with an infinite alphabet as for each finite set $C\subset\mathbb{Q}$, the restriction $\mathcal{L}_{\text{int}}\cap C^{\ast}$ is just a finite language. Note that the language is equivariant: $w\in\mathcal{L}_{\text{int}}\iff wg\in\mathcal{L}_{\text{int}}$ for any monotone bijection $g$, because nested intervals are preserved by monotone maps.444The $G$-action on words is defined point-wise: $(w_{1}\ldots w_{n})g=(w_{1}g)\ldots(w_{n}g)$. Indeed, $\mathcal{L}_{\text{int}}$ is a nominal set, although it is not orbit-finite.

Informally, the language $\mathcal{L}_{\text{int}}$ can be accepted by the automaton depicted in Figure 1. Here we allow the automaton to store rational numbers and compare them to new symbols. The input on a transition is denoted by the variable $a,b$ or $c$ which does not already appear in the source state. This input may be constrained by a guard. For example, the transition from $q_{2}$ to $q_{3}$ is taken if any value $c$ between $a$ and $b$ is read and then the currently stored value $a$ is replaced by $c$. For any other value read at state $q_{2}$ the automaton transitions to the sink state $q_{4}$. Such a transition structure is made precise by the notion of nominal automaton.

Remark 3.2**.**

For the reader familiar with register automata, Figure 1 resembles a register automaton. One notable difference to the classical definition of register automaton is that we allow each state to have a different set of registers. In this example, $q_{0}$ and $q_{4}$ have no registers, $q_{1}$ has a single register and the other states have two registers. This way, the values in the registers are always defined.

In general, register automata and nominal automata are equally expressive; a clear comparison is given by Bojańczyk [18]. Each state in a register automaton gives rise to one or more orbits in an equivalent nominal automaton. In fact, the number of orbits may be exponential in the number of states of the register automaton. These orbits represent distinct relations between registers.

Definition 3.3**.**

A nominal language is an equivariant subset $L\subseteq A^{*}$ where $A$ is an orbit-finite nominal set.

Definition 3.4**.**

A nominal deterministic finite automaton is a tuple $(S,A,F,\delta)$, where $S$ is an orbit-finite nominal set of states, $A$ is an orbit-finite nominal set of symbols, $F\subseteq S$ is an equivariant subset of final states and $\delta\colon S\times A\to S$ is the equivariant transition function.

Given a state $s\in S$, we define the usual acceptance condition: a word $w\in A^{*}$ is accepted if $w$ denotes a path from $s$ to a final state.

The automaton in Figure 1 can be formalised as a nominal deterministic finite automaton as follows. Let

[TABLE]

be the set of states, where the group action is defined as one would expect. The transition we described earlier can now be defined formally as

[TABLE]

By defining $\delta$ on all states accordingly and defining the final states as

[TABLE]

we obtain a nominal deterministic automaton $(S,\mathbb{Q},F,\delta)$. The state $q_{0}$ accepts the language $\mathcal{L}_{\text{int}}$.

3.1 Minimisation of Nominal Automata

For languages recognised by nominal DFAs, a Myhill-Nerode theorem holds which relates states to right congruence classes [3]. This guarantees the existence of unique minimal automata. We say an automaton is minimal if its set of states has the least number of orbits and each orbit has the smallest dimension possible.555Abstractly, an automaton is minimal if it has no proper quotients. Minimal deterministic automata are unique up to isomorphism.

Example 3.5**.**

Consider the language

[TABLE]

consisting of those words where the last symbol is the maximum of previous symbols. Figure 2 depicts a nominal automaton accepting $\mathcal{L}_{\text{max}}$, which is however not minimal. Figure 3 is the minimal nominal automaton accepting $\mathcal{L}_{\text{max}}$.

There are several algorithms for minimising deterministic automata. In this paper we focus on Moore’s minimisation algorithm. It generalises to nominal DFAs since it uses set operations which work just as well on nominal sets (see Algorithm 1). We will perform a complexity analysis in Section 8 and later use this algorithm for testing our library.

3.2 Learning nominal automata

Another interesting application is automata learning. The aim of automata learning is to infer an unknown regular language $\mathcal{L}$. We use the framework of active learning as set up by Dana Angluin [26] where a learning algorithm can query an oracle to gather information about $\mathcal{L}$. Formally, the oracle can answer two types of queries:

membership queries, where a query consists of a word $w\in A^{*}$ and the oracle replies whether $w\in\mathcal{L}$, and 2. 2.

equivalence queries, where a query consists of an automaton $\mathcal{H}$ and the oracle replies positively if $\mathcal{L}(\mathcal{H})=\mathcal{L}$ or provides a counterexample if $\mathcal{L}(\mathcal{H})\neq\mathcal{L}$.

With these queries, the L⋆ algorithm can learn regular languages efficiently [26]. In particular, it learns the unique minimal automaton for $\mathcal{L}$ using only finitely many queries. The L⋆ algorithm has been generalised to $\nu$L⋆ in order to learn nominal regular languages [12]. In particular, it learns a nominal DFA (over an infinite alphabet) using only finitely many queries. The algorithm is not polynomial, unlike the minimisation algorithm described above. However, the authors of loc. cit. conjecture that there is a polynomial algorithm.666See joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html for a sketch of the polynomial algorithm. For the correctness, termination and comparison with other learning algorithms see loc. cit.

Learning register automata is an active research area with applications such as bug-finding in internet protocols [27]; see [13] for other applications. We will implement $\nu$L⋆ to test our library in Section 9.4.

4 Representing nominal sets

In this section we sketch the representation of nominal sets according to [3]. We will not need all the details, but we include it to give a rough idea of the used techniques, and to fix notation. As noted in Section 2.1, a $G$-set is always a disjoint union of its orbits. In order to represent an orbit-finite $G$-set, it is hence sufficient to represent each orbit.

An orbit $X$ of a $G$-set can always be represented as a quotient of $G$. To see this, pick some element $x\in X$ and consider the subgroup $H=\{g\in G\mid xg=x\}$. The set of cosets $G/H$ is acted on by $G$ via right-multiplication. One can check that $X$ is isomorphic to $G/H$ as $G$-sets (for the isomorphism, send $x$ to the equivalence class of $1$). So an orbit is defined by some subgroup $H$.

What is left is to represent the data $H$ is some finite way. This is where we need the fact that $x$ has a least support $C$. We use $C$ to define two subgroups of $H$. First, there are elements which leave each $c\in C$ fixed, but may move elements outside of $C$. Second, there are the “local symmetries” that act as the identity outside of $C$, but may permute the elements of $C$. The subgroup $H$ is generated by these two subgroups. We only need to know the local symmetries $S$. The whole reduction from an abstract orbit to this subgroup is stated in the following theorem from [3].

Theorem 4.1**.**

Let $X$ be a single-orbit nominal set for a data symmetry $(\mathcal{D},G)$ that admits least supports and let $C\subseteq\mathcal{D}$ be the least support of some element $x\in X$. Then there exists a subgroup $S\leq G|_{C}$ such that $X\cong[C,S]^{ec}$,

where we used the following notation. The restriction of a group $G$ to a subset $C\subseteq\mathcal{D}$ is defined as

[TABLE]

where $\pi|_{C}$ is the restriction of the bijection $\pi\colon\mathcal{D}\to\mathcal{D}$ to the domain $C$. The extension of a subgroup (of local symmetries) $S\leq G|_{C}$ is defined as

[TABLE]

Finally, for $C\subseteq\mathcal{D}$ and $S\leq G|_{C}$, we define the orbit of right-cosets

[TABLE]

5 Representation in the total order symmetry

This section develops a concrete representation (based on Theorem 4.1) of nominal sets over the total order symmetry, as well as equivariant maps and products. From now on, by nominal set we always refer to a nominal set over the total order symmetry. Hence, our data domain is $\mathbb{Q}$ and we take $G$ to be the group of monotone bijections.

5.1 Orbits and nominal sets

Our first observation is that the finite group of local symmetries $S$ in Theorem 4.1 is always trivial, i.e., $S$ is the trivial group, $I=\{1\}$. This follows from the following lemma and the fact that $S\leq G|_{C}$.

Lemma 5.1**.**

For every finite subset $C\subset\mathbb{Q}$, we have $G|_{C}=I$.

Proof.

Let $\pi\in G|_{C}$ be any element of $G|_{C}$. If $\pi$ is not the identity, then since $C$ is finite, there exists a smallest element $c\in C$ with $c\pi\neq c$. Since $\pi$ is a bijection mapping $C$ to $C$, we find $c\pi\pi\neq c\pi$ and $c\pi\in C$, hence $c<c\pi$. Furthermore, there exists some $c^{\prime}\in C$ with $c^{\prime}\pi=c$. Since by assumption $c^{\prime}\neq c$, also $c<c^{\prime}$. But then both $c<c^{\prime}$ and $c\pi>c=c^{\prime}\pi$, contradicting monotonicity of $\pi$. Hence $\pi$ is the identity element, and $G|_{C}=I$. ∎

Immediately, we see that $(C,S)=(C,I)$, and hence that the orbit is fully represented by the set $C$. Together with Theorem 4.1 this leads to a complete characterisation of $[C,I]^{ec}$ in Lemma 5.3. In its proof, we also need the following.

Lemma 5.2** (Homogeneity).**

For any two finite $C\subseteq\mathbb{Q}$, $C^{\prime}\subseteq\mathbb{Q}$, if $|C|=|C^{\prime}|$, then there is a $\pi\in G$ such that $C\pi=C^{\prime}$.

Proof.

This is shown through construction of $\pi$. Number the elements of $C$ from smallest to largest, such that $C(1)$ is the smallest element and $C(n)$ the largest. Do the same for $C^{\prime}$. We define $\pi$ such that $C(i)\pi=C^{\prime}(i)$, interpolating in between (see Figure 4 for a visualisation):

[TABLE]

Note that since $\frac{C^{\prime}(i)-C^{\prime}(i-1)}{C(i)-C(i-1)}>0$ for any $1<i\leq n$, $\pi$ is monotone. Furthermore, its inverse is given by swapping $C$ and $C^{\prime}$.

[TABLE]

Hence $\pi$ is a monotone bijection, and we conclude $\pi\in G$. ∎

Lemma 5.3**.**

Given a finite subset $C\subset\mathbb{Q}$, we have $[C,I]^{ec}\cong\mathcal{P}_{|C|}(\mathbb{Q})$.

Proof.

From Lemma 5.2 it follows that $\mathcal{P}_{|C|}(\mathbb{Q})$ consists of a single orbit. Given this, in combination with the fact that $C\in\mathcal{P}_{|C|}(\mathbb{Q})$, Theorem 4.1 gives a subgroup $S\leq G|_{C}$ such that $\mathcal{P}_{|C|}(\mathbb{Q})\cong[C,S]^{ec}$. Since $S\leq G|_{C}$, Lemma 5.1 implies $S=I$. This proves that $[C,I]^{ec}\cong\mathcal{P}_{|C|}(\mathbb{Q})$. ∎

By Theorem 4.1 and the above lemmas, we can represent an orbit by a single integer $n$, the size of the least support of its elements.

Corollary 5.4**.**

Let $X$ be an orbit-finite nominal set. Then $X\cong\mathcal{P}_{\dim(X)}(\mathbb{Q})$.

Proof.

By Theorem 4.1, we get $C$ and $S\leq G|_{C}$ such that $X\cong[C,S]^{ec}$. By Lemma 5.1, $S=I$, and by Lemma 5.3 we get

[TABLE]

But $|C|=\dim(X)$, since $C$ is the least support of some element $x\in X$. ∎

This naturally extends to (orbit-finite) nominal sets with multiple orbits by using a multiset of natural numbers, representing the size of the least support of each of the orbits. These multisets are formalised here as functions $f\colon\mathbb{N}\rightarrow\mathbb{N}$.

Definition 5.5**.**

Given a function $f\colon\mathbb{N}\rightarrow\mathbb{N}$, we define a nominal set $\llbracket f\rrbracket$ by

[TABLE]

Proposition 5.6**.**

For every orbit-finite nominal set $X$, there is a unique function $f\colon\mathbb{N}\to\mathbb{N}$ such that $X\cong\llbracket f\rrbracket$ and the set $\{n\mid f(n)\neq 0\}$ is finite.

Proof.

We start by proving the existence. For this, grade $X$ by the dimension of its elements, defining $X_{i}=\{x\in X\mid\dim(x)=i\}$. Now split each $X_{i}$ up into its $k_{i}$ orbits $O_{i,j}$, such that

[TABLE]

By Corollary 5.4, we have $O_{i,j}\cong\{j\}\times\mathcal{P}_{i}(\mathbb{Q})$ for each orbit $O_{i,j}$.

Define $f\colon\mathbb{N}\rightarrow\mathbb{N}$ such that $f(i)=k_{i}$. Then $\{n\mid f(n)\neq 0\}$ is finite, since $X$ is orbit-finite. Writing this out gives

[TABLE]

Next, we need to show that $f$ is unique. Suppose $g\colon\mathbb{N}\rightarrow\mathbb{N}$ also represents $X$, e.g. $X\cong\llbracket g\rrbracket$. Then it follows that $\llbracket f\rrbracket\cong\llbracket g\rrbracket$. Let $h\colon\llbracket f\rrbracket\rightarrow\llbracket g\rrbracket$ be the isomorphism. Grade $\llbracket f\rrbracket$ and $\llbracket g\rrbracket$, letting $\llbracket f\rrbracket_{i}=\{x\in\llbracket f\rrbracket\mid\dim(x)=i\}$, and similarly for $\llbracket g\rrbracket_{i}$. Since $h$ is an isomorphism, we have for any $x\in\llbracket f\rrbracket$ that $\dim(h(x))=\dim(x)$, implying $h(\llbracket f\rrbracket_{i})=\llbracket g\rrbracket_{i}$. Furthermore, the fact that $h$ is an isomorphism gives $\operatorname{N}(h(\llbracket f\rrbracket_{i}))=\operatorname{N}(\llbracket f\rrbracket_{i})$. Using $\operatorname{N}(\llbracket f\rrbracket_{i})=f(i)$, we find that $f(i)=\operatorname{N}(\llbracket f\rrbracket_{i})=\operatorname{N}(h(\llbracket f\rrbracket_{i}))=\operatorname{N}(\llbracket g\rrbracket_{i})=g(i)$. Hence $f=g$, proving that $f$ is unique. ∎

Example 5.7**.**

Consider the set $\mathbb{Q}\times\mathbb{Q}$. The elements $(a,b)$ split in three orbits, one for $a<b$, one for $a=b$ and one for $a>b$. These have dimension 2, 1 and 2 respectively, so the set $\mathbb{Q}\times\mathbb{Q}$ is represented by the multiset $\{1,2,2\}$.

Remark 5.8**.**

The representation in terms of a function $f\colon\mathbb{N}\rightarrow\mathbb{N}$ enforces that there are only finitely many orbits of any given dimension. The first part of the above proposition generalises to arbitrary nominal sets by replacing the codomain of $f$ by the class of all sets and adapting Definition 5.5 accordingly. However, the choice of function $f$ is no longer unique in that case—this is avoided in the finite case by using natural numbers instead of finite sets.

5.2 Equivariant maps

We show how to represent equivariant maps, using two basic properties. Let $f\colon X\to Y$ be an equivariant map. The first property is that the direct image of an orbit (in $X$) is again an orbit (in $Y$), that is to say, $f$ is defined ‘orbit-wise’. Second, equivariant maps cannot introduce new elements in the support (but they can drop them). More precisely:

Lemma 5.9**.**

Let $f\colon X\to Y$ be an equivariant map, and $O\subseteq X$ a single orbit. The direct image $f(O)=\{f(x)\mid x\in O\}$ is a single-orbit nominal set.

Proof.

Let $y$ and $y^{\prime}$ both be elements of $f(O)$. To show that $f(O)$ is single-orbit, we need to construct a $\pi\in G$ such that $y\pi=y^{\prime}$. By definition of $f(O)$, there exist $x\in O$, $x^{\prime}\in O$ such that $f(x)=y$ and $f(x^{\prime})=y^{\prime}$. Since $O$ is single-orbit, there exists a $\pi\in G$ such that $x\pi=x^{\prime}$. As $f$ is an equivariant function, we find $y\pi=f(x)\pi=f(x\pi)=f(x^{\prime})=y^{\prime}$. This proves that $f(O)$ is single-orbit. ∎

Lemma 5.10**.**

Let $f\colon X\to Y$ be an equivariant map between two nominal sets $X$ and $Y$. Let $x\in X$ and let $C$ be a support of $x$. Then $C$ supports $f(x)$.

Proof.

Let $\pi\in G$ be such that $\forall c\in C,c\pi=c$. Then since $C$ is the support of $x$, $x\pi=x$. But then also $f(x)\pi=f(x\pi)=f(x)=f(x)$. Hence $C$ is a support of $f(x)$. Then, by definition, the least support of $f(x)$ is contained in $C$. ∎

Hence, equivariant maps are fully determined by associating two pieces of information for each orbit in the domain: the orbit on which it is mapped and a string denoting which elements of the least support of the input are preserved. These ingredients are formalised in the first part of the following definition. The second part describes how these ingredients define an equivariant function. Proposition 5.12 below then states that every equivariant function can be described in this way.

Definition 5.11**.**

Let $H=\{(I_{1},F_{1},O_{1}),\ldots,(I_{n},F_{n},O_{n})\}$ be a finite set of tuples where the $I_{i}$’s are disjoint single-orbit nominal sets, the $O_{i}$’s are single-orbit nominal sets with $\dim(O_{i})\leq\dim(I_{i})$ and the $F_{i}$’s are bit strings of length $\dim(I_{i})$ with exactly $\dim(O_{i})$ ones.

Given a set $H$ as above, we define $f_{H}\colon\bigcup I_{i}\to\bigcup O_{i}$ as the unique equivariant function such that, given $x\in I_{i}$ with least support $C$, $f_{H}(x)$ is the unique element of $O_{i}$ with support $\{C(j)\mid F_{i}(j)=1\}$, where $F_{i}(j)$ is the $j$-th bit of $F_{i}$ and $C(j)$ is the $j$-th smallest element of $C$.

Proposition 5.12**.**

For every equivariant map $f\colon X\rightarrow Y$ between orbit-finite nominal sets $X$ and $Y$ there exists a unique set $H$ as in Definition 5.11 such that $f=f_{H}$.

Proof.

We start with showing existence by construction. Split $X$ into its constituent orbits, call them $I_{1}$ through $I_{n}$. For each of these, select an element $e_{i}\in I_{i}$. Let $O_{i}$ be the orbit of $f(e_{i})$. By Lemma 5.9, $f(I_{i})=O_{i}$. For each $e_{i}$, let $C_{i}$ be the least support of $e_{i}$ and $C^{\prime}_{i}$ the least support of $f(e_{i})$. Let $F_{i}$ be the string with $F_{i}(j)=1$ if $C_{i}(j)\in C^{\prime}_{i}$, and $F_{i}(j)=0$ otherwise. Let $H=\{(I_{i},F_{i},O_{i})\mid i\in\{1,\ldots,n\}\}$. By construction, $f_{H}(e_{i})$ is the unique element of $O_{i}$ with support $C^{\prime}_{i}\cap C_{i}$. By Lemma 5.10, $C^{\prime}_{i}\cap C_{i}=C^{\prime}_{i}$, implying $f_{H}(e_{i})=f(e_{i})$. Since both are equivariant functions with the same domain, we have $f(x)=f_{H}(x)$ for all $x\in X$. Hence $f=f_{H}$.

To show that $H$ is unique, consider an $H^{\prime}$ such that $f=f_{H^{\prime}}$. As a consequence, we have $f_{H}=f_{H^{\prime}}$. From the definition of orbits it follows immediately that the split of $X$ into $I_{i}$ is unique up to the choice of indices, so that we can label the tuples $(I_{i}^{\prime},F_{i}^{\prime},O_{i}^{\prime})$ in $H^{\prime}$ such that $I_{i}^{\prime}=I_{i}$. It then follows that $O_{i}=f_{H}(I_{i})=f_{H^{\prime}}(I^{\prime}_{i})=O^{\prime}_{i}$. To show $F_{i}=F_{i}^{\prime}$, consider an $x\in I_{i}$. Let $C$ denote the least support of $x$, and $C_{f}$ the least support of $f(x)$. By definition of $f_{H}$ and $f_{H^{\prime}}$, it follows that $\{C(j)\mid F_{i}(j)=1\}=C_{x}=\{C(j)\mid F_{i}^{\prime}(j)$. But this is only possible if $F_{i}=F_{i}^{\prime}$, and hence $H=H^{\prime}$. ∎

Example 5.13**.**

Consider the function $\min\colon\mathcal{P}_{3}(\mathbb{Q})\rightarrow\mathbb{Q}$ which returns the smallest element of a 3-element set. Note that both $\mathcal{P}_{3}(\mathbb{Q})$ and $\mathbb{Q}$ are single orbits. Since for the orbit $\mathcal{P}_{3}(\mathbb{Q})$ we only keep the smallest element of the support, we can thus represent the function $\min$ with $\{(\mathcal{P}_{3}(\mathbb{Q}),100,\mathbb{Q})\}$.

Example 5.14**.**

Consider the (right) projection $\pi_{2}\colon\mathbb{Q}\times\mathbb{Q}\rightarrow\mathbb{Q}$. Recall from Example 5.7 that the set $\mathbb{Q}\times\mathbb{Q}$ has three orbits $Q_{1}=\{(a,b)\mid a<b\}$, $Q_{2}=\{(a,b)\mid a=b\}$ and $Q_{3}=\{(a,b)\mid a>b\}$. The function $\pi_{2}$ is represented by $\{(Q_{1},01,\mathbb{Q}),(Q_{2},1,\mathbb{Q}),(Q_{3},10,\mathbb{Q})$.

5.3 Products

The product $X\times Y$ of two nominal sets is again a nominal set and hence it can be represented itself in terms of the dimension of each of its orbits as shown in Section 5.1. However, this approach has some disadvantages.

Example 5.15**.**

We start by showing that the orbit structure of products can be non-trivial. Consider the product of $X=\mathbb{Q}$ and the set ${Y=\{(a,b)\in\mathbb{Q}^{2}\mid a<b\}}$. This product consists of five orbits, more than one might naively expect from the fact that both sets are single-orbit:

[TABLE]

We find that this product is represented by the multiset $\{2,2,3,3,3\}$. Unfortunately, this is not sufficient to accurately describe the product as it abstracts away from the relation between its elements with those in $X$ and $Y$. In particular, it is not possible to reconstruct the projection maps from such a representation.

The essence of our representation of products is that each orbit $O$ in the product $X\times Y$ is described entirely by the dimension of $O$ together with the two (equivariant) projections $\pi_{1}\colon O\to X$ and $\pi_{2}\colon O\to Y$. This combination of the orbit and the two projection maps can already be represented using Propositions 5.6 and 5.12. However, as we will see, a combined representation for this has several advantages. For discussing such a representation, let us first introduce what it means for tuples of a set and two functions to be isomorphic:

Definition 5.16**.**

Given nominal sets $X,Y,Z_{1}$ and $Z_{2}$, and equivariant functions $l_{1}\colon Z_{1}\to X$, $r_{1}\colon Z_{1}\to Y$, $l_{2}\colon Z_{2}\to X$ and $r_{2}\colon Z_{2}\to Y$, we define $(Z_{1},l_{1},r_{1})\cong(Z_{2},l_{2},r_{2})$ if there exists an isomorphism $h\colon Z_{1}\to Z_{2}$ such that $l_{1}=l_{2}\circ h$ and $r_{1}=r_{2}\circ h$.

Our goal is to have a representation that, for each orbit $O$, produces a tuple $(A,f_{1},f_{2})$ isomorphic to the tuple $(O,\pi_{1},\pi_{2})$. The next lemma gives a characterisation that can be used to simplify such a representation.

Lemma 5.17**.**

Let $X$ and $Y$ be nominal sets and $(x,y)\in X\times Y$. If $C$, $C_{x}$ and $C_{y}$ are the least supports of $(x,y)$, $x$ and $y$ respectively, then $C=C_{x}\cup C_{y}$.

Proof.

Let $\pi\in G$ be a group element such that $\forall c\in C_{x}\cup C_{y},c\pi=c$. Then $(x,y)\pi=(x\pi,y\pi)=(x,y)$ since $C_{x}$ and $C_{y}$ are supports of $x$ and $y$ respectively. Hence $C_{x}\cup C_{y}$ is a support of $x$, and since $C$ is the least support of $x$, $C\subseteq C_{x}\cup C_{y}$.

Now suppose that $C$ is strictly smaller than $C_{x}\cup C_{y}$. Then there is an element $c\in C_{x}\cup C_{y}$ with $c\notin C$. Without loss of generality we can assume $c\in C_{x}$. The set $(C_{x}\cup C_{y})\setminus\{c\}$ is not a support of $x$, since the least support $C_{x}$ of $x$ is not contained in $(C_{x}\cup C_{y})\setminus\{c\}$. Hence, there is some $\pi\in G$ such that $\forall c^{\prime}\in(C_{x}\cup C_{y})\setminus\{c\},c^{\prime}\pi=c^{\prime}$, but $x\pi\neq x$. For this $\pi$, we have $(x,y)\pi=(x\pi,y\pi)\neq(x,y)$. However, $(C_{x}\cup C_{y})\setminus\{c\}$ is a support of $(x,y)$, since $C\subseteq(C_{x}\cup C_{y})\setminus\{c\}$. Hence $(x,y)\pi=(x,y)$, yielding a contradiction. ∎

With Proposition 5.12 we represent the maps $\pi_{1}$ and $\pi_{2}$ by tuples $(O,F_{1},O_{1})$ and $(O,F_{2},O_{2})$ respectively. Using Lemma 5.17 and the definitions of $F_{1}$ and $F_{2}$, we see that at least one of $F_{1}(i)$ and $F_{2}(i)$ equals $1$ for each $i$.

We can thus combine the strings $F_{1}$ and $F_{2}$ into a single string $P\in\{L,R,B\}^{*}$ as follows. We set $P(i)=L$ when only $F_{1}(i)$ is $1$, $P(i)=R$ when only $F_{2}(i)$ is $1$, and $P(i)=B$ when both are $1$. The string $P$ fully describes the strings $F_{1}$ and $F_{2}$. This process for constructing the string $P$ gives it two useful properties:

The number of $L$s and $B$s in the string $P$ equals the dimension of $O_{1}$.

• 2.

The number of $R$s and $B$s in the string $P$ equals the dimension of $O_{2}$.

We will call strings $P$ with the above two properties valid (with respect to $O_{1},O_{2}$).

Thus, to describe a single orbit of the product $X\times Y$, a valid string $P$ together with the images of $\pi_{1}$ and $\pi_{2}$ is sufficient. This is stated more precisely in Proposition 5.20.

Definition 5.18**.**

Let $O_{1}\subseteq X$, $O_{2}\subseteq Y$ be single-orbit sets, and let $P\in\{L,R,B\}^{*}$ be a valid string with respect to $O_{1},O_{2}$. Define

[TABLE]

where $H_{i}=\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{i},O_{i})\}$ and the string $F_{1}$ is defined as the string $P$ with $L$s and $B$s replaced by $1$s and $R$s by [math]s. The string $F_{2}$ is similarly defined with the roles of $L$ and $R$ swapped.

This construction generates orbits of $X\times Y$:

Lemma 5.19**.**

Let $(P,O_{1},O_{2})$ be a tuple as in Definition 5.18. Then we have $\llbracket(P,O_{1},O_{2})\rrbracket\cong(O,\pi_{1},\pi_{2})$ for some orbit $O\subseteq X\times Y$.

Proof.

Let $(O^{\prime},f,g)=\llbracket(P,O_{1},O_{2})\rrbracket$. By construction, we find $f(O^{\prime})\subseteq X$ and $g(O^{\prime})\subseteq Y$. Denote by $\langle f,g\rangle\colon O^{\prime}\rightarrow X\times Y$ the pairing, i.e., $\langle f,g\rangle(x)=(f(x),g(x))$. By Lemma 5.9, since $O^{\prime}$ is single-orbit, so is $\langle f,g\rangle(O^{\prime})$. The latter is an orbit of $X\times Y$.

We now show that $\langle f,g\rangle$ is an isomorphism. First, by construction of $f$ and $g$, we find that if $C$ is the least support of $x\in O^{\prime}$, then $C$ is also the least support of $(f(x),g(x))$, since every element in the support of $x$ is in at least one of the least supports of $f(x)$ and $g(x)$, and by Lemma 5.17, the least support of $(f(x),g(x))$ is the union of the least supports of $f(x)$ and $g(x)$. This implies that the elements of both $O^{\prime}$ and $\langle f,g\rangle(O^{\prime})$ have the same support size. Since both $O^{\prime}$ and $\langle f,g\rangle(O^{\prime})$ are single-orbit, this makes $\langle f,g\rangle$ a bijection. Hence,

[TABLE]

The following result shows that every orbit of $X\times Y$ arises in this way, up to isomorphism.

Proposition 5.20**.**

For every orbit $O\subseteq X\times Y$ there is a unique tuple $(P,O_{1},O_{2})$ such that $O_{1}\subseteq X$, $O_{2}\subseteq Y$ are orbits, $P$ is a valid string and

[TABLE]

Proof.

Let us start by constructing such a tuple $(P,O_{1},O_{2})$ for a given orbit $O\subseteq X\times Y$. Since $O$ is an orbit, Lemma 5.12 provides two tuples $(O,F_{1},O_{1})$ and $(O,F_{2},O_{2})$ with $O_{1}$ an orbit of $X$ and $O_{2}$ an orbit of $Y$ such that $\pi_{1}|_{O}=f_{\{(O,F_{1},O_{1})\}}$ and $\pi_{2}|_{O}=f_{\{(O,F_{2},O_{2})\}}$. Now construct $P$ as the sequence of length $\dim(O)$ as follows:

[TABLE]

This covers all cases, since Lemma 5.17 guarantees that it will never be the case that the $i$-th letters of $F_{1}$ and $F_{2}$ are both [math].

We first show that $P$ is valid. To see this, observe that by Definition 5.11, each $1$ in the string $F_{1}$ corresponds to a unique element in the least support of an element of $O_{1}$. Hence $\dim(O_{1})=|F_{1}|$. By definition of $F_{1}$ we find $\dim(O_{1})=|F_{1}|=|P|_{L}+|P|_{B}$. A similar line of reasoning, replacing $L$ with $R$, shows $\dim(O_{2})=|F_{2}|=|P|_{R}+|P|_{B}$.

To show that the correspondence is bijective, we first show that, given an orbit $O\subseteq X\times Y$, if $(P,O_{1},O_{2})$ is the corresponding triple then

[TABLE]

Let $n=\dim(O)$. By Corollary 5.4, we have $\mathcal{P}_{n}(\mathbb{Q})\cong O$. Let $g\colon O\stackrel{{\scriptstyle\cong}}{{\rightarrow}}\mathcal{P}_{n}(\mathbb{Q})$ be the isomorphism between them. Then $f_{\{(O,F_{1},O_{1})\}}=f_{\{(\mathcal{P}_{|F_{1}|}(\mathbb{Q}),F_{1},O_{1})\}}\circ g$ and $f_{\{(O,F_{2},O_{2})\}}=f_{\{(\mathcal{P}_{|F_{2}|}(\mathbb{Q}),F_{2},O_{2})\}}\circ g$. As a consequence, we have

[TABLE]

By Definition 5.18 and the above construction of $P$, the right-hand side of the above equation equals $\llbracket(P,O_{1},O_{2})\rrbracket$. Hence, $(O,\pi_{1}|_{O},\pi_{2}|_{O})\cong\llbracket(P,O_{1},O_{2})\rrbracket$.

Finally, for uniqueness, consider two tuples $(P,O_{1},O_{2})$ and $(P^{\prime},O_{1}^{\prime},O_{2}^{\prime})$, such that $\llbracket(P,O_{1},O_{2})\rrbracket\cong\llbracket(P^{\prime},O_{1}^{\prime},O_{2}^{\prime})\rrbracket$. We let $F_{1}$ and $F_{2}$ denote the strings from Definition 5.18 for $\llbracket(P,O_{1},O_{2})\rrbracket$, and similarly $F_{1}^{\prime}$ and $F_{2}^{\prime}$ the strings for $\llbracket(P^{\prime},O_{1}^{\prime},O_{2}^{\prime})\rrbracket$.

Since $\llbracket(P,O_{1},O_{2})\rrbracket\cong\llbracket(P^{\prime},O_{1}^{\prime},O_{2}^{\prime})\rrbracket$ we have $\mathcal{P}_{|P|}(\mathbb{Q})\cong\mathcal{P}_{|P^{\prime}|}(\mathbb{Q})$, hence $|P|=|P^{\prime}|$. Furthermore, by the isomorphism, for any $x\in\mathcal{P}_{|P|}(\mathbb{Q})$, there exists an $x^{\prime}\in\mathcal{P}_{|P^{\prime}|}(\mathbb{Q})$ such that

[TABLE]

Since $O_{1}$, $O_{2}$, $O_{1}^{\prime}$ and $O_{2}^{\prime}$ single-orbit, this implies $O_{1}=O_{1}^{\prime}$ and $O_{2}=O_{2}^{\prime}$.

Moreover, by Lemma 5.17, the least support of any element $x\in\mathcal{P}_{|P|}(\mathbb{Q})$ equals the least support of $(f_{\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{1},O_{1})\}}(x),f_{\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{2},O_{2})\}}(x))$. But if we choose $x^{\prime}$ corresponding to $x$ as in the previous paragraph, then by (1) we obtain that the least support of $x$ equals the least support of $x^{\prime}$. Hence $x=x^{\prime}$. But this implies that $f_{\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{1},O_{1})\}}=f_{\{(\mathcal{P}_{|P^{\prime}|}(\mathbb{Q}),F_{1}^{\prime},O_{1})\}}$ and $f_{\{(\mathcal{P}_{|P|}(\mathbb{Q}),F_{2},O_{2})\}}=f_{\{(\mathcal{P}_{|P^{\prime}|}(\mathbb{Q}),F_{2}^{\prime},O_{2})\}}$, hence also $F_{1}=F_{1}^{\prime}$ and $F_{2}=F_{2}^{\prime}$. But $F_{1}=F_{1}^{\prime}$ and $F_{2}=F_{2}^{\prime}$ can hold only if $P$ and $P^{\prime}$ are equal. From this, we conclude that $(P,O_{1},O_{2})=(P^{\prime},O_{1}^{\prime},O_{2}^{\prime})$. ∎

From the above proposition it follows that we can generate the product $X\times Y$ simply by enumerating all valid strings $P$ for all pairs of orbits $(O_{1},O_{2})$ of $X$ and $Y$. Given this, we can calculate the multiset representation of a product from the multiset representations of both factors.

Theorem 5.21**.**

For $X\cong\llbracket f\rrbracket$ and $Y\cong\llbracket g\rrbracket$ we have $X\times Y\cong\llbracket h\rrbracket$, where

[TABLE]

Proof.

Every string $P\in\{L,R,B\}^{*}$ of length $n$ with $|P|_{L}=n-j$, $|P|_{R}=n-i$ and $|P|_{B}=i+j-n$ satisfies the requirements of Lemma 5.20, and hence describes a unique orbit for every pair of orbits $O_{1}$ and $O_{2}$ where the least support of the elements of $O_{1}$ has size $i$, and the least support of elements of $O_{2}$ have size $j$. Combinatorics tells us that there are ${{n}\choose{j}}{{j}\choose{n-i}}$ such strings. Summing over all $i\geq 0$, $j\geq 0$ such that $i+j-n$, $n-j$ and $n-i$ are positive, and multiplying with the number of orbits of the required size gives the result. ∎

Example 5.22**.**

To illustrate some aspects of the above representation, let us use it to calculate the product of Example 5.15. First, we observe that both $\mathbb{Q}$ and $S=\{(a,b)\in\mathbb{Q}^{2}\mid a<b\}$ consist of a single orbit. Hence any orbit of the product corresponds to a triple $(P,\mathbb{Q},S)$, where the string $P$ satisfies $|P|_{L}+|P|_{B}=\dim(\mathbb{Q})=1$ and $|P|_{R}+|P|_{B}=\dim(S)=2$. We can now find the orbits of the product $\mathbb{Q}\times S$ by enumerating all strings satisfying these equations. This yields:

LRR, corresponding to the orbit $\{(a,(b,c))\mid a,b,c\in\mathbb{Q},a<b<c\}$,

• 2.

RLR, corresponding to the orbit $\{(b,(a,c))\mid a,b,c\in\mathbb{Q},a<b<c\}$,

• 3.

RRL, corresponding to the orbit $\{(c,(a,b))\mid a,b,c\in\mathbb{Q},a<b<c\}$,

• 4.

RB, corresponding to the orbit $\{(b,(a,b))\mid a,b\in\mathbb{Q},a<b\}$, and

• 5.

BR, corresponding to the orbit $\{(a,(a,b))\mid a,b\in\mathbb{Q},a<b\}$.

Each product string fully describes the corresponding orbit. To illustrate this, consider the string BR. The corresponding bit strings for the projection functions are $F_{1}=10$ and $F_{2}=11$. From the lengths of the string we conclude that the dimension of the orbit is $2$. The string $F_{1}$ further tells us that the left element of the tuple consists only of the smallest element of the support. The string $F_{2}$ indicates that the right element of the tuple is constructed from both elements of the support. Combining this, we find that the orbit is $\{(a,(a,b))\mid a,b\in\mathbb{Q},a<b\}$.

5.4 Summary

We summarise our concrete representation in the following table. Propositions 5.6, 5.12 and 5.20 correspond to the three rows in the table.

Notice that in the case of maps and products, the orbits are inductively represented using the concrete representation. As a base case we can represent single orbits by their dimension.

5.5 Comparison to Families of symmetries by Ciancia et al.

The representation we have derived so far is the same as in the work of Ciancia et al [24]. In this section we elaborate on this equivalence. Their particular result is an encoding of nominal sets (in a general sense) as objects in the category $\textbf{Fam}(\textbf{Sym}(\mathcal{C})^{\textrm{op}})$, for a suitably picked $\mathcal{C}$.

In our setting of the total order symmetry, we have to take $\mathcal{C}$ to be the small category of finite sets with monotone injections. Concretely, the objects of $\mathcal{C}$ are the sets $\{1,\ldots,n\}$ for each $n\in\mathbb{N}$ and the maps of $\mathcal{C}$ are injective and order-preserving functions $f\colon\{1,\ldots,n\}\to\{1,\ldots,m\}$. (Note that an object $\{1,\ldots,n\}$ can just as well be encoded by the number $n$.) By Lemma 5.1, we note that $\textbf{Sym}(\mathcal{C})$ is isomorphic to $\mathcal{C}$. And so their representation $\textbf{Fam}(\textbf{Sym}(\mathcal{C})^{\textrm{op}})\cong\textbf{Fam}(\mathcal{C}^{\textrm{op}})$ also consists of multisets of natural numbers, as does ours (see Table 1). The maps are encoded per member in the family, together with local (backwards) maps. We have specialised this encoding of maps as follows. A monotone injection $f\colon n\to m$ can be recovered from its image $\operatorname{Im}(f)\subseteq m$. Such a subset can be encoded as a bit string, which is what we use.

They also provide a concrete description of the categorical product, in terms of the multi-coproduct (see [24, Section 5]). We have shown that an element in the multi-coproduct can be represented concretely by a certain string.

Finally, we mention [24, Theorem 4.12] which states that there is an equivalence $\textbf{Fam}(\textbf{Sym}(\mathcal{C})^{\textrm{op}})\to\textbf{Set}^{\mathcal{C}}_{\diamond}$. Since we have the same representation of nominal sets, this suggests that the category of nominal sets over $(\mathbb{Q},<)$ is equivalent to the category $\textbf{Set}^{\mathcal{C}}_{\diamond}$ of (wide) pullback preserving functors from C to Set. However, in this paper we have not defined the categorical underpinnings to further elaborate on this equivalence.

6 C++ Implementation of Ons

The ideas outlined above have been implemented in the C++ library Ons.777Ons can be found at https://github.com/davidv1992/ONS The library can represent orbit-finite nominal sets and their products, (disjoint) unions and maps. A full technical description of what it can do, and how to use it, is given in the documentation included with Ons.

Let us start here by showing an example program to calculate the product of the sets $\{(a,b)\mid a<b\}$ and $\mathbb{Q}$ (see Example 5.22). The program below calculates this product, and then prints one element for each orbit of the result.

⬇

nomset<rational> A = nomset_rationals();

nomset<pair<rational, rational>> B({rational(1),rational(2)});

auto AtimesB = nomset_product(A, B); // compute the product

for (auto orbit : AtimesB)

cout << orbit.getElement() << "␣";

In the first line, we create a nominal set $A$, and initialise it with the built-in set $\mathbb{Q}$. The type of such a nominal set variable is nomset<T>, where $T$ is the type of the elements. In case of $A$ this is the rational type.

In the second line, we create the set $B$ containing the elements of $\{(a,b)\mid a<b\}$. To do this, we instruct the constructor of $B$ to create the minimal nominal set containing the element $(1,2)$. This creates the nominal set with the orbit of $(1,2)$, which is exactly the set $\{(a,b)\mid a<b\}$.

Having created these sets, it then computes the product using the function nomset_product. This returns the product, of type nomset<pair<A,B>>, where A and B are the types of the elements of $A$ and $B$ respectively. In our case, this means that the result is a nominal set containing elements of type pair<rational,pair<rational,rational>>.

Finally, we loop over the orbits of the result, stored in the variable AtimesB, with for (auto orbit : AtimesB). This returns an orbit object for each orbit in the nominal set AtimesB. These objects describe the properties of the individual orbits of a nominal set. We use it here to get an element (with .getElement()), which is printed through standard out.

Running this code gives the following output (‘/1’ signifies the denominator):

⬇

(1/1,(2/1,3/1)) (1/1,(1/1,2/1)) (2/1,(1/1,3/1))

(2/1,(1/1,2/1)) (3/1,(1/1,2/1))

We see here a list of five elements, each corresponding to a single orbit of the product $\mathbb{Q}\times\{(a,b)\mid a<b\}$.

6.1 Core functionality

The main implementation of nominal sets and equivariant functions in the Ons library is split up in three main concepts:

orbit<T>, representing orbits; 2. 2.

nomset<T>, representing nominal sets, containing a number of orbit<T> objects; 3. 3.

eqimap, equivariant functions.

The orbit<T> objects contain a complete description of a single orbit of elements of type $T$. They allow querying of basic properties such as the size of the least support (with .supportSize), checking whether an element is a member of the orbit (with .isElement) and extraction of sample elements (with .getElement).

Next, nomset<T> is used to represent entire sets. Its functionality includes checking whether an element or other set is contained in the set (with .contains), iterating over the orbits (see above) and querying for the size of the set (with .size).

For working with nominal sets, Ons also provides implementations of common set operations. Examples of these are set union (with nomset_union), intersection (with nomset_intersect) and set products (with nomset_product).

The Ons library also implements support for filtering (with nomset_filter) and mapping (with nomset_map) of nominal sets. These take an (equivariant) function as argument, which can either be given as an equivariant function object eqimap or as a C++ function or function object, as long as the resulting behaviour when invoked is equivariant.

Finally, objects of type eqimap can be used to represent dynamically generated equivariant functions. They implement an evaluation, allowing the application of the function to concrete argument values. They also contain several functions for querying properties of the function represented (such as whether elements are in its domain, with .inDomain), and manipulating the function represented (such as extending the mapping, with .add).

6.2 Another example

Let us now consider a slightly more complicated piece of code. It refines a relation $R$ (called previousPartition) on the states $Q$ of an automaton, using a transition function $f\colon Q\times A\rightarrow A$ (called transitionFunction), over an alphabet $A$ (called alphabet). It returns as a result the set

[TABLE]

The code is as follows.

⬇

template <typename Q, typename A>

nomset<pair<Q,Q>> refineRelation(

nomset<A> alphabet,

nomset<pair<Q,Q>> previousRelation,

eqimap<pair<Q,A>, Q> transitionFunction) {

*// calculate R x A*

nomset<pair<pair<Q,Q>,A>> transitions =

    nomset_product(previousRelation, alphabet);

*// Find those where (f(q,a), f(q’,a)) not in R*

nomset<pair<pair<Q,Q>,A>> invalid =

    nomset_filter(transitions, [&](pair<pair<Q,Q>,A> input) {

        Q state1 = input.first.first;

        Q state2 = input.first.second;

        A letter = input.second;

        Q result1 = transitionFunction({state1, letter});

        Q result2 = transitionFunction({state2, letter});

        **return** !previousRelation.contains({result1, result2});

    });

*// Strip away alphabet*

nomset<pair<Q,Q>> toRemove =

    nomset_map(invalid, [](pair<pair<Q,Q>,A> input) {

        **return** input.first;

    });

*// Calculate result*

**return** nomset_minus(previousRelation, toRemove);

}

This result is computed in four steps. First, it calculates the set of all transition pairs it still needs to consider (transitions), using nomset_product to calculate the product $R\times A$.

Next, it uses nomset_filter to select those elements $((q,q^{\prime}),a)$ for which $(f(q,a),f(q^{\prime},a))\notin R$. Note that the function which calculates this is specified as a plain C++ lambda, whose behaviour is equivariant.

For modifying the relation, only the first part of $((q,q^{\prime}),a)$ is relevant, so in the third step we use nomset_map to project out the alphabet letters of the witnesses in the set invalid.

This leaves the code with a set of pairs $(q,q^{\prime})$ which need to be removed from $R$ to produce the final result. This is calculated using the set minus operation nomset_minus, resulting in the refined partition.

7 Haskell Implementation of Ons

We have implemented a similar library in Haskell, called Ons-hs.888Available at https://github.com/Jaxan/ons-hs This showcases the generality of the theoretical characterisation in Section 5.

At the core, there is the type class Nominal.

⬇

type Orbit a :: *

toOrbit :: a -> Orbit a

getElement :: Orbit a -> Support -> a

support :: a -> Support

index :: Proxy a -> Orbit a -> Int

It provides to basic functionality, toOrbit and getElement, to convert between elements (of type a) and orbits of elements (of type Orbit a). The functions support and index are utility functions, returning the (least) support of an element, and the dimension of an orbit.

Instances are defined for basic data types such as the type of rational numbers, Atom. Other instances can be derived for any algebraic data structure (following Table 1). For example, the data type for the states of the automaton in Figure 1 can be defined as:

⬇

deriving (Eq, ...)

deriving Nominal via Generic State

Deriving instances with generics make it easy for the user to use the library. One can also easily define trivial instances, where the group action is defined as the identity function. This is used for the EquivariantSet data structure. This data type provides an interface to (infinite) nominal sets and the usual set constructions are defined. Some of these functions are shown below (for brevity, we have omitted the type class context from the type signatures).

⬇

deriving Nominal via Trivial (EquivariantSet a)

map :: (a -> b) -> EquivariantSet a -> EquivariantSet b

filter :: (a -> Bool) -> EquivariantSet a -> EquivariantSet a

product :: EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b)

rationals :: EquivariantSet Atom

Function arguments (in, e.g., map and filter) are required to be equivariant. Finally, a data type for equivariant maps, EquivariantMap is provided with the expected functions for a map data structure.

With these functions, we can define all the states of the automaton in Figure 1 and the accepting states can easily be filtered out.

⬇

<> map (uncurry Q2) (product rationals rationals)

<> map (uncurry Q3) (product rationals rationals)

acceptingStates = filter accept states where

accept (Q2 a b) = a < b

accept _ = False

8 Complexity of set operations

Since our implementations are directly based on representing orbits, it is possible to derive concrete complexities for the set operations. To simplify such an analysis, we make the following assumptions on operations on orbits:

The comparison of two orbits takes $O(1)$.

• 2.

Constructing an orbit from an element takes $O(1)$.

• 3.

Checking whether an element is in an orbit takes $O(1)$.

These assumptions are justified as each of these operations takes time proportional to the size of the representation of an individual orbit, which in practice is small and approximately constant. For instance, the orbit $\mathcal{P}_{n}(\mathbb{Q})$ is represented by just the integer $n$ and its type.

Furthermore, two of the operations considered make use of an external function. Since these can be implemented in a variety of ways, and the time complexity of actually invoking these functions is highly dependent both on what it calculates, and the specific way it is implemented in the program, we will here simply consider invocations of these functions to take $O(1)$ time.

For the notation in the following statement, recall that $\operatorname{N}(X)$ denotes the number of orbits of $X$, and $\dim(X)$ the maximal size of the least support of its elements.

Theorem 8.1**.**

If nominal sets are implemented with a tree-based set structure (as in Ons), the complexity of the following set operations is as follows:

[TABLE]

The functions $p\colon X\rightarrow 2$ and $f\colon X\rightarrow Y$ are user defined, and assumed to take $O(1)$ time per invocation.

Proof.

Each of the statements will be proven individually:

Membership. To decide $x\in X$, we first construct the orbit containing $x$, which is done in constant time. Then we use a logarithmic lookup to decide whether this orbit is in our set data structure. Hence membership checking is $O(\log(\operatorname{N}(X)))$.

Inclusion. We can check $X\subseteq Y$ in $O(N(X)\log(N(Y)))$ by repeated membership. It is also possible to do a simultaneous in-order traversal of both sets, which takes $O(N(X)+N(Y))$ time. The implementation uses a cutoff on the size of $X$ relative to $Y$ to deal with this, giving a time complexity of $O(min(N(X)+N(Y),N(X)\log(N(Y))))$.

Union and Intersection. A simultaneous traversal through both sets $X$ and $Y$ can be used to compute their union and intersection. This gives a complexity of $O(N(X)+N(Y))$ for intersections and unions.

Filtering. Filtering a nominal set $X$ using some equivariant predicate $p$ can be done in linear time, as the results are obtained in order, giving a complexity of $O(N(X))$, assuming the time complexity of the function $p$ to be constant.

Mapping. Mapping is a harder than filtering, as the outputs of $f$ may be out of order. Hence, for a tree-based implementation of sets, a sorting step is needed (or equivalently, iterated insertions), which gives a complexity to $O(N(X)\log(N(X)))$, again assuming the time complexity of the function $f$ to be constant.

Products. Calculating the product of two nominal sets is the most complicated construction. For each pair of orbits in the original sets $X$ and $Y$, all product orbits need to be generated. Each product orbit itself is constructed in constant time. By generating these orbits in-order, the resulting set takes $O(\operatorname{N}(X\times Y))$ time to construct.

We can also give an explicit upper bound for the number of orbits in terms of the input. Recall that orbits in a product are represented by strings of length at most $\dim(X)+\dim(Y)$. (If the string is shorter, we pad it with one of the symbols.) Since there are three symbols ($L,R$ and $B$), the product of $X$ and $Y$ will have at most $3^{\dim(X)+\dim(Y)}\operatorname{N}(X)\operatorname{N}(Y)$ orbits. It follows that taking products has time complexity of $O(3^{\dim(X)+\dim(Y)}\operatorname{N}(X)\operatorname{N}(Y))$. ∎

Using the above complexity results on individual operations, we can derive the complexity of algorithms using nominal sets. We will demonstrate this here using Moore’s algorithm. Recall from Section 3.1:

Theorem 8.2**.**

The runtime complexity of Moore’s algorithm on nominal deterministic automata is $O(3^{5k}k\operatorname{N}(S)^{3}\operatorname{N}(A))$, where $k=\dim(S\cup A)$.

Proof.

This is shown by counting operations, using the complexity results of set operations stated in Theorem 8.1. We first focus on the while loop on lines 2 through 5. The runtime of an iteration of the loop is determined by line 3, as this is the most expensive step. Since the dimensions of $S$ and $A$ are at most $k$, computing $S\times S\times A$ takes $O(\operatorname{N}(S)^{2}\operatorname{N}(A)3^{5k})$. Filtering $S\times S$ using that then takes $O(\operatorname{N}(S)^{2}3^{2k})$. The time to compute $S\times S\times A$ dominates, hence each iteration of the loop takes $O(\operatorname{N}(S)^{2}\operatorname{N}(A)3^{5k})$.

Next, we need to count the number of iterations of the loop. Each iteration of the loop gives rise to a new partition, which is a refinement of the previous partition. Furthermore, every partition generated is equivariant. Note that this implies that each refinement of the partition does at least one of two things: distinguish between two orbits of $S$ previously in the same element(s) of the partition, or distinguish between two members of the same orbit previously in the same element of the partition. The first can happen only $\operatorname{N}(S)-1$ times, as after that there are no more orbits lumped together. The second can only happen $\dim(S)$ times per orbit, because each such a distinction between elements is based on splitting on the value of one of the elements of the support. Hence, after $\dim(S)$ times on a single orbit, all elements of the support are used up. Combining this, the longest chain of partitions of $S$ has length at most $O(k\operatorname{N}(S))$.

Since each partition generated in the loop is unique, the loop cannot run for more iterations than the length of the longest chain of partitions on $S$. It follows that there are at most $O(k\operatorname{N}(S))$ iterations of the loop, giving the loop a complexity of $O(k\operatorname{N}(S)^{3}\operatorname{N}(A)3^{5k})$

The remaining operations outside the loop have a lower complexity than that of the loop, hence the complexity of Moore’s minimisation algorithm for a nominal automaton is $O(k\operatorname{N}(S)^{3}\operatorname{N}(A)3^{5k})$. ∎

The above theorem shows in particular that minimisation of nominal automata is fixed-parameter tractable (FPT) with the dimension as fixed parameter. The complexity of Algorithm 1 for nominal automata is very similar to the $O(|S|^{3}|A|)$ bound given by a naive implementation of Moore’s algorithm for ordinary DFAs. This suggest that it is possible to further optimise an implementation with similar techniques used for ordinary automata.

9 Evaluation

This section presents an experimental evaluation of Ons and Ons-hs, comparing them against existing tools in two tasks related to nominal automata: learning and minimisation.

9.1 The Tools: Ons, Ons-hs, N$\lambda$ and Lois

In order to evaluate our library Ons(-hs), we compare it against two existing libraries for computing with nominal sets, N$\lambda$ [19] and Lois [20, 21]. We briefly describe how these tools work and what the differences are with Ons.

Both N$\lambda$ and Lois work symbolically. Nominal sets are represented with set-builder expressions: values with variables and a first-order formula describing those values. For example, the orbit $\{\{a,b,c\}\mid a,b,c\in\mathbb{Q},a<b<c\}$ is represented simply as:

[TABLE]

(Here fromList takes a list and constructs a set.) In Ons, orbits are represented more compactly: in this case, the integer $3$ suffices. On the other hand, a set such as $\mathbb{Q}^{3}$ has a compact representation in N$\lambda$ and Lois:

[TABLE]

and a larger representation in Ons, consisting of 13 strings (see Section 5.3).

Since N$\lambda$ and Lois use formulas, many set operations are expressed by manipulating these formulas. One of the crucial operations is determining whether a set is empty, which can be resolved by checking satisfiability of the formula. To this end, these libraries use an SMT solver (by default, both libraries use Z3 [28]). Consequently, the runtime will depend on the size of these formulas, and both libraries have routines to simplify formulas.

9.2 Benchmarks

We evaluate the scalability of each library by implementing the automata minimisation algorithm and learning algorithm discussed in Section 3. These are then tested on the following three sets of automata.

Structured automata

We define the following automata.

• FIFO($n$)

Automata accepting valid traces of a finite FIFO data structure of size $n$. The alphabet is defined by two orbits: $\{\text{Put}(a)\mid a\in\mathbb{Q}\}$ and $\{\text{Get}(a)\mid a\in\mathbb{Q}\}$.

• $ww(n)$

Automata accepting the language of words of the form $ww$, where $w\in\mathbb{Q}^{n}$.

• $\mathcal{L}_{\text{max}}$

The language $\mathcal{L}_{\text{max}}$ where the last symbol is the maximum of previous symbols (Example 3.5).

• $\mathcal{L}_{\text{int}}$

The language accepting a series of nested intervals (Example 3.1).

The first two classes of structured automata are used as test cases in [12]. These two classes are also equivariant w.r.t. the equality symmetry. The structured automata can be encoded directly in symbolic form in N$\lambda$ or Lois. In Ons, this structure is lost and the algorithms operate purely on orbits. Where applicable, the automata listed above were generated using the same code as used in [12], ported to the other libraries as needed.

The automaton accepting the FIFO language is not minimal. It is based on the purely functional queue which has two lists of data values: one for pushing, one for popping. If the list for popping is empty, the list for pushing is reversed and moved to the list for popping [29]. The use of two lists is redundant and hence the automaton is not minimal.

Orbit-wise random automata

Besides structured automata, we generate orbit-wise random automata as follows. The input alphabet is always $\mathbb{Q}$ and the number of orbits and dimension $k$ of the state space $S$ are fixed. For each orbit in the set of states, its dimension is chosen uniformly at random between [math] and $k$, inclusive. Each orbit has a probability $\frac{1}{2}$ of consisting of accepting states.

To generate the transition function $\delta$, we enumerate the orbits of $S\times\mathbb{Q}$ and choose a target state uniformly from the orbits $S$ with small enough dimension. The bit string indicating which part of the support is preserved is then sampled uniformly from all valid strings. We will denote these automata as rand${}_{\operatorname{N}(S),k}$. The choices made here are arbitrary and only provide basic automata. We note that the automata are generated orbit-wise and this may favour our tool.

Random automata with formulae

The two classes above (orbit-wise random and structured) are very different in nature. The random ones are defined orbit-wise (which is an advantage for Ons), whereas the structured ones hardly use the values in an interesting way. To provide a middle-ground, we also generate random automata which use formulas on transitions.

For these automata, the state space is constructed from multiple copies of $\mathbb{Q}^{n}$. We will refer to these copies as locations and we will refer to the number of locations in the state space as the size of the automaton. We fix the size of the automaton, and then for each location we sample its dimension $n$ uniformly from $[0,k]$, where $k$ is a chosen constant. This creates the set of states. Every location has a probability $\frac{1}{2}$ of being accepting. Note that $\mathbb{Q}^{n}$ consists of more than one orbit if $n>1$, and consequently, the number of orbits in the state of the resulting automata can vary. The alphabet used is always the set $\mathbb{Q}$.

To generate the transition function, we generate a formula for each of the locations. This is done by creating a tree, where every node is one operation. The tree starts with an empty root, and is then expanded by repeatedly selecting one of the empty nodes and replacing it with either a logical operation (‘and’ or ‘or’) with two new empty nodes, or by a literal, i.e., a comparison between two variables (either $<$, $=$, or $>$). Both options occur with equal chance. In the latter case, the variables are drawn from either the state values or the input value. This process is repeated until either there are no more empty nodes, or the limit on the number of logical operators is reached, at which point the remaining empty nodes are filled with literals. Finally, for each node in the tree we randomly invert the output or not.

These formulas are then used to create two edges: one for when the formula is true, and one for when the formula is false. The target state is specified by randomly choosing a location, and randomly selecting which elements of the original state and input are kept in the target location (we allow for duplicate values).

Properties of the random automata

Our main motivation for using the above described random automata is the unavailability of a good source of nominal automata used in practical applications. However, this makes it difficult to judge whether or not our random automata are representative for actual performance in real test cases. We will show some properties of the generated automata so the reader can make their own judgement. In particular, we will focus primarily on the degree to which the size of the automata is reduced during minimisation.

For the orbit-wise generated automata, this is shown in Figure 5. It can be clearly seen that the vast majority of the generated automata is either minimal, or very close to being minimal.

In contrast, the data for the formula automata (see Figures 6 and 7) shows a much broader distribution, generating automata that use significantly more orbits than needed for the recognised languages.

Given this, we think that our test cases are varied enough to give a decent representation of the performance of the various libraries.

9.3 Minimisation Results

For N$\lambda$ and Lois we used the implementations of Moore’s minimisation algorithm from the original papers [19, 20, 21]. For each of the libraries, we wrote routines to read in an automaton from a file and, for the structured test cases, to generate the requested automaton. For Ons, all automata were read from file. The output of these programs was manually checked to see if the minimisation was performed correctly.

The results in Table 2 show a clear advantage for Ons for random automata. The library is capable of running all supplied test cases in less than one second. This in contrast to both Lois and N$\lambda$, which take more than $2$ hours on the largest random automata.

The results for structured automata show a clear effect of the extra structure. Both N$\lambda$ and Lois remain capable of minimising the automata in reasonable amounts of time for larger sizes. In contrast, Ons benefits little from the extra structure. Despite this, it remains viable: even for the larger cases it falls behind significantly only for the largest FIFO automaton and the two largest $ww$ automata.

The random automata with formulae show a mixed bag (as expected). (We have not implemented this for LOIS.) We note that when the number of locations grow, N$\lambda$ becomes rather slow. Nonetheless, N$\lambda$ catches up when increasing the dimension. All the results show that Ons(-hs) is faster in lower dimensions, even with a high number of orbits, but that N$\lambda$ and Lois can handle higher dimensions.

The libraries Ons and Ons-hs are very comparable in terms of scalability. However, we note that Ons-hs is sometimes faster, we expect this is due to the lazy nature of Haskell: When iterating through a set (especially those formed by products), breaking early means that the remainder of the set does not need to be constructed.

9.4 Learning Results

Both implementations in N$\lambda$ and Ons are direct implementations of the pseudocode for $\nu$L⋆ with no further optimisations. The authors of Lois implemented $\nu$L⋆ in their library as well.999Can be found on github.com/eryxcc/lois/blob/master/tests/learning.cpp They reported similar performance as the implementation in N$\lambda$ (private communication). Hence we focus our comparison on N$\lambda$ and Ons. We use the variant of $\nu$L⋆ where counterexamples are added as columns instead of prefixes.

The implementation in N$\lambda$ has the benefit that it can work with different symmetries. Indeed, the structured examples, FIFO and $ww$, are equivariant w.r.t. the equality symmetry as well as the total order symmetry. For that reason, we run the N$\lambda$ implementation using both the equality symmetry and the total order symmetry on those languages. For the languages $\mathcal{L}_{\text{max}}$, $\mathcal{L}_{\text{int}}$ and the random automata, we can only use the total order symmetry.

To run the $\nu$L⋆ algorithm, we implement an external oracle for the membership queries. This is akin to the application of learning black box systems [13]. For equivalence queries, we constructed counterexamples by hand. All implementations receive the same counterexamples. We measure CPU time instead of real time, so that we do not account for the external oracle.

The results in Table 3 show an advantage for Ons for random automata. Additionally, we report the number of membership queries, which can vary for each implementation as some steps in the algorithm depend on the internal ordering of set data structures.

We have not benchmarked the learning algorithm with the random automata with formulae. The reason is that the logical information, the formulae, are not even given to the learning algorithm, since the learning algorithm can only query the language.

In contrast to the case of minimisation, the results suggest that N$\lambda$ cannot exploit the logical structure of FIFO$(n)$, $\mathcal{L}_{\text{max}}$ and $\mathcal{L}_{\text{int}}$ as it is not provided a priori. For $ww(2)$ we inspected the output on N$\lambda$ and saw that it learned some logical structure. For example, it outputs $\{(a,b)\mid a\neq b\}$ as a single object instead of two orbits $\{(a,b)\mid a<b\}$ and $\{(a,b)\mid b<a\}$. This may explain why N$\lambda$ is still competitive. For languages which are equivariant for the equality symmetry, the N$\lambda$ implementation using the equality symmetry can learn with much fewer queries. This is expected as the automata themselves have fewer orbits. It is interesting to see that these languages can be learned more efficiently by choosing the right symmetry.

10 Related work

As stated in the introduction, N$\lambda$ [19] and Lois [20] use first-order formulas to represent nominal sets and use SMT solvers to manipulate them. This makes both libraries very flexible and they indeed implement the equality symmetry as well as the total order symmetry. As their representation is not unique, the efficiency depends on how the logical formulas are constructed. As such, they do not provide complexity results. In contrast, our direct representation allows for complexity results (Section 6) and leads to different performance characteristics (Section 9).

A second big difference is that both N$\lambda$ and Lois implement a “programming paradigm” instead of just a library. This means that they overload natural programming constructs in their host languages (Haskell and C++ respectively). For programmers this means they can think of infinite sets without having to know about nominal sets.

It is worth mentioning that an older (unreleased) version of N$\lambda$ implemented nominal sets with orbits instead of SMT solvers [30]. However, instead of characterising orbits (e.g., by its dimension), they represent orbits by a representative element. The authors of N$\lambda$ have reported that the current version is faster [19].

The theoretical foundation of our work is the main representation theorem in [3]. We add to that by instantiating it to the total order symmetry and distil a concrete representation of nominal sets. As far as we know, we provide the first implementation of the representation theory in [3].

Another tool using nominal sets is Mihda [31], where only the equality symmetry is implemented. This tool translates the $\pi$-calculus to history-dependent automata (HD-automata), with the aim of minimisation and checking bisimilarity. The implementation in OCaml is based on named sets, which are finite representations for nominal sets. The theory of named sets is well-studied and has been used to model various behavioural models with local names. For those results, the categorical equivalences between named sets, nominal sets and a certain (pre)sheaf category are exploited [24, 32, 33]. In particular, a finite representation similar to ours is presented in [24], see Section 5.5. The total order symmetry is not mentioned in their work.

Fresh OCaml [34] and Nominal Isabelle [35] are both specialised in name-binding and $\alpha$-conversion used in proof systems. They only use the equality symmetry and do not provide a library for manipulating nominal sets. Hence they are not suited for our applications.

On the theoretical side, there are many complexity results for register automata [5, 36]. In particular, we note that problems such as emptiness and equivalence are NP-hard depending on the type of register automaton. This does not easily compare to our complexity results for minimisation. One difference is that we use the total order symmetry, where the local symmetries are always trivial (Lemma 5.1). As a consequence, all the complexity required to deal with groups vanishes. Rather, the complexity is transferred to the input of our algorithms, because automata over the equality symmetry require more orbits when expressed over the total order symmetry. Another difference is that register automata allow for duplicate values in the registers. In nominal automata, such configurations will be encoded in different orbits. An interesting open problem is whether equivalence of unique-valued register automata is in Ptime [36].

Orthogonal to nominal automata, there is the notion of symbolic automata [4, 37]. These automata are also defined over infinite alphabets but they use predicates on transitions, instead of relying on symmetries. Symbolic automata are finite state (as opposed to infinite state nominal automata) and do not allow for storing values. However, they do allow for general predicates over an infinite alphabet, including comparison to constants.

11 Conclusion and Future Work

We presented a concrete finite representation for nominal sets over the total order symmetry. This allowed us to implement a library, Ons, and provide complexity bounds for common operations. The experimental comparison of Ons against existing solutions for automata minimisation and learning show that our implementation is much faster in many instances. As such, we believe Ons is a promising implementation of nominal techniques.

A natural direction for future work is to consider other symmetries, such as the equality symmetry. Here, we may take inspiration from existing tools such as Mihda (see Section 10). Another interesting question is whether it is possible to translate a nominal automaton over the total order symmetry which accepts an equality language to an automaton over the equality symmetry. This would allow one to efficiently move between symmetries. Finally, our techniques can potentially be applied to timed automata by exploiting the intriguing connection between the nominal automata that we consider and timed automata [25].

Acknowledgements

We would like to thank Szymon Toruńczyk and Eryk Kopczyński for their prompt help when using the Lois library. For general comments and suggestions we would like to thank Ugo Montanari and Niels van der Weide. At last, we want to thank the anonymous reviewers of ICTAC 2018 and this extended paper for their comments.