{\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
\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?
projects / matthijs / master-project / report.git / blobdiff