Commit 3d79ec6c authored by Ralf Jung's avatar Ralf Jung

docs: type-level later

parent 979bd7af
...@@ -40,6 +40,7 @@ Note that $\COFEs$ is cartesian closed. ...@@ -40,6 +40,7 @@ Note that $\COFEs$ is cartesian closed.
A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map. A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn} \end{defn}
Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
\subsection{RA} \subsection{RA}
......
% !TEX root = ./appendix.tex % !TEX root = ./appendix.tex
\section{COFE constructions}
\subsection{Next (type-level later)}
Given a COFE $\cofe$, we define $\latert\cofe$ as follows:
\begin{align*}
\latert\cofe \eqdef{}& \latertinj(\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
\end{align*}
$\latert(-)$ is a locally \emph{contractive} bifunctor from $\COFEs$ to $\COFEs$.
\clearpage
\section{CMRA constructions} \section{CMRA constructions}
\subsection{Product} \subsection{Product}
......
...@@ -101,6 +101,7 @@ ...@@ -101,6 +101,7 @@
\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}} \newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}} \newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
\newcommand{\latert}{\mathord{\blacktriangleright}} \newcommand{\latert}{\mathord{\blacktriangleright}}
\newcommand{\latertinj}{\textlog{next}}
\newcommand{\Sem}[1]{\llbracket #1 \rrbracket} \newcommand{\Sem}[1]{\llbracket #1 \rrbracket}
......
...@@ -41,7 +41,7 @@ It does not matter whether they fork off an arbitrary expression. ...@@ -41,7 +41,7 @@ It does not matter whether they fork off an arbitrary expression.
\end{enumerate} \end{enumerate}
\end{defn} \end{defn}
\subsection{The concurrent language} \subsection{Concurrent language}
For any language $\Lang$, we define the corresponding thread-pool semantics. For any language $\Lang$, we define the corresponding thread-pool semantics.
...@@ -64,7 +64,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. ...@@ -64,7 +64,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\end{mathpar} \end{mathpar}
\clearpage \clearpage
\section{The logic} \section{Logic}
To instantiate Iris, you need to define the following parameters: To instantiate Iris, you need to define the following parameters:
\begin{itemize} \begin{itemize}
......
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