X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=cf905c3c6155003bef0419d251ebafaef4cd1e36;hp=f4156b6131685dc6d81880ff80fec2d14b2bff16;hb=b21616e3601566e7b89293af948de0e0505dfc48;hpb=754d1564abbf23561192301163388a9494a91bbf diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index f4156b6..cf905c3 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -796,6 +796,7 @@ normal form. \placeintermezzo{}{ + \defref{substitution notation} \startframedtext[width=8cm,background=box,frame=no] \startalignment[center] {\tfa Substitution notation} @@ -888,7 +889,8 @@ This transformation is not needed to get an expression into intended normal form (since these bindings are part of the intended normal form), but makes the resulting \small{VHDL} a lot shorter. - + + \refdef{substitution notation} \starttrans letrec a0 = E0 @@ -1645,7 +1647,7 @@ This propagation makes higher order values become applied (in particular both of the alternatives of the case now have a - representable type. Completely applied top level functions (like the + representable type). Completely applied top level functions (like the first alternative) are now no longer invalid (they fall under \in{item}[item:completeapp] above). (Completely) applied lambda abstractions can be removed by β-abstraction. For our example, @@ -1820,6 +1822,7 @@ solves (part of) the polymorphism, higher order values and unrepresentable literals in an expression. + \refdef{substitution notation} \starttrans letrec a0 = E0 @@ -1942,7 +1945,6 @@ \todo{Examples. Perhaps reference the previous sections} - \section{Unsolved problems} The above system of transformations has been implemented in the prototype and seems to work well to compile simple and more complex examples of @@ -2058,6 +2060,37 @@ transformations will probably need updating to handle them in all cases. + \subsection{Normalization of stateful descriptions} + Currently, the intended normal form definition\refdef{intended + normal form definition} offers enough freedom to describe all + valid stateful descriptions, but is not limiting enough. It is + possible to write descriptions which are in intended normal + form, but cannot be translated into \VHDL in a meaningful way + (\eg, a function that swaps two substates in its result, or a + function that changes a substate itself instead of passing it to + a subfunction). + + It is now up to the programmer to not do anything funny with + these state values, whereas the normalization just tries not to + mess up the flow of state values. In practice, there are + situations where a Core program that \emph{could} be a valid + stateful description is not translateable by the prototype. This + most often happens when statefulness is mixed with pattern + matching, causing a state input to be unpacked multiple times or + be unpacked and repacked only in some of the code paths. + + \todo{example?} + + Without going into detail about the exact problems (of which + there are probably more than have shown up so far), it seems + unlikely that these problems can be solved entirely by just + improving the \VHDL state generation in the final stage. The + normalization stage seems the best place to apply the rewriting + needed to support more complex stateful descriptions. This does + of course mean that the intended normal form definition must be + extended as well to be more specific about how state handling + should look like in normal form. + \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: @@ -2105,12 +2138,15 @@ 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 - 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 α. + Before looking into how to prove these properties, we'll look at + transformation systems from a graph perspective. We will first define + the graph view and then illustrate it using a simple example from lambda + calculus (which is a different system than the Cλash normalization + system). 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; @@ -2158,10 +2194,10 @@ 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. + Of course the graph for Cλash 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 @@ -2211,7 +2247,6 @@ Also, since there is only one node in the normal set, it must obviously be \emph{deterministic} as well. - \todo{Add content to these sections} \subsection{Termination} In general, proving termination of an arbitrary program is a very hard problem. \todo{Ref about arbitrary termination} Fortunately,