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:
projects / matthijs / master-project / report.git / commitdiff