X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=0700b3acb044d0f4ac7929d0fbddde318f169295;hp=3d53853a58129f8b8cf90e5a22b8da3f02f75d30;hb=19c17205efa182b80916caa31afeadad9d2dd5b5;hpb=0eb8796e904c051f3103e10629dad4a3d13bfec5 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 3d53853..0700b3a 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -551,7 +551,7 @@ \stoplambda Again, the transformation does not apply to this lambda abstraction, so we - look at its body. For brevity, we'll put the case statement on one line from + look at its body. For brevity, we'll put the case expression on one line from now on. \startlambda @@ -821,7 +821,6 @@ \stopframedtext } - \defref{beta-reduction} \subsubsection[sec:normalization:beta]{β-reduction} β-reduction is a well known transformation from lambda calculus, where it is the main reduction step. It reduces applications of lambda abstractions, @@ -1428,7 +1427,7 @@ \stoptrans \todo{Check the subscripts of this transformation} - Note that this transformation applies to case statements with any + Note that this transformation applies to case expressions with any scrutinee. If the scrutinee is a complex expression, this might result in duplicate hardware. An extra condition to only apply this transformation when the scrutinee is already simple (effectively @@ -1481,10 +1480,10 @@ \in{section}[sec:transformation:caseremoval]. \subsubsection[sec:transformation:caseremoval]{Case removal} - This transform removes any case statements with a single alternative and + This transform removes any case expression with a single alternative and only wild binders. - These "useless" case statements are usually leftovers from case simplification + These "useless" case expressions are usually leftovers from case simplification on extractor case (see the previous example). \starttrans @@ -1647,7 +1646,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, @@ -1945,7 +1944,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 @@ -2061,6 +2059,38 @@ transformations will probably need updating to handle them in all cases. + \subsection[sec:normalization:stateproblems]{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. + + 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. + \in{Section}[sec:prototype:statelimits] already contains a + tight description of the limitations on the use of state + variables, which could be adapted into the intended 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: @@ -2108,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; @@ -2161,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 @@ -2214,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,