From 78c6348d1dca069dfe2d26f255db7bc197bffe5f Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 3 Oct 2018 14:50:38 +0200 Subject: [PATCH] More intro nom sets --- content/introduction.tex | 117 +++++++++++++++++++++++++++++++++++++-- environment/notation.tex | 1 + 2 files changed, 112 insertions(+), 6 deletions(-) diff --git a/content/introduction.tex b/content/introduction.tex index 006fc48..862ae3b 100644 --- a/content/introduction.tex +++ b/content/introduction.tex @@ -55,7 +55,7 @@ The idea that names and permutations are sufficient was picked up by \citet[DBLP 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?}] @@ -66,19 +66,30 @@ Before we dive into the relation with automata, we will define the notion of nom 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. +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 -As noted before, we want to let permutations act on objects constructed from names (such as lambda terms). +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 $\Perm(\atoms)$. +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{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).} +\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 @@ -89,6 +100,100 @@ A set together with a $G$-action, $(X, {\cdot})$, is called a \emph{$G$-set}. 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 diff --git a/environment/notation.tex b/environment/notation.tex index 25b8b7b..4a7ddac 100644 --- a/environment/notation.tex +++ b/environment/notation.tex @@ -54,6 +54,7 @@ \define\Nsize{N} \define\Sym{Sym} \define[2]\swap{(#1 \, #2)} +\define\Pm{\Perm(\atoms)} \define\Lint{\mathcal{L}_{\text{int}}} \define\Lmax{\mathcal{L}_{\text{max}}}