X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=82305479b573f29b9b8e68a51c16c44305d17026;hp=77dd977c8e87f7175c5f16bdc375c2fa95717eda;hb=a8cc8a42f676a1ab1ddca1c84b017d059610783d;hpb=28b745e6faf774843ecdfbce67bdd22b8b4fc550 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 77dd977..8230547 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -224,7 +224,7 @@ -> State (Word, Word) -> (State (Word, Word), Word) - -- All arguments are an inital lambda + -- All arguments are an initial lambda -- (address, data, packed state) regbank = λa.λd.λsp. -- There are nested let expressions at top level @@ -374,7 +374,7 @@ | \italic{builtinapp} \stopbuffer - \placedefinition[][def:IntendedNormal]{Definition of the intended nnormal form using an \small{EBNF}-like syntax.} + \placedefinition[][def:IntendedNormal]{Definition of the intended normal form using an \small{EBNF}-like syntax.} {\defref{intended normal form definition} \typebufferlam{IntendedNormal}} @@ -387,7 +387,7 @@ ports are mapped to local signals (\italic{userarg}). Some of the others use a built-in construction (\eg\ the \lam{case} expression) or call a built-in function (\italic{builtinapp}) such as \lam{+} or \lam{map}. - For these, a hardcoded \small{VHDL} translation is available. + For these, a hard-coded \small{VHDL} translation is available. \section[sec:normalization:transformation]{Transformation notation} To be able to concisely present transformations, we use a specific format @@ -412,7 +412,7 @@ Nevertheless, we will more precisely specify their meaning below: \startdesc{} The expression pattern that will be matched - against (subexpressions of) the expression to be transformed. We call this a + against (sub-expressions of) the expression to be transformed. We call this a pattern, because it can contain \emph{placeholders} (variables), which match any expression or binder. Any such placeholder is said to be \emph{bound} to the expression it matches. It is convention to use an uppercase letter (\eg\ @@ -476,7 +476,7 @@ To understand this notation better, the step by step application of the η-expansion transformation to a simple \small{ALU} will be shown. Consider η-expansion, which is a common transformation from - labmda calculus, described using above notation as follows: + lambda calculus, described using above notation as follows: \starttrans E \lam{E :: a -> b} @@ -506,7 +506,7 @@ High -> (-) \stoplambda - There are a few subexpressions in this function to which we could possibly + There are a few sub-expressions in this function to which we could possibly apply the transformation. Since the pattern of the transformation is only the placeholder \lam{E}, any expression will match that. Whether the transformation applies to an expression is thus solely decided by the @@ -610,7 +610,7 @@ We look at the \lam{} pattern, which is \lam{E}. This means we bind \lam{E} to \lam{(+)}. We then replace the expression - with the \lam{}, replacing all occurences of + with the \lam{}, replacing all occurrences of \lam{E} with \lam{(+)}. In the \lam{}, the This gives us the replacement expression: \lam{λx.(+) x} (A lambda expression binding \lam{x}, with a body that applies the addition operator to \lam{x}). @@ -674,7 +674,7 @@ A \emph{hardware representable} (or just \emph{representable}) type or value is (a value of) a type that we can generate a signal for in hardware. For example, a bit, a vector of bits, a 32 bit unsigned word, etc. Values that are - not runtime representable notably include (but are not limited to): types, + not run-time representable notably include (but are not limited to): types, dictionaries, functions. \defref{representable} @@ -728,8 +728,8 @@ \stoplambda Now, we have replaced the \lam{a} binder with a reference to the \lam{x} - binder. No harm done here. But note that we see multiple occurences of the - \lam{c} binder. The first is a binding occurence, to which the second refers. + binder. No harm done here. But note that we see multiple occurrences of the + \lam{c} binder. The first is a binding occurrence, to which the second refers. The last, however refers to \emph{another} instance of \lam{c}, which is bound somewhere outside of this expression. Now, if we would apply beta reduction without taking heed of binder uniqueness, we would get: @@ -752,7 +752,7 @@ can be accessed. There are a number of ways to solve this. \small{GHC} has isolated this - problem to their binder substitution code, which performs \emph{deshadowing} + problem to their binder substitution code, which performs \emph{de-shadowing} during its expression traversal. This means that any binding that shadows another binding on a higher level is replaced by a new binder that does not shadow any other binding. This non-shadowing invariant is enough to prevent @@ -760,13 +760,13 @@ In our transformation system, maintaining this non-shadowing invariant is a bit harder to do (mostly due to implementation issues, the prototype - does not use \small{GHC}'s subsitution code). Also, the following points + does not use \small{GHC}'s substitution code). Also, the following points can be observed. \startitemize - \item Deshadowing does not guarantee overall uniqueness. For example, the + \item De-shadowing does not guarantee overall uniqueness. For example, the following (slightly contrived) expression shows the identifier \lam{x} bound in - two seperate places (and to different values), even though no shadowing + two separate places (and to different values), even though no shadowing occurs. \startlambda @@ -779,10 +779,10 @@ unique. \item When we know that all binders in an expression are unique, moving around - or removing a subexpression will never cause any binder conflicts. If we have - some way to generate fresh binders, introducing new subexpressions will not + or removing a sub-expression will never cause any binder conflicts. If we have + some way to generate fresh binders, introducing new sub-expressions will not cause any problems either. The only way to cause conflicts is thus to - duplicate an existing subexpression. + duplicate an existing sub-expression. \stopitemize Given the above, our prototype maintains a unique binder invariant. This @@ -830,7 +830,7 @@ 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 + occurrence of some expression (usually a variable reference) with another expression. There have been a lot of different notations used in literature for @@ -841,7 +841,7 @@ E[A=>B] \stoplambda - This means expression \lam{E} with all occurences of \lam{A} replaced + This means expression \lam{E} with all occurrences of \lam{A} replaced with \lam{B}. \stopframedtext } @@ -864,12 +864,12 @@ In our transformation system, this step helps to remove unwanted lambda abstractions (basically all but the ones at the top level). Other transformations (application propagation, non-representable inlining) make - sure that most lambda abstractions will eventually be reducable by + sure that most lambda abstractions will eventually be reducible by β-reduction. Note that β-reduction also works on type lambda abstractions and type applications as well. This means the substitution below also works on - type variables, in the case that the binder is a type variable and teh + type variables, in the case that the binder is a type variable and the expression applied to is a type. \starttrans @@ -1042,7 +1042,7 @@ This transform takes simple top level bindings generated by the \small{GHC} compiler. \small{GHC} sometimes generates very simple \quote{wrapper} bindings, which are bound to just a variable - reference, or contain just a (partial) function appliation with + reference, or contain just a (partial) function application with the type and dictionary arguments filled in (such as the \lam{(+)} in the example below). @@ -1088,9 +1088,9 @@ allowed in \VHDL\ architecture names\footnote{Technically, it is allowed to use non-alphanumerics when using extended identifiers, but it seems that none of the tooling likes - extended identifiers in filenames, so it effectively does not + extended identifiers in file names, so it effectively does not work.}, so the entity would be called \quote{w7aA7f} or - something similarly meaningless and autogenerated). + something similarly meaningless and auto-generated). \subsection{Program structure} These transformations are aimed at normalizing the overall structure @@ -1384,10 +1384,10 @@ \refdef{global variable} Note that references to \emph{global variables} (like a top level - function without arguments, but also an argumentless dataconstructors + function without arguments, but also an argumentless data-constructors like \lam{True}) are also simplified. Only local variables generate signals in the resulting architecture. Even though argumentless - dataconstructors generate constants in generated \VHDL\ code and could be + data-constructors generate constants in generated \VHDL\ code and could be mapped to an input port directly, they are still simplified to make the normal form more regular. @@ -1424,7 +1424,7 @@ reference. \item (A partial application of) a top level function (either built-in on user-defined). The function extraction transformation described in - this section takes care of turning every functiontyped argument into + this section takes care of turning every function-typed argument into (a partial application of) a top level function. \item Any expression that is not representable and does not have a function type. Since these can be any expression, there is no @@ -1433,7 +1433,7 @@ previous two categories. This means that \emph{any} Core expression that is used as an argument to a built-in function will be either transformed into one of the above categories, or end up in this - categorie. In any case, the result is in normal form. + category. In any case, the result is in normal form. \stopitemize As noted, the argument simplification will handle any representable @@ -1452,7 +1452,7 @@ translation rules needed for built-in functions, since they only need to handle (partial applications of) top level functions. - Any free variables occuring in the extracted arguments will become + Any free variables occurring in the extracted arguments will become parameters to the new global function. The original argument is replaced with a reference to the new function, applied to any free variables from the original argument. @@ -1464,7 +1464,7 @@ even more complicated expressions). \starttrans - M N \lam{M} is (a partial aplication of) a built-in function. + M N \lam{M} is (a partial application of) a built-in function. --------------------- \lam{f0 ... fn} are all free local variables of \lam{N} M (x f0 ... fn) \lam{N :: a -> b} ~ \lam{N} is not a (partial application of) a top level function @@ -1486,7 +1486,7 @@ Note that the function \lam{f} will still need normalization after this. - \subsection{Case normalisation} + \subsection{Case normalization} The transformations in this section ensure that case statements end up in normal form. @@ -1516,7 +1516,7 @@ False -> b \stopbuffer - \transexample{letflat}{Case normalisation}{from}{to} + \transexample{letflat}{Case normalization}{from}{to} \placeintermezzo{}{ @@ -1532,7 +1532,7 @@ The Haskell syntax offers the underscore as a wild binder that cannot even be referenced (It can be seen as introducing a new, - anonymous, binder everytime it is used). + anonymous, binder every time it is used). In these transformations, the term wild binder will sometimes be used to indicate that a binder must not be referenced. @@ -1600,7 +1600,7 @@ let bindings for each of the alternatives' value and a single selector case to select the right value out of these. - Technically, the defintion of this transformation would require + Technically, the definition of this transformation would require that the constructor for every alternative has exactly the same amount (\lam{m}) of arguments, but of course this transformation also applies when this is not the case. @@ -1789,7 +1789,7 @@ \startlambda f 1 2 \stoplambda - the subexpression \lam{f 1} has a function type. But this is + the sub-expression \lam{f 1} has a function type. But this is allowed, since it is inside a complete application. \stopitemize @@ -1918,7 +1918,7 @@ first argument and applies that function twice to the second argument. Again, we have made the function monomorphic for clarity, even though this function would be a lot more useful if it was polymorphic. The - function \lam{main} uses \lam{twice} to apply a lambda epression twice. + function \lam{main} uses \lam{twice} to apply a lambda expression twice. When faced with a user defined function, a body is available for that function. This means we could create a specialized version of the @@ -1955,7 +1955,7 @@ \subsubsection{Literals} There are a limited number of literals available in Haskell and Core. \refdef{enumerated types} When using (enumerating) algebraic - datatypes, a literal is just a reference to the corresponding data + data-types, a literal is just a reference to the corresponding data constructor, which has a representable type (the algebraic datatype) and can be translated directly. This also holds for literals of the \hs{Bool} Haskell type, which is just an enumerated type. @@ -1965,7 +1965,7 @@ literals for all three integer types supported (\hs{SizedWord}, \hs{SizedInt} and \hs{RangedWord}). This is implemented using Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method - that converts any \hs{Integer} to the Cλash datatypes. + that converts any \hs{Integer} to the Cλash data-types. When \GHC\ sees integer literals, it will automatically insert calls to the \hs{fromInteger} method in the resulting Core expression. For @@ -2059,11 +2059,11 @@ (λb -> add b 1) (add 1 x) \stopbuffer - \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to} + \transexample{nonrepinline}{Non-representable binding inlining}{from}{to} \subsubsection[sec:normalization:specialize]{Function specialization} This transform removes arguments to user-defined functions that are - not representable at runtime. This is done by creating a + not representable at run-time. This is done by creating a \emph{specialized} version of the function that only works for one particular value of that argument (in other words, the argument can be removed). @@ -2102,7 +2102,7 @@ exactly one free variable, itself, we would only replace that argument with itself). - This shows that any free local variables that are not runtime + This shows that any free local variables that are not run-time representable cannot be brought into normal form by this transform. We rely on an inlining or β-reduction transformation to replace such a variable with an expression we can propagate again. @@ -2136,7 +2136,7 @@ The argument that we are specializing for, \lam{Y_i}, is put inside the new function body. The old function body is applied to it. Since we use this new function only in place of an application with that - particular argument \lam{Y_i}, behaviour should not change. + particular argument \lam{Y_i}, behavior should not change. Note that the types of the arguments of our new function are taken from the types of the \emph{actual} arguments (\lam{T0 ... Tn}). This @@ -2177,7 +2177,7 @@ A possible solution to this would be to use the following alternative transformation, which is of course no longer normal β-reduction. The - followin transformation has not been tested in the prototype, but is + following transformation has not been tested in the prototype, but is given here for future reference: \starttrans @@ -2250,7 +2250,7 @@ For this particular problem, the solutions for duplication of work seem from the previous section seem to fix the determinism of our transformation system as well. However, it is likely that there are - other occurences of this problem. + other occurrences of this problem. \subsection[sec:normalization:castproblems]{Casts} We do not fully understand the use of cast expressions in Core, so @@ -2268,14 +2268,14 @@ 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). + function that changes a sub-state itself instead of passing it to + a sub-function). 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 + stateful description is not translatable 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. @@ -2297,7 +2297,7 @@ 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: + number of sub-questions: \startitemize[KR] \item[q:termination] Does our system \emph{terminate}? Since our system will @@ -2489,7 +2489,7 @@ will of course leave the meaning unchanged and is thus \emph{sound}. - The current prototype has only been verified in an ad-hoc fashion + The current prototype has only been verified in an ad hoc fashion by inspecting (the code for) each transformation. A more formal verification would be more appropriate. @@ -2508,12 +2508,12 @@ assign a meaning to Core expressions that assumes neither. Since each of the transformations can be applied to any - subexpression as well, there is a constraint on our meaning + sub-expression as well, there is a constraint on our meaning definition: the meaning of an expression should depend only on the - meaning of subexpressions, not on the expressions themselves. For + meaning of sub-expressions, not on the expressions themselves. For example, the meaning of the application in \lam{f (let x = 4 in x)} should be the same as the meaning of the application in \lam{f - 4}, since the argument subexpression has the same meaning (though + 4}, since the argument sub-expression has the same meaning (though the actual expression is different). \subsection{Completeness}