Changeset 1435 for Deliverables/D4.2-4.3

Timestamp:

Oct 21, 2011, 5:24:08 PM (9 years ago)

Author:

sacerdot

Message:

More on dependent types. One citation is missing.

File:

• Deliverables/D4.2-4.3/reports/D4-2.tex (modified) (2 diffs)

Deliverables/D4.2-4.3/reports/D4-2.tex

@@ -330 +330 @@
 \label{subsect.use.of.dependent.types}
 
-We see two potential ways in which a compiler can fail to compile a program:
+We see several potential ways in which a compiler can fail to compile a program:
 \begin{enumerate}
 \item
 The program is malformed, and there is no hope of making sense of the program.
 \item
-The compiler is buggy, or an invariant in the compiler is invalidated, for example, if the program is too large to fit into the processor's code memory.
+The compiler is buggy, or an invariant in the compiler is invalidated.
+\item Some non complete heuristics in the compiler fails.
+\item The compiled code exhausts some bounded resource, tipically the
+processor's code memory.
 \end{enumerate}
+Standard compilers can fail for all the above reasons. Certified compilers
+are only required to rule out the second class of failures, but they can
+still fail for all other reasons. In particular, a compiler that systematically
+refuses to compile any well formed program is a sound compiler. On the contrary,
+we would like our certified compiler to fail only in the fourth case. We
+plan to achieve this aim using the following strategy. First of all,
+the compiler is abstracted over all non complete heuristics, seen as total
+functions. To obtain an executable code, the compiler is eventually composed
+with implementations of the strategies, and the composition takes care of the
+possibility that the heuristics can fail to find a solution. Secondly,
+we will reject all malformed programs using dependent types:
+only well-formed programs should typecheck and the compiler can be applied only
+to well-typed programs. Finally, exhaustion of bounded resources can be checked
+only at the very end of the compilation. Therefore, all intermediate compilation
+steps are now total functions that cannot diverge, nor fail: these properties
+are directly guaranteed by the type system of Matita.
+
+At the moment, the plan has not been fulfilled, and we are improving the code
+according to the plan by progressively strenghthening the code by means of
+dependent types. We now detail the different ways in which dependent types
+have been exploited so far. 
+
 First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions.
 There are numerous examples of this throughout the backend.
@@ -370 +395 @@
 \end{lstlisting}
 Here, \texttt{codeT} is a parameterised type representing the `structure' of the function's body (a graph in graph based languages, and a list in the linearised LIN language).
-Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph.
-A similar device exists for the exit label.
-
-Finally, we make use of dependent types for another reason: experimentation.
+Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph. A similar device exists for the exit label.
+
+We make use of dependent types also for another reason: experimentation.
 Namely, CompCert makes little use of dependent types to encode invariants.
 In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of `stress testing' Matita's support for dependent types.
-In particular, we would like to make use of Matita's support for `Russell'-style reasoning.
+
+Moreover, at the moment we make practically no use of inductive predicates
+to specify compiler invariants and to describe the semantics of intermediate
+languages. On the contrary, all predicates are computable functions. Therefore,
+the proof style that we will adopt will be necessarily significantly different
+from, say, CompCert's one. At the moment, in Matita ``Russell-''-style reasoning
+(in the sense of~\cite{sozeauXXX}) seems to be the best solution to work on
+computable functions. This style is heavily based on the idea that all
+computable functions should be specified using dependent types to describe
+their pre and post-conditions. As a consequence, it is natural to add
+dependent types almost everywhere in the code.
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%