X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=0700b3acb044d0f4ac7929d0fbddde318f169295;hp=78b7a1d2e2352662fd759c495af3904b7fdd163b;hb=a4cfdaa1ccacc0dcf9a374bb202b247b8f28dccb;hpb=e1d6411fce1aecea50e986f4002c7241b88f4342 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 78b7a1d..0700b3a 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 @@ -555,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 @@ -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,33 @@ 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 + } + \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 +888,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 @@ -1405,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 @@ -1458,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 @@ -1624,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, @@ -1799,6 +1821,7 @@ solves (part of) the polymorphism, higher order values and unrepresentable literals in an expression. + \refdef{substitution notation} \starttrans letrec a0 = E0 @@ -1921,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 @@ -1990,7 +2012,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 +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: @@ -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,