lama_byterun/spec/01.02.notation.tex

51 lines
692 B
TeX
Raw Normal View History

2019-11-24 02:30:32 +03:00
\section{Notation}
Pairs and tuples:
\[
\inbr{\bullet,\,\bullet,\,\dots}
\]
Lists of elements of kind $X$:
\[
X^*
\]
Deconstructing lists into sublists:
\[
h\circ t
\]
This applies also to lists of length 1. Empty list is denoted
\[
\epsilon
\]
For a mapping $f : X\to Y$ we use the following definition:
\[
f [x\gets y] = \lambda\,z\,.\,
\left\{
\begin{array}{rcl}
y &,& x = z \\
f\;x &,& x\neq z
\end{array}
\right.
\]
Empty mapping (undefined everywhere) is denoted $\Lambda$, the domain of a mapping $f$~--- $\dom{f}$, and we abbreviate
\[
\Lambda[x_1\gets y_1][x_2\gets y_2]\dots[x_k\gets y_k]
\]
as
\[
[x_1\gets y_1,\,x_2\gets y_2,\,\dots,\,x_k\gets y_k]
\]