diff --git a/docs/algebra.tex b/docs/algebra.tex index 4479a15967e3fe54df1385952d7f7ed4aa4d4aec..494fb54c752674b296412c1368063186d2d6b2b5 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -39,7 +39,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e \end{defn} Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data. Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$. -The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. +The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique}\footnote{Uniqueness is not proven in Coq.} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. @@ -59,6 +59,7 @@ Note that $\COFEs$ is cartesian closed. In particular: \end{defn} The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor. 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. +The reason contractive (bi)functors are interesting is that by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, they have a unique\footnote{Uniqueness is not proven in Coq.} fixed-point. \subsection{RA} diff --git a/docs/model.tex b/docs/model.tex index 34506fd6653b29985ca82b32d3d04bfffc0c70fa..31db77a01ea5797d3f7e374662e5b4db65c1c972 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -62,7 +62,8 @@ Furthermore, since $\Sigma$ is locally contractive, so is $\textdom{ResF}$. Now we can write down the recursive domain equation: $\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp))$ -$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}. +$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor. +This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}. We do not need to consider how the object is constructed. We only need the isomorphism, given by \begin{align*}