diff --git a/docs/algebra.tex b/docs/algebra.tex index f9ee23ccda21a67cf0f2970cd96a00cc430d56f0..3b726eccd7ace4a78ee8925ade3f3f3980ded5ee 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -2,13 +2,17 @@ \subsection{COFE} +\begin{defn}[Chain] + Given some set $T$ and an indexed family $({\nequiv{n}} \subseteq T \times T)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to T$ such that $\All n, m. n < m \Ra c (m) \nequiv{n} c (n+1)$. +\end{defn} + \begin{defn} - A COFE is a tuple $(T, (\nequiv{n})_{n \in \mathbb{N}}, c : (\mathbb{N} \to T) \to T)$ satisfying + A \emph{complete ordered family of equivalences} (COFE) is a tuple $(T, ({\nequiv{n}} \subseteq T \times T)_{n \in \mathbb{N}}, \lim : \chain(T) \to T)$ satisfying \begin{align*} \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\ - \All n, X.& c(X) \nequiv{n} X(n+1) \tagH{cofe-compl} + \All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl} \end{align*} \end{defn} @@ -17,7 +21,7 @@ \subsection{CMRA} \begin{defn} - A CMRA is a tuple $(\monoid, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \munit: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid, (\mdiv) : \monoid \times \monoid \to \monoid)$ satisfying + A \emph{CMRA} is a tuple $(\monoid, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \munit: \monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid, (\mdiv) : \monoid \times \monoid \to \monoid)$ satisfying \begin{align*} \All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\ \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\ diff --git a/docs/setup.tex b/docs/setup.tex index 22d2a72a4fc90d9ef25ca26517eaa2a16724aeb0..a75c3a5a95ffb218671a3d3890983f501850a632 100644 --- a/docs/setup.tex +++ b/docs/setup.tex @@ -176,10 +176,9 @@ \newcommand{\pset}[1]{\wp(#1)} % Powerset \newcommand{\psetdown}[1]{\wp^\downarrow(#1)} -\newcommand{\dom}{\textrm{dom}} -%\newcommand{\rng}{\textrm{rng}} -%\newcommand{\cod}{\textrm{cod}} - +\newcommand{\dom}{\mathrm{dom}} +\newcommand{\cod}{\mathrm{cod}} +\newcommand{\chain}{\mathrm{chain}} \newcommand{\IF}{\mathrel{\text{if}}} \newcommand{\WHEN}{\textrm{when }}