Changeset 393 for Deliverables/D3.1

Timestamp:

Dec 8, 2010, 6:08:05 PM (10 years ago)

Author:

campbell

Message:

A few more details in D3.1.

Location:

Deliverables/D3.1/Report

Files:

• report.pdf (modified) (previous)
• report.tex (modified) (3 diffs)

Deliverables/D3.1/Report/report.tex

@@ -580 +580 @@
 The definition also incorporates errors, and uses a coercion to automatically
 transform values from the plain error monad.
-\todo{should perhaps give more details of the resumption monad?}
+
+The definition of the monad is:
+\begin{quote}
+\begin{lstlisting}
+ninductive IO (output:Type) (input:output $\rightarrow$ Type) (T:Type) : Type :=
+| Interact : $\forall$o:output. (input o $\rightarrow$ IO output input T) $\rightarrow$ IO output input T
+| Value : T $\rightarrow$ IO output input T
+| Wrong : IO output input T.
+
+nlet rec bindIO (O:Type) (I:O $\rightarrow$ Type) (T,T':Type) (v:IO O I T) (f:T $\rightarrow$ IO O I T') on v : IO O I T' :=
+match v with
+[ Interact out k $\Rightarrow$ (Interact ??? out ($\lambda$res. bindIO O I T T' (k res) f))
+| Value v' $\Rightarrow$ (f v')
+| Wrong $\Rightarrow$ Wrong O I T'
+].
+\end{lstlisting}
+\end{quote}
+Note that the type of the input value is dependent on the output value.
+This enables us to ensure that the input is always well-typed.  An
+alternative approach is a check in the semantics, but this causes
+programs to fail in a way that has no counterpart in the inductive
+semantics.
 
 The execution of assignments is straightforward,
@@ -714 +735 @@
 \end{lstlisting}
 \end{quote}
-\begin{quote}
 We then show the completeness theorems, such as
+\begin{quote}
 \begin{lstlisting}
 ntheorem step_complete: $\forall$ge,s,tr,s'.
@@ -723 +744 @@
 by case analysis on the inductive derivation and a mixture of
 reduction and rewriting.
-\todo{Whole execution equivalence}
+
+Showing the equivalence of whole program execution is a little
+trickier.  Our executable semantics produces a coinductive
+\lstinline'execution' which is really a tree of executions, branching
+at each I/O resumption on the input value:
+\begin{quote}
+[TODO]
+\end{quote}
+However, the inductive semantics divides program behaviours into four
+categories which have \emph{individual} (co)inductive descriptions:
+\begin{itemize}
+\item successfully terminating executions;
+\item programs which eventually diverge (with an empty trace);
+\item programs which keep interacting in some way (with an infinite
+  trace\footnote{In our setting this includes passing through cost
+    labels as well as I/O.}; and
+\item programs which \emph{go wrong}.
+\end{itemize}
+
+We cannot constructively decide which of these categories an execution
+can fit into because the properties they describe are undecidable.
+Hence we follow CompCert's approach for showing that one of the
+behaviours always exists using classical logic.  Thus we characterise
+the executions, then show the existence of the inductive semantics'
+behaviour that matches.  We limit the scope of classical reasoning by
+taking the relevant axioms as hypotheses:
+\begin{quote}
+\begin{lstlisting}
+ntheorem exec_inf_equivalence:
+  $\forall$classic:($\forall$P:Prop.P $\vee$ $\neg$P).
+  $\forall$constructive_indefinite_description:($\forall$A:Type. $\forall$P:A$\rightarrow$Prop. ($\exists$x. P x) $\rightarrow$ $\Sigma$x : A. P x).
+  $\forall$p. $\exists$b.execution_matches_behavior (exec_inf p) b $\wedge$ exec_program p b.
+\end{lstlisting}
+\end{quote}
 
 \subsection{Animation of simple C programs}