From a5a38adb4d77b953f80dda4ba29fb57eff62bd36 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <lakseru@gmail.com>
Date: Tue, 2 Oct 2018 18:14:25 +0200
Subject: [PATCH] some intro for nom sets

---
 content/introduction.tex | 70 ++++++++++++++++++++++++++++++++++++++++
 environment/notation.tex |  2 ++
 2 files changed, 72 insertions(+)

diff --git a/content/introduction.tex b/content/introduction.tex
index b42c5f2..006fc48 100644
--- a/content/introduction.tex
+++ b/content/introduction.tex
@@ -21,7 +21,77 @@ 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.
 
+
+\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.
+
+
+\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 $\Perm(\atoms) = \{ \pi \colon \atoms \to \atoms \mid \pi \text{ is bijective} \}$ to be the set of permutations of atoms.
+Together with function composition, $\Perm(\atoms)$ forms a group.
+\stopdefinition
+
+As noted before, we want to let permutations act on objects constructed from names (such as lambda terms).
+The notion of a group action captures exactly this.
+In most cases we are interested in the group $\Perm(\atoms)$.
+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{Most 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 composition 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$).
+
+
+\stopsubsection
 \stopsection
 \referencesifcomponent
 \stopchapter
diff --git a/environment/notation.tex b/environment/notation.tex
index f5cd1cf..25b8b7b 100644
--- a/environment/notation.tex
+++ b/environment/notation.tex
@@ -36,6 +36,7 @@
 \define\N{\naturalnumbers}
 \define\Q{\rationals}
 \define\EAlph{\mathbb{A}}
+\define\atoms{\EAlph}
 \define\Perm{Perm}
 \define\id{id}
 \define\supp{{\tt supp}}
@@ -52,6 +53,7 @@
 \define\ext{ext}
 \define\Nsize{N}
 \define\Sym{Sym}
+\define[2]\swap{(#1 \, #2)}
 
 \define\Lint{\mathcal{L}_{\text{int}}}
 \define\Lmax{\mathcal{L}_{\text{max}}}