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

docs: mention uniqueness of fixed-points

parent fd83e468
Pipeline #2616 passed with stage
in 8 minutes and 55 seconds
......@@ -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}
......
......@@ -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*}
......
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