From 48c3a9bccff30b9ba46879a771586e971e4d64b2 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 5 Oct 2018 14:41:35 +0200 Subject: [PATCH] Rewrote intro to nom sets --- content/introduction.tex | 111 ++++++++++++++++++++++++++++----------- environment/font.tex | 3 +- environment/notation.tex | 4 ++ environment/tikz.tex | 1 + 4 files changed, 86 insertions(+), 33 deletions(-) diff --git a/content/introduction.tex b/content/introduction.tex index 862ae3b..a8aaa47 100644 --- a/content/introduction.tex +++ b/content/introduction.tex @@ -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 diff --git a/environment/font.tex b/environment/font.tex index 720656f..7e801f2 100644 --- a/environment/font.tex +++ b/environment/font.tex @@ -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] diff --git a/environment/notation.tex b/environment/notation.tex index 4a7ddac..32ba6ee 100644 --- a/environment/notation.tex +++ b/environment/notation.tex @@ -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}} diff --git a/environment/tikz.tex b/environment/tikz.tex index 576628e..738e358 100644 --- a/environment/tikz.tex +++ b/environment/tikz.tex @@ -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}}}