diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 92e25252c0887b56d6ce8fe30218c3565e580d75..5e7d5418327fbbf5b0bf1c755fa5ba15a46c398b 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -448,7 +448,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlo {\upd\plainly\prop \proves \prop} \end{mathpar} The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about$a$and$B$. -%\ralf{Trouble is, we don't actually have$\in$inside the logic...} +%\ralf{Trouble is, we do not actually have$\in$inside the logic...} \subsection{Consistency} diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex index 843b8751a75159ac1b73ad46d6cd81849ecf78bc..402a67310a77fed4e22cc730ee612edd106ddf0e 100644 --- a/docs/ghost-state.tex +++ b/docs/ghost-state.tex @@ -44,7 +44,7 @@ Noteworthy here is the fact that$\prop \proves \later\prop$can be derived from \subsection{Persistent Propositions} We call a proposition$\prop$\emph{persistent} if$\prop \proves \always\prop$. -These are propositions that don't own anything'', so we can (and will) treat them like normal'' intuitionistic propositions. +These are propositions that do not own anything'', so we can (and will) treat them like normal'' intuitionistic propositions. Of course,$\always\prop$is persistent for any$\prop$. Furthermore, by the proof rules given in \Sref{sec:proof-rules},$\TRUE$,$\FALSE$,$t = t'$as well as$\ownGhost\gname{\mcore\melt}$and$\mval(\melt)$are persistent. diff --git a/docs/paradoxes.tex b/docs/paradoxes.tex index a3bb499a4dd2363a349ef80bcca125dedf892449..8addc115deaa3a393bed534b90d277298a2e11ee 100644 --- a/docs/paradoxes.tex +++ b/docs/paradoxes.tex @@ -32,7 +32,7 @@ Notice that these are immutable locations, so the maps-to proposition is persist The rule \ruleref{sprop-alloc} is then thought of as allocation, and the rule \ruleref{sprop-agree} states that a given location$\gname$can only store \emph{one} proposition, so multiple witnesses covering the same location must agree. %Compared to saved propositions in prior work, \ruleref{sprop-alloc} is stronger since the stored proposition can depend on the name being allocated. -%\derek{Can't we cut the above sentence? This makes it sound like we are doing something weird that we ought not to be since prior work didn't do it. But in fact, I thought that in our construction we don't really need to rely on this feature at all! So I'm confused.} +%\derek{Can't we cut the above sentence? This makes it sound like we are doing something weird that we ought not to be since prior work didn't do it. But in fact, I thought that in our construction we do not really need to rely on this feature at all! So I'm confused.} The conclusion of \ruleref{sprop-agree} usually is guarded by a$\later$. The point of this theorem is to show that said later is \emph{essential}, as removing it introduces inconsistency. % @@ -43,7 +43,7 @@$A(\gname) \eqdef \Exists \prop : \Prop. \always\lnot \prop \land \gname \Mapsto Intuitively, $A(\gname)$ says that the saved proposition named $\gname$ does \emph{not} hold, \ie we can disprove it. Using \ruleref{sprop-persist}, it is immediate that $A(\gname)$ is persistent. -Now, by applying \ruleref{sprop-alloc} with $A$, we obtain a proof of $\prop \eqdef \gname \Mapsto A(\gname)$: this says that the proposition named $\gname$ is the proposition saying that it, itself, doesn't hold. +Now, by applying \ruleref{sprop-alloc} with $A$, we obtain a proof of $\prop \eqdef \gname \Mapsto A(\gname)$: this says that the proposition named $\gname$ is the proposition saying that it, itself, does not hold. In other words, $\prop$ says that the proposition named $\gname$ expresses its own negation. Unsurprisingly, that leads to a contradiction, as is shown in the following lemma: \begin{lem} \label{lem:saved-prop-counterexample-not-agname} We have $\gname \Mapsto A(\gname) \proves \always\lnot A(\gname)$ and $\gname \Mapsto A(\gname) \proves A(\gname)$. \end{lem} diff --git a/docs/program-logic.tex b/docs/program-logic.tex index f4a4ba7ce70da554e255729538c2c0c0f3638420..df72785caaed76f5f05af3443bdeb568e30aa31f 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -521,7 +521,7 @@ Furthermore, as we construct more sophisticated and more interesting things that For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition: $\Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop)$ -This accessor is idempotent'' in the sense that it doesn't actually change the state. After applying it, we get our $\prop$ back so we end up where we started. +This accessor is idempotent'' in the sense that it does not actually change the state. After applying it, we get our $\prop$ back so we end up where we started. %%% Local Variables: %%% mode: latex