The following notation will be used throughout this dissertation.

Let $X$ and $Y$ be sets.  $\mymath{X \rightarrow{} Y}$ denotes the set
of functions from $X$ to $Y$.  $\mymath{X \times Y}$ denotes the
\emph{Cartesian product} of $X$ and $Y$, i.e., the set of ordered
pairs $(x, y)$, with $x\in X$ and $y\in Y$. 

Let $\mathbb{Z}$ be the set of integers and
$\mathbb{N} = \{0, 1,\ldots\}$ be the set of natural numbers.  For
$n \in \mathbb{N}$, we use $\nprocs{n}$ to denote the set of natural
numbers $\{0, 1, \ldots{}, n-1\}$.  $\nprocs{0}$ is an empty set.

Let $S$ be a set.  The power set of $S$, i.e., the set of all subsets
of $S$, is denoted $\powerset(S)$.  The set of all finite sequences of
elements of $S$ is denoted $S^*$.  Formally,
\[
S^* = \bigcup_{n \geq 0} (\nprocs{n} \rightarrow{} S).
\]
However, we will often use the standard notation
$s_0s_1 \cdots s_{n-1}$ to denote the sequence
$\xi\colon \nprocs{n}\rightarrow S$ such that $\xi(i) = s_i$ for
$0 \leq i < n$.

Let $\xi = s_0s_1 \cdots s_{n-1}$ be an element
of $S^*$.  The length of $\xi$, denoted $|\xi|$, is $n$.  The empty
sequence, i.e., the unique element in $S^*$ of length 0, is denoted
$\epsilon$.  If $\zeta = s'_0 \cdots s'_{m-1}$ is also an element of
$S^*$, then the \emph{concatenation} of $\xi$ and $\zeta$, denoted 
$\xi \circ{} \zeta$, is the sequence
$s_0 \cdots{} s_{n-1}s'_0 \cdots{} s'_{m-1}$.  Note
$|\xi \circ{} \zeta| = n + m$.  If $|\xi| > 0'$,
$\mymath{\myhead{}(\xi) = s_0}$ and $\mymath{\mytail{}(\xi) = s_{n-1}}$. (Note
$\mymath{\myhead{}(\epsilon)}$ and $\mymath{\mytail{}(\epsilon)}$ are
undefined.)

There are various structures, e.g., sequences, tuples and expressions.
Let $t$ be some structures.  A \emph{substitution} notation,
$\mymath{t\lbrack{}a'/a\rbrack{}}$, denotes the structure of the same
type as $t$ that is obtained by substituting all appearances of $a$
with $a'$ in $t$.


Let $X$ and $Y$ be sets.  Let $f \colon{} X \rightarrow{} Y$,
$a \in X$ and $b \in Y$.
$\mymath{f\lbrack{} a \mapsto b\rbrack{}}\colon{} X \rightarrow{} Y$
denotes a function defined by:
\begin{align}
  \mymath{
  f\lbrack{}a \mapsto b\rbrack{}(c) = 
  \begin{cases}
    b & \text{if } a = c \\
    f(c) & \text{otherwise.}
  \end{cases}} \nonumber
\end{align}

Let $t$ be a tuple and $c$ a component of $t$.  Let $c'$ be a
structure of the same type as $c$.  We use $t[c:=c']$ to denote the
tuple that is obtained by changing $c$ of $t$ to $c'$.

Let $A$, $B$ and $C$ be formulas in a logic.  An \emph{inference rule}
has the form $\frac{A,\, B,\, ...}{C}$.  It means that if the
\emph{premises} $A$, $B$, ...\ are derived, the \emph{conclusion} $C$
can be derived.

Propositional logic operators are written as follows: $\wedge{}$
denotes \emph{and}, $\vee{}$ denotes \emph{or}, $\neg{}$ denotes
\emph{negation}, $\Rightarrow$ denotes \emph{implies}.  In addition,
$\forall{x \in X}.\, p$ denotes a \emph{universally quantified
  expression}, where $x$ is a bound variable, $X$ is the domain of
$x$, and $p$ is a predicate.  Similarly, $\exists{x \in X}.\, p$
denotes a \emph{existentially quantified expression}.

Let $l$ be a variable, and let $s$ and $e$ be mathematical
expressions.  We use ``let $l = s$ in $e$'' to denote the expression
resulting from replacing every occurrence of $l$ with $s$ in $e$.



%A \emph{tree} is a \emph{list} if no node in the tree has more than one child node.  Given a tree $t$ and a list $l$ that have at least one common node, a node $n$ is called the least common ancestor of $t$ and $l$, denoted as $\mymath{lca(t, l)}$, iff

%\begin{itemize}
 % \item $n$ is in $t$ and $n$ is in $l$, and
 % \item the $i$-th ancestor of $n$ in $t$ equals to the $i$-th ancestor of $n$ in $l$, and
 % \item no child of $n$ in $t$ equals to the child of $n$ in $l$.
 % \end{itemize}