joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Rewrote intro to nom sets

Browse source
This commit is contained in:
Joshua Moerman 2018-10-05 14:41:35 +02:00
parent 78c6348d1d
commit 48c3a9bccf
4 changed files with 86 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

111
content/introduction.tex
View file

@ -21,41 +21,71 @@ learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learni
\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.
In the second part of this thesis, I will present results related to nominal automata.
Usually, nominal techniques are introduced in order to solve problems involving name binding in topics like lambda calculus.
However, for our applications it makes more sense to focus more on the symmetries (of names) first and show how this is useful in automata theory.
To motivate the use of symmetries, we will look at an example of a register auttomaton.
In the following automaton we model a (not-so-realistic) login system for a single person.
The alphabet consists of the following actions:
\startformula\startalign
\NC \kw{register}(p) \NR
\NC \kw{login}(p) \NR
\NC \kw{logout}() \NR
\NC \kw{view}() \NR
\stopalign\stopformula
The \kw{register} action allows one to set a password $p$.
This can only be done when the system is initialised.
The \kw{login} and \kw{logout} actions speak for themselves and the \kw{view} action allows one to see the secret data (we abstract away from what the user actually gets to see here).
A simple automaton with roughly this behaviour is given in \in{Figure}[fig:login-system].
\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.
\startplacefigure
[title={A simple register automaton. The symbol $\ast$ denotes any input otherwise not specified. The $r$ in states $q_1$ and $q_2$ is a register.},
list={A simple register automaton.},
reference=fig:login-system]
\hbox{\starttikzpicture[node distance=4cm]
\node[state,initial] (0) {$q_0$};
\node[state with output,right of=0] (1) {$q_1$ \nodepart{lower} $r$};
\node[state with output,right of=1] (2) {$q_2$ \nodepart{lower} $r$};
\path[->]
(0) edge [loop below] node [below] {$\ast$ / \checknok}
(0) edge node [above, align=center] {$\kw{register}(p)$ / \checkok \\ set $r := p$} (1)
(1) edge [loop below] node [below] {$\ast$ / \checknok}
(1) edge [bend left, align=center] node [above] {$\kw{login}(p)$ / \checkok \\ if $r = p$} (2)
(2) edge [loop below] node [right, align=left] {$\kw{view}()$ / \checkok \\ $\ast$ / \checknok}
(2) edge [bend left] node [below] {$\kw{logout}()$ / \checkok} (1);
\stoptikzpicture}
\stopplacefigure
To model the behaviour nicely, we want the domain of passwords to be infinite.
After all, one should allow arbitrarily long passwords.
This means that a register automaton is actually an automaton over an infinite alphabet.
Common algorithms for automata, such as learning, will not work with an infinite alphabet.
Any loop which iterates over the alphabet will diverge.
In order to cope with this, we will use the \emph{symmetries} present in the alphabet.
Let us continue with the example and look at its symmetries.
If a person registers with a password \quotation{\kw{hello}} and consequently logins with \quotation{\kw{hello}}, then this is not distinguishable from a person registering and logging in with \quotation{\kw{bye}}.
However, a trace $\kw{register}(\kw{hello})\, \kw{login}(\kw{bye})$ is different.
This is an example of symmetry:
the values \quotation{\kw{hello}} and \quotation{\kw{bye}} can be permuted, or interchanged.
Before formalising the permutations, let me remark the the use of symmetries in automata theory is not new.
One of the first to use symmetries was \citet[DBLP:conf/alt/Sakamoto97].
He devised an \LStar{} learning algorithm for register automata, much like the one presented in \in{Chapter}[chap:learning-nominal-automata].
The symmetries are crucial to reduce the problem to a finite alphabet and use the regular \LStar{} algorithm.
(\in{Chapter}[chap:learning-nominal-automata] shows how to do it with more general symmetries.)
Around the same time \citet[FerrariMT05] worked on automata theoretic algorithms for the \pi-calculus.
Their approach was based on the same symmetries and they developed a theory of \emph{named sets} to implement their algorithms.
Named sets are equivalent to nominal sets.
However, nominal sets are defined in a more elementary way.
The nominal sets we will soon see are introduced by \citet[GabbayP02] to solve certain problems in name binding in abstract syntaxes.
Although this is not really related to automata theory, it was picked up by \citet[DBLP:journals/corr/BojanczykKL14].
They provide an equivalence between register automata and nominal automata.
Additionally, they generalise the work on nominal sets to other symmetries.
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?}]
@ -193,9 +223,26 @@ 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}.
To see this we will order the elements of $\atoms = \{ a_0, a_1, a_2, \ldots \}$.
Now, let $\sigma \in 2^{\omega}$ be an element of the Cantor space.
We define the following sequence $x^{\sigma} \in \atoms^{\omega}$:
\startformula\startalign
\NC x^{\sigma}_0 \NC = a_0 \NR
\NC x^{\sigma}_{i+1} \NC =
\startmathcases
\NC a_i, \NC if $\sigma(i) = 0$ \NR
\NC a_{i+1}, \NC if $\sigma(i) = 1$ \NR
\stopmathcases \NR
\stopalign\stopformula
Now for two distinct elements $\sigma, \tau \in 2^{\omega}$, the elements $x^{\sigma}$ and $x^{\tau}$ are different.
More importantly, their orbits $\orb(x^{\sigma})$ and $\orb(x^{\tau})$ are different.
This shows that there is an injective map from $2^{\omega}$ to the orbits of $\atoms^{\omega}$.
This concludes that $\atoms^{\omega}$ has uncountably many orbits.
\stopitemize
\stopsubsection
\stopsection
\referencesifcomponent

3
environment/font.tex
View file

@ -18,7 +18,8 @@
% (Neo) Euler heeft niet alle symbolen, maar Pagella wel
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range=0x0266D-0x0266F,rscale=0.95] % sharp and flat
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x025A1,0x025B3}] % triangle, square
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x022EE}] % vdots
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x022EE, 0x02254}] % vdots, assignment
% \definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x02713,0x02717}] % checkmark
% Neo Euler voor wiskunde. Merk op dat dit niet cursief is!
\definefontfamily[mainfamily] [mm] [Neo Euler] [rscale=0.95]
% \definefontfamily[mainfamily] [mm] [Latin Modern Math]

4
environment/notation.tex
View file

@ -1,9 +1,13 @@
\startenvironment notation
\usesymbols[fontawesome]
% Pijlen met text erboven
\definemathstackers [arrowstack] [voffset=-.7\mathexheight, topcommand=\m]
\definemathextensible [arrowstack] [tot] ["27F6]
\define\checkok{\scale[height=.5em]{\symbol[fontawesome][ok]}} % ✓
\define\checknok{\scale[height=.5em]{\symbol[fontawesome][remove]}} % find a font with ✗
\define[1]\Fam{\mathcal{#1}}
\define\lang{\mathcal{L}}

1
environment/tikz.tex
View file

@ -8,6 +8,7 @@
% defaults
\tikzset{node distance=2cm} % 'shorten >=2pt' only for automata
\tikzset{/pgfplots/table/search path={data,../data}}
\tikzset{initial text=}
% observation table
\tikzset{obs table/.style={matrix of math nodes, ampersand replacement=\&, column 1/.style={anchor=base west}}}