Finalize the proofs section.
authorMatthijs Kooijman <matthijs@stdin.nl>
Mon, 30 Nov 2009 19:50:12 +0000 (20:50 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Mon, 30 Nov 2009 19:50:12 +0000 (20:50 +0100)
Also add a section about proofs to the future work section.

Chapters/Future.tex
Chapters/Normalization.tex
Outline

index daeee3f..852d14f 100644 (file)
@@ -616,4 +616,12 @@ lightly.
   methods for describing don't care conditions. Possibly there are completely
   other methods which work better.
 
+\section{Correctness proofs of the normalization system}
+As stated in \in{section}[sec:normalization:properties], there are a
+number of properties we would like to see verified about the
+normalization system.  In particular, the \emph{termination} and
+\emph{completeness} of the system would be a good candidate for future
+research. Specifying formal semantics for the Core language in
+order to verify the \emph{soundness} of the system would be an even more
+challenging task.
 % vim: set sw=2 sts=2 expandtab:
index 941958d..4e00759 100644 (file)
       Some clauses have an expression listed in parentheses. These are conditions
       that need to apply to the clause.
 
+      \defref{intended normal form definition}
       \todo{Fix indentation}
       \startlambda
       \italic{normal} = \italic{lambda}
         \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
 
 
-  \section{Provable properties}
+  \section[sec:normalization:properties]{Provable properties}
     When looking at the system of transformations outlined above, there are a
     number of questions that we can ask ourselves. The main question is of course:
     \quote{Does our system work as intended?}. We can split this question into a
     three: The translator would still function properly without it.
     \stopitemize
 
+    Unfortunately, the final transformation system has only been
+    developed in the final part of the research, leaving no more time
+    for verifying these properties. In fact, it is likely that the
+    current transformation system still violates some of these
+    properties in some cases and should be improved (or extra conditions
+    on the input hardware descriptions should be formulated).
+
+    This is most likely the case with the completeness and determinism
+    properties, perhaps als the termination property. The soundness
+    property probably holds, since it is easier to manually verify (each
+    transformation can be reviewed separately).
+
+    Even though no complete proofs have been made, some ideas for
+    possible proof strategies are shown below.
+
     \subsection{Graph representation}
       Before looking into how to prove these properties, we'll look at our
       transformation system from a graph perspective. The nodes of the graph are
       Note that the normal form of such a system consists of the set of nodes
       (expressions) without outgoing edges, since those are the expression to which
       no transformation applies anymore. We call this set of nodes the \emph{normal
-      set}.
+      set}. The set of nodes containing expressions in intended normal
+      form \refdef{intended normal form} is called the \emph{intended
+      normal set}.
 
       From such a graph, we can derive some properties easily:
       \startitemize[KR]
         \item A system is \emph{complete} if all of the nodes in the normal set have
         the intended normal form. The inverse (that all of the nodes outside of
         the normal set are \emph{not} in the intended normal form) is not
-        strictly required.
+        strictly required. In other words, our normal set must be a
+        subset of the intended normal form, but they do not need to be
+        the same set.
+        form.
         \item A system is deterministic if all paths starting at a particular
         node, which end in a node in the normal set, end at the same node.
       \stopitemize
 
     \todo{Add content to these sections}
     \subsection{Termination}
-      Approach: Counting.
-
-      Church-Rosser?
+      In general, proving termination of an arbitrary program is a very
+      hard problem. \todo{Ref about arbitrary termination} Fortunately,
+      we only have to prove termination for our specific transformation
+      system.
+
+      A common approach for these kinds of proofs is to associate a
+      measure with each possible expression in our system. If we can
+      show that each transformation strictly decreases this measure
+      (\ie, the expression transformed to has a lower measure than the
+      expression transformed from).  \todo{ref about measure-based
+      termination proofs / analysis}
+      
+      A good measure for a system consisting of just β-reduction would
+      be the number of lambda expressions in the expression. Since every
+      application of β-reduction removes a lambda abstraction (and there
+      is always a bounded number of lambda abstractions in every
+      expression) we can easily see that a transformation system with
+      just β-reduction will always terminate.
+
+      For our complete system, this measure would be fairly complex
+      (probably the sum of a lot of things). Since the (conditions on)
+      our transformations are pretty complex, we would need to include
+      both simple things like the number of let expressions as well as
+      more complex things like the number of case expressions that are
+      not yet in normal form.
+
+      No real attempt has been made at finding a suitable measure for
+      our system yet.
 
     \subsection{Soundness}
