Add some stuff about provable properties of our system.

This section is still incomplete, the actual (ideas for) proofs still need
to be written.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index b74333ae103c15d51b08fa37cc708cc7c3f1503b..17a37c6713fbbf057cbf0a72fd86d2a3e044e1e2 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -314,7 +314,7 @@ subtractor.}
     {\boxedgraphic{NormalComplete}}{The architecture described by the normal form.}
   \stopcombination
 
-\subsection{Normal form definition}
+\subsection{Intended normal form definition}
 Now we have some intuition for the normal form, we can describe how we want
 the normal form to look like in a slightly more formal manner. The following
 EBNF-like description completely captures the intended structure (and
@@ -1512,3 +1512,150 @@ x = let x = add 1 2 in x
 \stopbuffer
 
 \transexample{Return value simplification}{from}{to}
+
+\section{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
+  number of subquestions:
+
+  \startitemize[KR]
+  \item[q:termination] Does our system \emph{terminate}? Since our system will
+  keep running as long as transformations apply, there is an obvious risk that
+  it will keep running indefinitely. One transformation produces a result that
+  is transformed back to the original by another transformation, for example.
+  \item[q:soundness] Is our system \emph{sound}? Since our transformations
+  continuously modify the expression, there is an obvious risk that the final
+  normal form will not be equivalent to the original program: Its meaning could
+  have changed.
+  \item[q:completeness] Is our system \emph{complete}? Since we have a complex
+  system of transformations, there is an obvious risk that some expressions will
+  not end up in our intended normal form, because we forgot some transformation.
+  In other words: Does our transformation system result in our intended normal
+  form for all possible inputs?
+  \item[q:determinism] Is our system \emph{deterministic}? Since we have defined
+  no particular order in which the transformation should be applied, there is an
+  obvious risk that different transformation orderings will result in
+  \emph{different} normal forms. They might still both be intended normal forms
+  (if our system is \emph{complete}) and describe correct hardware (if our
+  system is \emph{sound}), so this property is less important than the previous
+  three: The translator would still function properly without it.
+  \stopitemize
+
+  \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
+    all possible Core expressions. The (directed) edges of the graph are
+    transformations. When a transformation α applies to an expression \lam{A} to
+    produce an expression \lam{B}, we add an edge from the node for \lam{A} to the
+    node for \lam{B}, labeled α.
+
+    \startuseMPgraphic{TransformGraph}
+      save a, b, c, d;
+
+      % Nodes
+      newCircle.a(btex \lam{(λx.λy. (+) x y) 1} etex);
+      newCircle.b(btex \lam{λy. (+) 1 y} etex);
+      newCircle.c(btex \lam{(λx.(+) x) 1} etex);
+      newCircle.d(btex \lam{(+) 1} etex);
+
+      b.c = origin;
+      c.c = b.c + (4cm, 0cm);
+      a.c = midpoint(b.c, c.c) + (0cm, 4cm);
+      d.c = midpoint(b.c, c.c) - (0cm, 3cm);
+
+      % β-conversion between a and b
+      ncarc.a(a)(b) "name(bred)";
+      ObjLabel.a(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
+      ncarc.b(b)(a) "name(bexp)", "linestyle(dashed withdots)";
+      ObjLabel.b(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
+
+      % η-conversion between a and c
+      ncarc.a(a)(c) "name(ered)";
+      ObjLabel.a(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
+      ncarc.c(c)(a) "name(eexp)", "linestyle(dashed withdots)";
+      ObjLabel.c(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
+
+      % η-conversion between b and d
+      ncarc.b(b)(d) "name(ered)";
+      ObjLabel.b(btex $\xrightarrow[normal]{}{η}$ etex) "labpathname(ered)", "labdir(rt)";
+      ncarc.d(d)(b) "name(eexp)", "linestyle(dashed withdots)";
+      ObjLabel.d(btex $\xleftarrow[normal]{}{η}$ etex) "labpathname(eexp)", "labdir(lft)";
+
+      % β-conversion between c and d
+      ncarc.c(c)(d) "name(bred)";
+      ObjLabel.c(btex $\xrightarrow[normal]{}{β}$ etex) "labpathname(bred)", "labdir(rt)";
+      ncarc.d(d)(c) "name(bexp)", "linestyle(dashed withdots)";
+      ObjLabel.d(btex $\xleftarrow[normal]{}{β}$ etex) "labpathname(bexp)", "labdir(lft)";
+
+      % Draw objects and lines
+      drawObj(a, b, c, d);
+    \stopuseMPgraphic
+
+    \placeexample[right][ex:TransformGraph]{Partial graph of a labmda calculus
+    system with β and η reduction (solid lines) and expansion (dotted lines).}
+        \boxedgraphic{TransformGraph}
+
+    Of course our graph is unbounded, since we can construct an infinite amount of
+    Core expressions. Also, there might potentially be multiple edges between two
+    given nodes (with different labels), though seems unlikely to actually happen
+    in our system.
+
+    See \in{example}[ex:TransformGraph] for the graph representation of a very
+    simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
+    y) 1}, \lam{λy. (+) 1 y}, \lam{(λx.(+) x) 1} and \lam{(+) 1}. The
+    transformation system consists of β-reduction and η-reduction (solid edges) or
+    β-reduction and η-reduction (dotted edges).
+
+    TODO: Define β-reduction and η-reduction?
+
+    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}.
+
+    From such a graph, we can derive some properties easily:
+    \startitemize[KR]
+      \item A system will \emph{terminate} if there is no path of infinite length
+      in the graph (this includes cycles).
+      \item Soundness is not easily represented in the graph.
+      \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.
+      \item A system is deterministic if all paths from a node, which end in a node
+      in the normal set, end at the same node.
+    \stopitemize
+
+    When looking at the \in{example}[ex:TransformGraph], we see that the system
+    terminates for both the reduction and expansion systems (but note that, for
+    expansion, this is only true because we've limited the possible expressions!
+    In comlete lambda calculus, there would be a path from \lam{(λx.λy. (+) x y)
+    1} to \lam{(λx.λy.(λz.(+) z) x y) 1} to \lam{(λx.λy.(λz.(λq.(+) q) z) x y) 1}
+    etc.)
+
+    If we would consider the system with both expansion and reduction, there would
+    no longer be termination, since there would be cycles all over the place.
+
+    The reduction and expansion systems have a normal set of containing just
+    \lam{(+) 1} or \lam{(λx.λy. (+) x y) 1} respectively. Since all paths in
+    either system end up in these normal forms, both systems are \emph{complete}.
+    Also, since there is only one normal form, it must obviously be
+    \emph{deterministic} as well.
+
+  \subsection{Termination}
+    Approach: Counting.
+
+    Church-Rosser?
+
+  \subsection{Soundness}
+    Needs formal definition of semantics.
+    Prove for each transformation seperately, implies soundness of the system.
+   
+  \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.
+
+  \subsection{Determinism}
+    How to prove this?