Commit 25118e82 authored by Ralf Jung's avatar Ralf Jung

complete description of COFEs

parent 87e74b01
Pipeline #192 passed with stage
...@@ -2,13 +2,17 @@ ...@@ -2,13 +2,17 @@
\subsection{COFE} \subsection{COFE}
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)$.
\begin{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*} \begin{align*}
\All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\ \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 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 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{align*}
\end{defn} \end{defn}
...@@ -17,7 +21,7 @@ ...@@ -17,7 +21,7 @@
\subsection{CMRA} \subsection{CMRA}
\begin{defn} \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*} \begin{align*}
\All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\ \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} \\ \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
...@@ -176,10 +176,9 @@ ...@@ -176,10 +176,9 @@
\newcommand{\pset}[1]{\wp(#1)} % Powerset \newcommand{\pset}[1]{\wp(#1)} % Powerset
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)} \newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
\newcommand{\dom}{\textrm{dom}} \newcommand{\dom}{\mathrm{dom}}
%\newcommand{\rng}{\textrm{rng}} \newcommand{\cod}{\mathrm{cod}}
%\newcommand{\cod}{\textrm{cod}} \newcommand{\chain}{\mathrm{chain}}
\newcommand{\IF}{\mathrel{\text{if}}} \newcommand{\IF}{\mathrel{\text{if}}}
\newcommand{\WHEN}{\textrm{when }} \newcommand{\WHEN}{\textrm{when }}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment