From 6b839469218335203112e4b367cb8abd7a26ecb1 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 14 Mar 2016 12:49:00 +0100 Subject: [PATCH] some more intuition for SProp --- docs/constructions.tex | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/constructions.tex b/docs/constructions.tex index dc3b643b..6f30b971 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -28,9 +28,12 @@ One way to understand this definition is to re-write it a little. We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, we proposition either holds or does not hold. \begin{align*} \SProp \eqdef{}& \psetdown{\mathbb{N}} \\ - \eqdef{}& \setComp{\prop \in \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \prop \Ra m \in \prop } \\ - \prop \nequiv{n} \propB \eqdef{}& \All m \leq n. m \in \prop \Lra m \in \propB + \eqdef{}& \setComp{X \in \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\ + X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y \end{align*} +Notice that with this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA: +We could equivalently require every CRMA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}. + Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a monotone'' function here is a little funny. \begin{align*} \UPred(\monoid) \cong{}& \monoid \monra \SProp \\ -- GitLab