203 lines
No EOL
10 KiB
TeX
203 lines
No EOL
10 KiB
TeX
\project thesis
|
|
\startcomponent introduction
|
|
|
|
\startchapter
|
|
[title={Pakkende titel},
|
|
reference=chap:introduction]
|
|
|
|
\startsection
|
|
[title={Learning and Testing}]
|
|
|
|
\todo{Gekopieerd van test methods paper.}
|
|
|
|
Finite state machine conformance testing is a core topic in testing literature that is relevant for communication protocols and other reactive systems.
|
|
The combination of conformance testing and automata learning is applied in practice and it proves to be an effective way of finding bugs \cite[Joeri], replacing legacy software \cite[Philips], or inferring models to be used in model checking \cite[MeinkeSindhu].
|
|
|
|
Several model learning applications:
|
|
learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learning the TCP protocol \cite[DBLP:conf/cav/Fiterau-Brostean16] and learning the MQTT protocol \cite[DBLP:conf/icst/TapplerAB17].
|
|
|
|
|
|
\stopsection
|
|
\startsection
|
|
[title={Nominal Techniques}]
|
|
|
|
The theory of nominal sets has been introduced to cope with name binding.
|
|
Dealing with names is very common in computer science and several techniques exist to do this.
|
|
For example, one can use a meta language to talk about bound and free variables.
|
|
This is easy enough to use in theoretical research, but can be a burden to implement (there is quite a bit of bookkeeping).
|
|
Another way is to use some sort of normal form, for example, by naming things with numbers (sequentially).
|
|
One example of such a numbering scheme is using de Bruijn indices.
|
|
|
|
|
|
\citet[GabbayP02] introduced a third option, based on nominal techniques.
|
|
Instead of relying on the meta level, we declare names to really exist:
|
|
\startformula
|
|
\atoms = \{ a, b, c, \ldots \}.
|
|
\stopformula
|
|
Here we understand that $a$ and $b$ are different names and these names can be directly used in lambda terms or other objects.
|
|
(These names do not stand for variables!
|
|
The names exist in their own right.)
|
|
As a consequence, we can describe lambda terms such as
|
|
\startformula
|
|
\lambda x . a \quad \text{and} \quad \lambda x . b \, .
|
|
\stopformula
|
|
These two lambda terms are distinct, since they are constructed with different names.
|
|
In order to talk about equivalence, we introduce permutations.
|
|
If we write $\swap{a}{b}$ for the permutation which swaps $a$ and $b$, then we can relate the two lambda terms as follows.
|
|
\startformula
|
|
\swap{a}{b} \lambda x . a = \lambda x . b
|
|
\stopformula
|
|
How the permutations act on objects other than names will be explained later.
|
|
This way we can relate the two terms, without talking about free or bound variables.
|
|
We only talk about the names and permutations we declared.
|
|
|
|
The idea that names and permutations are sufficient was picked up by \citet[DBLP:journals/corr/BojanczykKL14].
|
|
They show that besides abstract syntax, nominal techniques are also interesting when modelling automata over infinite alphabets.
|
|
Here the infinite alphabet will be the set of names and the automaton should respect the permutations.
|
|
We will see why this is a natural way to model such automata in the next section.
|
|
\todo{\pi-calculus en named sets door mensen in Pisa.}
|
|
|
|
\startsubsection
|
|
[title={What is a nominal set?}]
|
|
|
|
Before we dive into the relation with automata, we will define the notion of nominal sets.
|
|
|
|
\startdefinition
|
|
Fix a countable, infinite set $\atoms = \{ a, b, \ldots \}$ of \emph{names} (sometimes called \emph{atoms}).
|
|
The elements of $\atoms$ bare no relationship to natural numbers, or other standard mathematical entities.
|
|
|
|
Define $\Pm = \{ \pi \colon \atoms \to \atoms \mid \pi \text{ is bijective} \}$ to be the set of permutations of names.
|
|
Together with function composition, $\Pm$ forms a group.
|
|
For two elements $a$ and $b$ we define a particular bijection $\swap{a}{b} \in \Pm$ which swaps $a$ and $b$ and leaves all other elements fixed.
|
|
\stopdefinition
|
|
|
|
It is good to stress that the set of names has no other structure defined on it.
|
|
The names are abstract entities which can be compared for equality, but nothing else.
|
|
\footnote{We can have more structure on the set of atoms, this is discussed in \in{Section}[].}
|
|
This also means that although $a$ and $b$ are distinct names, they are interchangeable.
|
|
If we write $a \in \atoms$, then $a$ can stand for any of the names.
|
|
So if we write $a, b \in \atoms$, then $a$ and $b$ can refer to the same name, i.e., $a = b$.
|
|
In other words, we do not adapt the permutative convention by \cite[].
|
|
|
|
As noted before, we want to let permutations act on objects constructed from names, such as lambda terms, tuples, and words.
|
|
The notion of a group action captures exactly this.
|
|
In most cases we are interested in the group $\Pm$.
|
|
However, in order to be general enough for the next chapters, we introduce group actions for an arbitrary group $G$.
|
|
|
|
\startdefinition
|
|
Let $X$ be a set.
|
|
A (left)
|
|
\footnote{Many authors use left actions.
|
|
However, we note that \citet[DBLP:journals/corr/BojanczykKL14] use a right action.
|
|
For them to have a well-defined group action, their group multiplication has to be defined as $g \cdot f = f \circ g$ (i.e., reverse function composition).}
|
|
\emph{$G$-action} is a function ${\cdot} \colon G \times X \to X$ satisfying:
|
|
\startformula\startalign[n=3]
|
|
\NC 1 \cdot x \NC = x \NC \quad \forall x \in X \NR
|
|
\NC (g \cdot h) \cdot x \NC = g \cdot (h \cdot x) \NC \quad \forall x \in X, \forall g,h \in G \NR
|
|
\stopalign\stopformula
|
|
A set together with a $G$-action, $(X, {\cdot})$, is called a \emph{$G$-set}.
|
|
\stopdefinition
|
|
|
|
It is worth noting that we generally fix $G$ but we consider many sets with a $G$-action.
|
|
In a way all these sets will have the same symmetries (namely $G$).
|
|
Instead of writing $g \cdot x$ we will often write the group action by juxtaposition $g x$.
|
|
We will often write $X$ instead of $(X, {\cdot})$ when the intended action is clear from the context.
|
|
\footnote{One should be cautious, as a set often allows for many different $G$-actions.}
|
|
|
|
\startexample
|
|
We list several examples of group actions.
|
|
Many of them will be used later in this thesis.
|
|
\startitemize
|
|
\item
|
|
The set $\atoms$ itself admits a natural $\Pm$-action, defined by
|
|
\startformula \pi \cdot a = \pi(a). \stopformula
|
|
The two requirements are easily verified by a routine calculation.
|
|
We will also omit this verification for the upcoming examples.
|
|
\item
|
|
The set of words $\atoms^{*}$ has a $\Pm$-action which is defined point-wise:
|
|
\startformula \pi \cdot a_1 a_2 \ldots a_k = \pi(a_1) \pi(a_2) \ldots \pi(a_k) \stopformula
|
|
\item
|
|
Similarly, the set of infinite words $\atoms^{\omega}$ has such a $\Pm$-action:
|
|
\startformula \pi \cdot a_1 a_2 \ldots = \pi(a_1) \pi(a_2) \ldots \stopformula
|
|
\item
|
|
The empty set always admits a unique $G$-action for any $G$.
|
|
(This is unique since the domain $G \times \emptyset = \emptyset$.)
|
|
\startformula {\cdot} \colon G \times \emptyset \to \emptyset \stopformula
|
|
\item
|
|
The singleton set always admits a unique $G$-action for any $G$.
|
|
(This is unique since the codomain only has just one element.)
|
|
\startformula {\cdot} \colon G \times \{*\} \to \{*\} \stopformula
|
|
\item
|
|
For any set $X$, we can define a $G$-action by defining
|
|
\startformula g \cdot x = x \stopformula
|
|
for all the elements $x \in X$.
|
|
Such an action is called \emph{trivial}.
|
|
Note that the action on $\emptyset$ and $\{*\}$ are trivial, but the $\Pm$-actions on $\atoms$, $\atoms^{*}$ and $\atoms^{\omega}$ are not trivial.
|
|
\item
|
|
Another interesting non-trivial example is the set $\Pm$ itself.
|
|
There are three different actions which are natural:
|
|
\startformula\startalign
|
|
\NC \pi \cdot_1 \sigma \NC = \pi \sigma \NR
|
|
\NC \pi \cdot_2 \sigma \NC = \sigma \pi^{-1} \NR
|
|
\NC \pi \cdot_3 \sigma \NC = \pi \sigma \pi^{-1} \NR
|
|
\stopalign\stopformula
|
|
Here the group multiplication is written by juxtaposition.
|
|
The first two actions are left-multiplication and right-multiplication respectively.
|
|
The latter is called conjugation.
|
|
For each of them, one can verify the requirements.
|
|
\stopitemize
|
|
\stopexample
|
|
|
|
In the above examples, the non trivial $\Pm$-sets are all infinite.
|
|
Yet, in a sense, the set $\atoms^{*}$ is bigger than the set $\atoms$.
|
|
To be able to quantify this, we introduce the notion of an orbit.
|
|
|
|
\startdefinition
|
|
Given a $G$-set $(X, {\cdot})$ and an element $x \in X$, we define the \emph{orbit of $x$} as the set
|
|
\startformula \orb(x) = \{ g x \mid g \in G \}. \stopformula
|
|
\stopdefinition
|
|
|
|
If for two elements $x, y \in X$ we have $\orb(x) = \orb(y)$, then we say that $x$ and $y$ are in the same orbit.
|
|
This precisely happens if there exists a $g$ such that $g x = y$.
|
|
The relation of \quotation{being in the same orbit} is an equivalence relation (it is reflexive as a group has an identity element, symmetric because of the inverses and transitive because of composition).
|
|
This relation partitions the set $X$ in a collection of orbits:
|
|
\startformula X = \bigcup_{x \in X} \orb(x). \stopformula
|
|
|
|
For a trivial $G$-set $X$, each element defines its own orbit, since $\orb(x) = \{ g x \mid g \in G \}$ is a singleton set.
|
|
|
|
\startexample
|
|
We will describe the orbits for some non-trivial $\Pm$-sets.
|
|
\startitemize
|
|
\item
|
|
The $\Pm$-set $\atoms$ only has \emph{one orbit}.
|
|
To see this, take two (distinct) elements $a, b \in \atoms$ and consider the bijection $\pi = \swap{a}{b}$.
|
|
Then we see that $\pi \cdot a = b$, meaning that $a$ and $b$ are in the same orbit.
|
|
So $\atoms$ is a single-orbit set.
|
|
\item
|
|
Before we tackle $\atoms^{*}$, we will analyse $\atoms^{2}$.
|
|
The set consists of exactly \emph{two orbits}:
|
|
\startformula\startalign
|
|
\NC \{ (a, a) \NC \mid a \in \atoms \} \NR
|
|
\NC \{ (a, b) \NC \mid a, b \in \atoms, a \neq b \} \NR
|
|
\stopalign\stopformula
|
|
This is because a bijection $\pi \in \Pm$ can never send an element of the form $(a, b)$ to an element of the form $(a, a)$ or vice versa.
|
|
It can, however send any element $(a, b)$ to $(c, d)$ and so on.
|
|
\item
|
|
The set $\atoms^{*}$ has \emph{countably many orbits}.
|
|
Since the action preserves the length of a word, we will show that the set has finitely many orbits for each length.
|
|
So consider the set $\atoms^{k}$ with the point-wise action.
|
|
An orbit of $\atoms^{k}$ is precisely determined by specifying which of the $k$ elements are equal to each other.
|
|
This is a partition of $k$ elements, and there exactly $B_k$, the $k$th Bell number, such partitions.
|
|
(As we have seen for $k = 2$, the second Bell number is $B_2 = 2$.
|
|
This quantity grows exponential in $k$.)
|
|
This shows that the set $\atoms^{*} = \bigcup_k \atoms^{k}$ has countably many orbits.
|
|
\item
|
|
The set $\atoms^{\omega}$ has \emph{uncountably many orbits}.
|
|
\stopitemize
|
|
|
|
|
|
\stopsubsection
|
|
\stopsection
|
|
\referencesifcomponent
|
|
\stopchapter
|
|
\stopcomponent |