Skip to content
Snippets Groups Projects
Commit 0aaa35e7 authored by Ralf Jung's avatar Ralf Jung
Browse files

update iris.sty

parent 5cb9dfc4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
docs/constructions.tex
+ 5
− 5
View file @ 0aaa35e7
...@@ -387,20 +387,20 @@ The construction follows the idea of STSs as described in CaReSL \cite{caresl}. ...@@ -387,20 +387,20 @@ The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set: We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set:
\begin{align*} \begin{align*}
(s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\ (s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \sep \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2) s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2)
\end{align*} \end{align*}
We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set: We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
\begin{align*} \begin{align*}
\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \sep T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\ \STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\
\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' } \upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
\end{align*} \end{align*}
The STS RA is defined as follows The STS RA is defined as follows
\begin{align*} \begin{align*}
\monoid \eqdef{}& \setComp{\STSauth((s, T) \in \STSS \times \wp(\STST))}{\STSL(s) \sep T} +{}\\& \setComp{\STSfrag((S, T) \in \wp(\STSS) \times \wp(\STST))}{\STSclsd(S, T) \land S \neq \emptyset} + \bot \\ \monoid \eqdef{}& \setComp{\STSauth((s, T) \in \STSS \times \wp(\STST))}{\STSL(s) \disj T} +{}\\& \setComp{\STSfrag((S, T) \in \wp(\STSS) \times \wp(\STST))}{\STSclsd(S, T) \land S \neq \emptyset} + \bot \\
\STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \sep T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\ \STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
\STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \sep T'$ and $s \in S$} \\ \STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\
\mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\ \mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
\mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset) \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
\end{align*} \end{align*}
......
docs/derived.tex
+ 2
− 2
View file @ 0aaa35e7
...@@ -319,8 +319,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$ ...@@ -319,8 +319,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$. We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$. We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.
Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix. Similarly, we define $\namesp_1 \disj \namesp_2 \eqdef \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
We have that $\namesp_1 \sep \namesp_2 \Ra \namecl{\namesp_2} \sep \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$. We have that $\namesp_1 \disj \namesp_2 \Ra \namecl{\namesp_2} \disj \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \disj \namesp.\iname_2$.
We will overload the usual Iris notation for invariant assertions in the following: We will overload the usual Iris notation for invariant assertions in the following:
\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \] \[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
......
docs/iris.sty
+ 4
− 4
View file @ 0aaa35e7
...@@ -29,9 +29,8 @@ ...@@ -29,9 +29,8 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} \DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
\newcommand{\bigast}{\Sep} \newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
\newcommand\pord{\sqsubseteq}
\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep"
\newcommand\dplus{\mathbin{+\kern-1.0ex+}} \newcommand\dplus{\mathbin{+\kern-1.0ex+}}
\newcommand{\upclose}{\mathord{\uparrow}} \newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ } \newcommand{\ALT}{\ |\ }
...@@ -44,10 +43,11 @@ ...@@ -44,10 +43,11 @@
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}% \newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}} \newcommand{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
\newcommand{\pfn}{\rightharpoonup} \newcommand{\pfn}{\rightharpoonup}
\newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}} \newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}}
\newcommand{\la}{\leftarrow}
\newcommand{\ra}{\rightarrow} \newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow} \newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow} \newcommand{\Lra}{\Leftrightarrow}
......
docs/logic.tex
+ 3
− 3
View file @ 0aaa35e7
...@@ -50,7 +50,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. ...@@ -50,7 +50,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n \tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
\] \]
\judgment{Machine reduction} {\cfg{\tpool}{\state} \step \judgment[Machine reduction]{\cfg{\tpool}{\state} \step
\cfg{\tpool'}{\state'}} \cfg{\tpool'}{\state'}}
\begin{mathpar} \begin{mathpar}
\infer \infer
...@@ -181,7 +181,7 @@ The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable cont ...@@ -181,7 +181,7 @@ The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable cont
A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types. A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types.
In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$. In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$.
\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}} \judgment[Well-typed terms]{\vctx \proves_\Sig \wtt{\term}{\type}}
\begin{mathparpagebreakable} \begin{mathparpagebreakable}
%%% variables and function symbols %%% variables and function symbols
\axiom{x : \type \proves \wtt{x}{\type}} \axiom{x : \type \proves \wtt{x}{\type}}
...@@ -312,7 +312,7 @@ We implicitly assume that an arbitrary variable context, $\vctx$, is added to ev ...@@ -312,7 +312,7 @@ We implicitly assume that an arbitrary variable context, $\vctx$, is added to ev
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent. Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived. Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived.
\judgment{}{\vctx \mid \pfctx \proves \prop} \judgment{\vctx \mid \pfctx \proves \prop}
\paragraph{Laws of intuitionistic higher-order logic with equality.} \paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard. This is entirely standard.
\begin{mathparpagebreakable} \begin{mathparpagebreakable}
......
docs/model.tex
+ 2
− 2
View file @ 0aaa35e7
...@@ -95,7 +95,7 @@ We only have to define the missing connectives, the most interesting bits being ...@@ -95,7 +95,7 @@ We only have to define the missing connectives, the most interesting bits being
\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp} \typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
\begin{align*} \begin{align*}
\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned} \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
\All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\& \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
\Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f} \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
\end{aligned}} \end{aligned}}
\end{align*} \end{align*}
...@@ -105,7 +105,7 @@ We only have to define the missing connectives, the most interesting bits being ...@@ -105,7 +105,7 @@ We only have to define the missing connectives, the most interesting bits being
$\textdom{wp}$ is defined as the fixed-point of a contractive function. $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*} \begin{align*}
\textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned} \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned}
\All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\ \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
&(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\ &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\
&(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\ &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
&\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\ &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
......
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