From 25118e823309bb318b6cb10c4936708acbbde9fa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 29 Feb 2016 13:39:05 +0100
Subject: [PATCH] complete description of COFEs
---
docs/algebra.tex | 10 +++++++---
docs/setup.tex | 7 +++----
2 files changed, 10 insertions(+), 7 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index f9ee23ccd..3b726eccd 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 22d2a72a4..a75c3a5a9 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 }}
--
GitLab