X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=cf905c3c6155003bef0419d251ebafaef4cd1e36;hp=d3b37003774e7f81abf3e6fc8661bf47811ce3f6;hb=b21616e3601566e7b89293af948de0e0505dfc48;hpb=2790ccea19648fe307a85db7485ec8986e63e773 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index d3b3700..cf905c3 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -28,11 +28,7 @@ core can describe expressions that do not have a direct hardware interpretation. - \todo{Describe core properties not supported in \VHDL, and describe how the - \VHDL we want to generate should look like.} - \section{Normal form} - \todo{Refresh or refer to distinct hardware per application principle} The transformations described here have a well-defined goal: To bring the program in a well-defined form that is directly translatable to hardware, while fully preserving the semantics of the program. We refer to this form as @@ -629,9 +625,11 @@ In particular, we define no particular order of transformations. Since transformation order should not influence the resulting normal form, - \todo{This is not really true, but would like it to be...} this leaves - the implementation free to choose any application order that results in - an efficient implementation. + this leaves the implementation free to choose any application order that + results in an efficient implementation. Unfortunately this is not + entirely true for the current set of transformations. See + \in{section}[sec:normalization:non-determinism] for a discussion of this + problem. When applying a single transformation, we try to apply it to every (sub)expression in a function, not just the top level function body. This allows us to @@ -641,8 +639,6 @@ In the following sections, we will be using a number of functions and notations, which we will define here. - \todo{Define substitution (notation)} - \subsubsection{Concepts} A \emph{global variable} is any variable (binder) that is bound at the top level of a program, or an external module. A \emph{local variable} is any @@ -799,8 +795,34 @@ optimizations, but they are required to get our program into intended normal form. + \placeintermezzo{}{ + \defref{substitution notation} + \startframedtext[width=8cm,background=box,frame=no] + \startalignment[center] + {\tfa Substitution notation} + \stopalignment + \blank[medium] + + In some of the transformations in this chapter, we need to perform + substitution on an expression. Substitution means replacing every + occurence of some expression (usually a variable reference) with + another expression. + + There have been a lot of different notations used in literature for + specifying substitution. The notation that will be used in this report + is the following: + + \startlambda + E[A=>B] + \stoplambda + + This means expression \lam{E} with all occurences of \lam{A} replaced + with \lam{B}. + \stopframedtext + } + + \defref{beta-reduction} \subsubsection[sec:normalization:beta]{β-reduction} - \defref{beta-reduction} β-reduction is a well known transformation from lambda calculus, where it is the main reduction step. It reduces applications of lambda abstractions, removing both the lambda abstraction and the application. @@ -867,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 @@ -1084,7 +1107,7 @@ \transexample{apppropcase}{Application propagation for a case expression}{from}{to} - \subsubsection{Let recursification} + \subsubsection[sec:normalization:letrecurse]{Let recursification} This transformation makes all non-recursive lets recursive. In the end, we want a single recursive let in our normalized program, so all non-recursive lets can be converted. This also makes other @@ -1367,7 +1390,7 @@ False -> b \stopbuffer - \transexample{letflat}{Let flattening}{from}{to} + \transexample{letflat}{Case normalisation}{from}{to} \subsubsection{Case simplification} @@ -1624,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, @@ -1799,6 +1822,7 @@ solves (part of) the polymorphism, higher order values and unrepresentable literals in an expression. + \refdef{substitution notation} \starttrans letrec a0 = E0 @@ -1921,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 @@ -1990,7 +2013,7 @@ let y = (a * b) in y + y \stoplambda - \subsection{Non-determinism} + \subsection[sec:normalization:non-determinism]{Non-determinism} As an example, again consider the following expression: \startlambda @@ -2037,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: @@ -2084,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; @@ -2137,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 @@ -2190,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,