From 38b6c3033c199b847192d3fa74c7b58c4e6a680d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 28 Oct 2017 18:16:51 +0200 Subject: [PATCH] more CHANGELOG --- CHANGELOG.md | 4 ++-- docs/algebra.tex | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4fc86cd7..74ade33e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,10 +9,10 @@ Changes in and extensions of the theory: * [#] Add new modality: ■ ("plainly"). * [#] Camera morphisms have to be homomorphisms, not just monotone functions. -* [#] Add a proof that f has a fixed point if f^k is contractive. +* Add a proof that f has a fixed point if f^k is contractive. * Constructions for least and greatest fixed points over monotone predicates (defined in the logic of Iris using impredicative quantification). -* A proof of the inverse of wp_bind. +* Add a proof of the inverse of wp_bind. Changes in Coq: diff --git a/docs/algebra.tex b/docs/algebra.tex index b5050387..972778a8 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -75,6 +75,7 @@ The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the d Completeness is necessary to take fixed-points. For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. +This also holds if $f^k$ is contractive for an arbitrary $k$. Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point. -- GitLab