-      Needs formal definition of semantics.
-      Prove for each transformation seperately, implies soundness of the system.
-     
+      Soundness is a property that can be proven for each transformation
+      separately. Since our system only runs separate transformations
+      sequentially, if each of our transformations leaves the
+      \emph{meaning} of the expression unchanged, then the entire system
+      will of course leave the meaning unchanged and is thus
+      \emph{sound}.
+
+      The current prototype has only been verified in an ad-hoc fashion
+      by inspecting (the code for) each transformation. A more formal
+      verification would be more appropriate.
+
+      To be able to formally show that each transformation properly
+      preserves the meaning of every expression, we require an exact
+      definition of the \emph{meaning} of every expression, so we can
+      compare them. Currently there seems to be no formal definition of
+      the meaning or semantics of \GHC's core language, only informal
+      descriptions are available.
+
+      It should be possible to have a single formal definition of
+      meaning for Core for both normal Core compilation by \GHC and for
+      our compilation to \VHDL. The main difference seems to be that in
+      hardware every expression is always evaluated, while in software
+      it is only evaluated if needed, but it should be possible to
+      assign a meaning to core expressions that assumes neither.
+      
+      Since each of the transformations can be applied to any
+      subexpression as well, there is a constraint on our meaning
+      definition: The meaning of an expression should depend only on the
+      meaning of subexpressions, not on the expressions themselves. For
+      example, the meaning of the application in \lam{f (let x = 4 in
+      x)} should be the same as the meaning of the application in \lam{f
+      4}, since the argument subexpression has the same meaning (though
+      the actual expression is different).
+      
     \subsection{Completeness}
-      Show that any transformation applies to every Core expression that is not
-      in normal form. To prove: no transformation applies => in intended form.
-      Show the reverse: Not in intended form => transformation applies.
+      Proving completeness is probably not hard, but it could be a lot
+      of work. We have seen above that to prove completeness, we must
+      show that the normal set of our graph representation is a subset
+      of the intended normal set.
+
+      However, it is hard to systematically generate or reason about the
+      normal set, since it is defined as any nodes to which no
+      transformation applies. To determine this set, each transformation
+      must be considered and when a transformation is added, the entire
+      set should be re-evaluated. This means it is hard to show that
+      each node in the normal set is also in the intended normal set.
+      Reasoning about our intended normal set is easier, since we know
+      how to generate it from its definition. \refdef{intended normal
+      form definition}.
+
+      Fortunately, we can also prove the complement (which is
+      equivalent, since $A \subseteq B \Leftrightarrow \overline{B}
+      \subseteq \overline{A}$): Show that the set of nodes not in
+      intended normal form is a subset of the set of nodes not in normal
+      form. In other words, show that for every expression that is not
+      in intended normal form, that there is at least one transformation
+      that applies to it (since that means it is not in normal form
+      either and since $A \subseteq C \Leftrightarrow \forall x (x \in A
+      \rightarrow x \in C)$).
+
+      By systematically reviewing the entire Core language definition
+      along with the intended normal form definition (both of which have
+      a similar structure), it should be possible to identify all
+      possible (sets of) core expressions that are not in intended
+      normal form and identify a transformation that applies to it.
+      
+      This approach is especially useful for proving completeness of our
+      system, since if expressions exist to which none of the
+      transformations apply (\ie if the system is not yet complete), it
+      is immediately clear which expressions these are and adding
+      (or modifying) transformations to fix this should be relatively
+      easy.
+
+      As observed above, applying this approach is a lot of work, since
+      we need to check every (set of) transformation(s) separately.
 
-    \subsection{Determinism}
-      How to prove this?
+      \todo{Perhaps do a few steps of the proofs as proof-of-concept}
 
 % vim: set sw=2 sts=2 expandtab:
diff --git a/Outline b/Outline
index 8f2d0c3..533ca69 100644 (file)
--- a/Outline
+++ b/Outline
@@ -56,3 +56,5 @@ TODO: Expand on "representable"
 TODO: Register
 TODO: Variable vs binder
 TODO: simplification -> Normalisation?
+TODO: Use saturated (application) instead of complete (application)?
+TODO: core => Core