Commit f01811c1 authored by Ralf Jung's avatar Ralf Jung

setup.tex: remove loads of unused stuff, start sorting a little

parent 511f26a4
\section{Algebraic Structures}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
......@@ -379,3 +379,8 @@ By upward-closedness, it suffices to show $\textsf{frame}(s, T_f) \ststrans \tex
This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step.
\end{proof}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
......@@ -38,11 +38,16 @@
%\clearpage
\tableofcontents
\clearpage\input{algebra}
\clearpage\input{constructions}
\clearpage\input{logic}
\clearpage\input{model}
\clearpage\input{derived}
\clearpage
\input{algebra}
\clearpage
\input{constructions}
\clearpage
\input{logic}
\clearpage
\input{model}
\clearpage
\input{derived}
\clearpage\printbibliography % If we want biblatex
......
......@@ -22,20 +22,20 @@
expression then so is $\fork{\expr}$. We moreover assume a value
\textsf{fRet} (giving the intended return value of a fork), and we assume that
\begin{align*}
\fork{\expr} &\notin \textdom{Val} \\
\fork{\expr_1} = \fork{\expr_2} &\implies \expr_1 = \expr_2
\fork{\expr} &\notin \textdom{Val} \\
\fork{\expr_1} = \fork{\expr_2} &\implies \expr_1 = \expr_2
\end{align*}
\item A set $\textdom{Ectx}$ of \emph{evaluation contexts} ($\ectx$) that includes the empty context $[\; ]$,
a plugging operation $\ectx[\expr]$ that produces an expression, and context composition $\circ$
satisfying the following axioms:
\begin{align*}
[\; ][ \expr ] &= \expr \\
\ectx_1[\ectx_2[\expr]] &= (\ectx_1 \circ \ectx_2) [\expr] \\
\ectx_1[\expr] = \ectx_2[\expr] &\implies \ectx_1 = \ectx_2 \\
\ectx[\expr_1] = \ectx[\expr_2] &\implies \expr_1 = \expr_2 \\
\ectx_1 \circ \ectx_2 = [\; ] &\implies \ectx_1 = \ectx_2 = [\; ] \\
\ectx[\expr] \in \textdom{Val} &\implies \ectx = [\;] \\
\ectx[\expr] = \fork{\expr'} &\implies \ectx = [\;]
[\; ][ \expr ] &= \expr \\
\ectx_1[\ectx_2[\expr]] &= (\ectx_1 \circ \ectx_2) [\expr] \\
\ectx_1[\expr] = \ectx_2[\expr] &\implies \ectx_1 = \ectx_2 \\
\ectx[\expr_1] = \ectx[\expr_2] &\implies \expr_1 = \expr_2 \\
\ectx_1 \circ \ectx_2 = [\; ] &\implies \ectx_1 = \ectx_2 = [\; ] \\
\ectx[\expr] \in \textdom{Val} &\implies \ectx = [\;] \\
\ectx[\expr] = \fork{\expr'} &\implies \ectx = [\;]
\end{align*}
\item A set \textdom{State} of shared machine states (\eg heaps), metavariable $\state$.
......@@ -45,7 +45,7 @@
and notions of an expression to be \emph{reducible} or \emph{stuck}, such that
\begin{align*}
\textlog{reducible}(\expr) &\iff \Exists \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \\
\textlog{stuck}(\expr) &\iff \All \ectx, \expr'. \expr = \ectx[\expr'] \implies
% \textlog{stuck}(\expr) &\iff \All \ectx, \expr'. \expr = \ectx[\expr'] \implies
\lnot \textlog{reducible}(\expr')
\end{align*}
and the following hold
......@@ -340,14 +340,13 @@ Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \R
%
% Proof rules implicitly assume well-sortedness.
\subsection{Laws of intuitionistic higher-order logic with guarded recursion over a simply-typed lambda calculus}\label{sec:HOL}
% e\subsection{Laws of intuitionistic higher-order logic with guarded recursion over a simply-typed lambda calculus}\label{sec:HOL}
Standard.
This is entirely standard.
Soundness follows from the theorem that ${\cal U}(\any, \textdom{Prop})
: {\cal U}^\textrm{op} \to \textrm{Poset}$ is a hyperdoctrine.
: {\cal U}^{\textrm{op}} \to \textrm{Poset}$ is a hyperdoctrine.
\elide{
\begin{mathpar}
\inferH{Asm}
{\prop \in \pfctx}
......@@ -357,87 +356,86 @@ Soundness follows from the theorem that ${\cal U}(\any, \textdom{Prop})
{\pfctx \proves \prop(\term) \\ \pfctx \proves \term = \term'}
{\pfctx \proves \prop(\term')}
\and
\inferH{$\wedge$I}
\infer[$\wedge$I]
{\pfctx \proves \prop \\ \pfctx \proves \propB}
{\pfctx \proves \prop \wedge \propB}
\and
\inferH{$\wedge$EL}
\infer[$\wedge$EL]
{\pfctx \proves \prop \wedge \propB}
{\pfctx \proves \prop}
\and
\inferH{$\wedge$ER}
\infer[$\wedge$ER]
{\pfctx \proves \prop \wedge \propB}
{\pfctx \proves \propB}
\and
\inferH{$\vee$E}
\infer[$\vee$E]
{\pfctx \proves \prop \vee \propB \\
\pfctx, \prop \proves \propC \\
\pfctx, \propB \proves \propC}
{\pfctx \proves \propC}
\and
\inferH{$\vee$IL}
\infer[$\vee$IL]
{\pfctx \proves \prop }
{\pfctx \proves \prop \vee \propB}
\and
\inferH{$\vee$IR}
\infer[$\vee$IR]
{\pfctx \proves \propB}
{\pfctx \proves \prop \vee \propB}
\and
\inferH{$\Ra$I}
\infer[$\Ra$I]
{\pfctx, \prop \proves \propB}
{\pfctx \proves \prop \Ra \propB}
\and
\inferH{$\Ra$E}
\infer[$\Ra$E]
{\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop}
{\pfctx \proves \propB}
\and
\inferH{$\forall_1$I}
\infer[$\forall_1$I]
{\pfctx, x : \sort \proves \prop}
{\pfctx \proves \forall x: \sort.\; \prop}
\and
\inferH{$\forall_1$E}
\infer[$\forall_1$E]
{\pfctx \proves \forall X \in \sort.\; \prop \\
\pfctx \proves \term: \sort}
{\pfctx \proves \prop[\term/X]}
\and
\inferH{$\exists_1$E}
\infer[$\exists_1$E]
{\pfctx \proves \exists X\in \sort.\; \prop \\
\pfctx, X : \sort, \prop \proves \propB}
{\pfctx \proves \propB}
\and
\inferH{$\exists_1$I}
\infer[$\exists_1$I]
{\pfctx \proves \prop[\term/X] \\
\pfctx \proves \term: \sort}
{\pfctx \proves \exists X: \sort. \prop}
\and
\inferH{$\forall_2$I}
\infer[$\forall_2$I]
{\pfctx, \pvar: \Pred(\sort) \proves \prop}
{\pfctx \proves \forall \pvar\in \Pred(\sort).\; \prop}
\and
\inferH{$\forall_2$E}
\infer[$\forall_2$E]
{\pfctx \proves \forall \pvar. \prop \\
\pfctx \proves \propB: \Prop}
{\pfctx \proves \prop[\propB/\pvar]}
\and
\inferH{$\exists_2$E}
\infer[$\exists_2$E]
{\pfctx \proves \exists \pvar \in \Pred(\sort).\prop \\
\pfctx, \pvar : \Pred(\sort), \prop \proves \propB}
{\pfctx \proves \propB}
\and
\inferH{$\exists_2$I}
\infer[$\exists_2$I]
{\pfctx \proves \prop[\propB/\pvar] \\
\pfctx \proves \propB: \Prop}
{\pfctx \proves \exists \pvar. \prop}
\and
\inferHB{Elem}
\inferB[Elem]
{\pfctx \proves \term \in (X \in \sort). \prop}
{\pfctx \proves \prop[\term/X]}
\and
\inferHB{Elem-$\mu$}
\inferB[Elem-$\mu$]
{\pfctx \proves \term \in (\mu\pvar \in \Pred(\sort). \pred)}
{\pfctx \proves \term \in \pred[\mu\pvar \in \Pred(\sort). \pred/\pvar]}
\end{mathpar}
}
\subsection{Axioms from the logic of (affine) bunched implications}
\begin{mathpar}
......@@ -807,3 +805,8 @@ The following specializations cover all cases of a heap-manipulating lambda calc
The first is restricted to deterministic pure reductions, like $\beta$-reduction.
The second is suited to proving triples for (possibly non-deterministic) atomic expressions; for example, with $\expr \eqdef \;!\ell$ (dereferencing $\ell$) and $\state \eqdef h \mtimes \ell \mapsto \valB$ and $\pred(\val, \state') \eqdef \state' = (h \mtimes \ell \mapsto \valB) \land \val = \valB$, one obtains the axiom $\All h, \ell, \valB. \hoare{\ownPhys{h \mtimes \ell \mapsto \valB}}{!\ell}{\Ret\val. \val = \valB \land \ownPhys{h \mtimes \ell \mapsto \valB} }$.
%Axioms for CAS-like operations can be obtained by first deriving rules for the two possible cases, and then using the disjunction rule.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
......@@ -84,7 +84,7 @@ action on morphisms).
\textdom{Res} &\eqdef&
\{\, \rs = (\pres, \ghostRes) \mid
\pres \in \textdom{State} \uplus \{\munit\} \land \ghostRes \in \mcarp{\monoid} \,\} \\[0.5em]
(\pres, \ghostRes) \rsplit
(\pres, \ghostRes) \rtimes
(\pres', \ghostRes') &\eqdef&
\begin{cases}
(\pres, \ghostRes \mtimes \ghostRes') & \mbox{if $\pres' = \munit$ and $\ghostRes \mtimes \ghostRes' \neq \mzero$} \\
......@@ -93,7 +93,7 @@ action on morphisms).
\\[0.5em]
%
\rs \leq \rs' & \eqdef &
\Exists \rs''. \rs' = \rs \rsplit \rs''\\[1em]
\Exists \rs''. \rs' = \rs \rtimes \rs''\\[1em]
%
\UPred(\textdom{Res}) &\eqdef&
\{\, p \subseteq \mathbb{N} \times \textdom{Res} \mid
......@@ -149,7 +149,7 @@ For a set $X$, write $\Delta X$ for the discrete c.o.f.e.\ with $x \nequiv{n}
x'$ iff $n = 0$ or $x = x'$
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\semSort{\unit} &\eqdef& \Delta \{ \star \} \\
\semSort{\textsort{Unit}} &\eqdef& \Delta \{ \star \} \\
\semSort{\textsort{InvName}} &\eqdef& \Delta \mathbb{N} \\
\semSort{\textsort{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\
\semSort{\textsort{Monoid}} &\eqdef& \Delta |\monoid|
......@@ -234,7 +234,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\begin{align*}
\fullSat{\state}{\mask}{\rs}{W} &=
\begin{aligned}[t]
\{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rsplit \rsB).\pres = \state \land{}\\
\{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rtimes \rsB).\pres = \state \land{}\\
&\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\rsB) \land {}\\
&\quad\quad \iota \in \mask \ra (n, \rsB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \}
\end{aligned}
......@@ -295,9 +295,9 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\begin{aligned}[t]
\{\, (n, \rs) &\mid \All W_F \geq W. \All \rs_F, \mask_F, \state. \All k \leq n.\\
&\qquad
k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\rs \rsplit \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
&\qquad
\Exists W' \geq W_F. \Exists \rs'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k, \rs') \in q(W')
\Exists W' \geq W_F. \Exists \rs'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(W')
\,\}
\end{aligned}
\end{align*}
......@@ -392,19 +392,19 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\begin{align*}
\mathit{wp}_\mask(\expr, q) &\eqdef \Lam W.
\begin{aligned}[t]
\{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs \rsplit \rs_F}{W_F}) \implies{}\\
\{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \implies{}\\
&\qquad
(\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\
&\qquad\qquad
k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
&\qquad
(\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\
&\qquad\qquad
k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
&\qquad
(\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\
&\qquad\qquad
k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rsplit \rs_F}{W'}) \land \rs' = \rs_1' \rsplit \rs_2'~\land \\
k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land \rs' = \rs_1' \rtimes \rs_2'~\land \\
&\qquad\qquad
(k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
(k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
......@@ -520,3 +520,8 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\implies (n, \rs) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W)
\end{aligned}
\]
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
......@@ -52,6 +52,7 @@
\newcommand*{\axiomhref}[3]{\inferhref{#1}{#2}{}{#3}}
\newcommand*{\axiomH}[2]{\inferH{#1}{}{#2}}
\newcommand*{\inferhrefB}[4]{{\BIIMP\inferhref{#1}{#2}{#3}{#4}}}
\newcommand*{\inferB}[3][]{{\BIIMP\infer[#1]{#2}{#3}}}
\newcommand*{\inferHB}[3]{{\BIIMP\inferH{#1}{#2}{#3}}}
\newcommand*{\taghref}[2]{\label{#2}\tag{\rulenamestyle{#1}}}
\newcommand*{\tagH}[1]{\taghref{#1}{#1}}
......
This diff is collapsed.
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