From: Matthijs Kooijman Date: Fri, 30 Oct 2009 16:42:54 +0000 (+0100) Subject: Add some stuff about provable properties of our system. X-Git-Tag: final-thesis~185 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=c684451040e76a69af0507381dd03ecc2b72d0f1;p=matthijs%2Fmaster-project%2Freport.git 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 b74333a..17a37c6 100644 --- 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?