notation.tex

\section{Notation}\label{sec:notation}

\begin{description}
\item[Natural Numbers] The set $\mathbb{N}$ refers to the set of all natural
  numbers $\{0, 1, 2, \ldots\}$. The set $\mathbb{Q}$ refers to the set of
  rational numbers.
\item[Booleans] The set $\mathbb{B}$ denotes the set of booleans
  $\{\var{True}, \var{False}\}$.
\item[Powerset] Given a set $\type{X}$, $\powerset{\type{X}}$ is the set of all
  the subsets of $X$.
\item[Sequences] Given a set $\type{X}$, $\seqof{\type{X}}$ is the set of
  sequences having elements taken from $\type{X}$. The empty sequence is
  denoted by $\epsilon$, and given a sequence $\Lambda$, $\Lambda; \type{x}$ is
  the sequence that results from appending $\type{x} \in \type{X}$ to
  $\Lambda$.
\item[Functions] $A \to B$ denotes a \textbf{total function} from $A$ to $B$.
  Given a function $f$ we write $f~a$ for the application of $f$ to argument
  $a$.
\item[Inverse Image] Given a function $f: A \to B$ and $b\in B$, we write
  $f^{-1}~b$ for the \textbf{inverse image} of $f$ at $b$, which is defined by
  $\{a \mid\ f a =  b\}$.
\item[Maps and partial functions] $A \mapsto B$ denotes a \textbf{partial
    function} from $A$ to $B$, which can be seen as a map (dictionary) with
  keys in $A$ and values in $B$. Given a map $m \in A \mapsto B$, notation
  $a \mapsto b \in m$ is equivalent to both $m~ a = b$ and $\mathsf{a}~m = b$.
  Given a set $A$, $A \mapsto A$ represents the identity map on $A$:
  $\{a \mapsto a \mid a \in A\}$. The $\emptyset$ symbol is also used to
  represent the empty map as well.
\item[Domain and range] Given a relation $R \in \powerset{(A \times B)}$,
  $\dom~R \in \powerset{A}$ refers to the domain of $R$, and
  $\range~R \in \powerset{B}$ refers to the range of $R$. Note that (partial)
  functions (and hence maps) are also relations, so we will be using $\dom$ and
  $\range$ on functions.
\item[Domain and range operations] Given a relation
  $R \in \powerset{(A \times B)}$ we make use of the \textit{domain-restriction},
  \textit{domain-exclusion}, and \textit{range-restriction} operators, which
  are defined in \cref{fig:domain-and-range-ops}. Note that a map $A \mapsto B$
  can be seen as a relation, which means that these operators can be
  applied to maps as well.
\item[Integer ranges] Given $a, b \in \mathbb{Z}$, $[a, b]$ denotes the
  sequence $[i \mid a \leq i \leq b]$ . Ranges can have open ends: $[.., b]$
  denotes sequence $[i \mid i \leq b]$, whereas $[a, ..]$ denotes sequence
  $[i \mid a \leq i]$. Furthermore, sometimes we use $[a, b]$ to denote a set
  instead of a sequence. The context in which it is used should provide enough
  information about the specific type.
\item[Domain and range operations on sequences] We overload the $\restrictdom$,
  $\subtractdom$, and $\restrictrange$ to operate over sequences. So for
  instance given $S \in \seqof{A}$, and $R \in \seqof{(A \times B)}$:
  $S \restrictdom R$ denotes the sequence
  $[ (a, b) \mid (a, b) \in R, a \in S]$.
\item[Wildcard variables] When a variable is not needed in a term, we replace
  it by $\wcard$ to make it explicit that we do not use this variable in the
  scope of the given term.
\item[Implicit existential quantifications] Given a predicate
  $P \in X \to \mathbb{B}$, we use $P \wcard$ as a shorthand notation for
  $\exists x \cdot P~x$.

\item[Pattern matching in premises] In the inference-rules premises use
  $\var{patt} \leteq \var{exp}$ to pattern-match an expression $\var{exp} $
  with a certain pattern $\var{patt}$. For instance, we use
  $\Lambda'; x \leteq \Lambda$ to be able to deconstruct a sequence $\Lambda$
  in its last element, and prefix. If an expression does not match the given
  pattern, then the premise does not hold, and the rule cannot trigger.

\item[Ceiling] Given a number $n \in \mathbb{R}$, $\ceil{n}$ represents the
  ceiling of $n$, and $\floor{n}$ represents its floor.
\end{description}

\begin{figure}[htb]
  \begin{align*}
    \var{S} \restrictdom \var{R}
    & = \{ (a, b) \mid (a, b) \in R, ~ a \in S \}
    & \text{domain restriction}
    \\
    S \subtractdom R
    & = \{ (a, b) \mid (a, b) \in R, ~ a \notin S \}
    & \text{domain exclusion}
    \\
    R \restrictrange S
    & = \{ (a, b) \mid (a, b) \in R, ~ b \in S \}
    & \text{range restriction}
  \end{align*}
  \caption{Domain and range operations}
  \label{fig:domain-and-range-ops}
\end{figure}