# Changeset 393 for Deliverables/D3.1

Ignore:
Timestamp:
Dec 8, 2010, 6:08:05 PM (9 years ago)
Message:

A few more details in D3.1.

Location:
Deliverables/D3.1/Report
Files:
2 edited

### Legend:

Unmodified
 r381 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, \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'. 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}