X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=03cafcf23ed1ac11d908b283a9300328429a16e7;hp=fd62fea830bb20103c8c653ef1ceeb5db745d2da;hb=2ff5f767f17203c764a8ec9ef6711b234c1deb6d;hpb=58a5aa7ca5edc07ba1070f4f4ed384b42e36e8f3 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index fd62fea..03cafcf 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -21,12 +21,12 @@ \stopcombination } - The first step in the core to \small{VHDL} translation process, is normalization. We - aim to bring the core description into a simpler form, which we can + The first step in the Core to \small{VHDL} translation process, is normalization. We + aim to bring the Core description into a simpler form, which we can subsequently translate into \small{VHDL} easily. This normal form is needed because - the full core language is more expressive than \small{VHDL} in some + the full Core language is more expressive than \small{VHDL} in some areas (higher-order expressions, limited polymorphism using type - classes, etc.) and because core can describe expressions that do not + classes, etc.) and because Core can describe expressions that do not have a direct hardware interpretation. \section{Normal form} @@ -224,7 +224,8 @@ -> State (Word, Word) -> (State (Word, Word), Word) - -- All arguments are an inital lambda (address, data, packed state) + -- All arguments are an initial lambda + -- (address, data, packed state) regbank = λa.λd.λsp. -- There are nested let expressions at top level let @@ -320,7 +321,7 @@ Now we have some intuition for the normal form, we can describe how we want the normal form to look like in a slightly more formal manner. The EBNF-like description in \in{definition}[def:IntendedNormal] captures - most of the intended structure (and generates a subset of \GHC's core + most of the intended structure (and generates a subset of \GHC's Core format). There are two things missing from this definition: cast expressions are @@ -373,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}} @@ -386,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 @@ -411,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\ @@ -475,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} @@ -505,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 @@ -609,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}). @@ -673,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} @@ -712,7 +713,7 @@ \subsection[sec:normalization:uniq]{Binder uniqueness} A common problem in transformation systems, is binder uniqueness. When not considering this problem, it is easy to create transformations that mix up - bindings and cause name collisions. Take for example, the following core + bindings and cause name collisions. Take for example, the following Core expression: \startlambda @@ -727,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: @@ -751,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 @@ -759,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 @@ -778,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 @@ -796,7 +797,6 @@ unique. This is done by generating a fresh binder for every binder used. This also replaces binders that did not cause any conflict, but it does ensure that all binders within the function are generated by the same unique supply. - \refdef{fresh binder} \item Whenever a new binder must be generated, we generate a fresh binder that is guaranteed to be different from \emph{all binders generated so far}. This can thus never introduce duplication and will maintain the invariant. @@ -820,41 +820,41 @@ \in{section}[sec:normalization:transformation]. \subsection{General cleanup} - These transformations are general cleanup transformations, that aim to - make expressions simpler. These transformations usually clean up the - mess left behind by other transformations or clean up expressions to - expose new transformation opportunities for other transformations. - - Most of these transformations are standard optimizations in other - compilers as well. However, in our compiler, most of these are not just - 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] + \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 + occurrence 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: - 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. + \startlambda + E[A=>B] + \stoplambda - 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: + This means expression \lam{E} with all occurrences of \lam{A} replaced + with \lam{B}. + \stopframedtext + } - \startlambda - E[A=>B] - \stoplambda + These transformations are general cleanup transformations, that aim to + make expressions simpler. These transformations usually clean up the + mess left behind by other transformations or clean up expressions to + expose new transformation opportunities for other transformations. - This means expression \lam{E} with all occurences of \lam{A} replaced - with \lam{B}. - \stopframedtext - } + Most of these transformations are standard optimizations in other + compilers as well. However, in our compiler, most of these are not just + optimizations, but they are required to get our program into intended + normal form. \subsubsection[sec:normalization:beta]{β-reduction} β-reduction is a well known transformation from lambda calculus, where it is @@ -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 @@ -913,7 +913,6 @@ either. To prevent the \VHDL\ generation from breaking on these artifacts, this transformation removes them. - \todo{Do not use old-style numerals in transformations} \starttrans letrec a0 = E0 @@ -1042,7 +1041,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). @@ -1078,7 +1077,7 @@ \in{Example}[ex:trans:toplevelinline] shows a typical application of the addition operator generated by \GHC. The type and dictionary arguments used here are described in - \in{Section}[section:prototype:polymorphism]. + \in{Section}[sec:prototype:coretypes]. Without this transformation, there would be a \lam{(+)} entity in the \VHDL\ which would just add its inputs. This generates a @@ -1088,9 +1087,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 @@ -1273,45 +1272,54 @@ This transformation ensures that the return value of a function is always a simple local variable reference. - This transformation only applies to the entire body of a - function instead of any subexpression in a function. This is - achieved by the contexts, like \lam{x = E}, though this is - strictly not correct (you could read this as "if there is any - function \lam{x} that binds \lam{E}, any \lam{E} can be - transformed, while we only mean the \lam{E} that is bound by - \lam{x}). - - Note that the return value is not simplified if its not - representable. Otherwise, this would cause a direct loop with - the inlining of unrepresentable bindings. If the return value is - not representable because it has a function type, η-expansion - should make sure that this transformation will eventually apply. - If the value is not representable for other reasons, the - function result itself is not representable, meaning this - function is not translatable anyway. - - \starttrans - x = E \lam{E} is representable - ~ \lam{E} is not a lambda abstraction - E \lam{E} is not a let expression - --------------------------- \lam{E} is not a local variable reference - letrec x = E in x - \stoptrans + The basic idea of this transformation is to take the body of a + function and bind it with a let expression (so the body of that let + expression becomes a variable reference that can be used as the output + port). If the body of the function happens to have lambda abstractions + at the top level (which is allowed by the intended normal + form\refdef{intended normal form definition}), we take the body of the + inner lambda instead. If that happens to be a let expression already + (which is allowed by the intended normal form), we take the body of + that let (which is not allowed to be anything but a variable reference + according the the intended normal form). + + This transformation uses the context conditions in a special way. + These contexts, like \lam{x = λv1 ... λvn.E}, are above the dotted + line and provide a condition on the environment (\ie\ they require a + certain top level binding to be present). These ensure that + expressions are only transformed when they are in the functions + \quote{return value} directly. This means the context conditions have + to interpreted in the right way: not \quote{if there is any function + \lam{x} that binds \lam{E}, any \lam{E} can be transformed}, but we + mean only the \lam{E} that is bound by \lam{x}). + + Be careful when reading the transformations: Not the entire function + from the context is transformed, just a part of it. + + Note that the return value is not simplified if it is not representable. + Otherwise, this would cause a loop with the inlining of + unrepresentable bindings in + \in{section}[sec:normalization:nonrepinline]. If the return value is + not representable because it has a function type, η-expansion should + make sure that this transformation will eventually apply. If the + value is not representable for other reasons, the function result + itself is not representable, meaning this function is not translatable + anyway. \starttrans - x = λv0 ... λvn.E \lam{E} is representable - ~ \lam{E} is not a lambda abstraction - E \lam{E} is not a let expression - --------------------------- \lam{E} is not a local variable reference - letrec x = E in x + x = λv1 ... λvn.E \lam{n} can be zero + ~ \lam{E} is representable + E \lam{E} is not a lambda abstraction + --------------------------- \lam{E} is not a let expression + letrec y = E in y \lam{E} is not a local variable reference \stoptrans \starttrans - x = λv0 ... λvn.let ... in E - ~ \lam{E} is representable - E \lam{E} is not a local variable reference - ----------------------------- - letrec x = E in x + x = λv1 ... λvn.letrec binds in E \lam{n} can be zero + ~ \lam{E} is representable + letrec binds in E \lam{E} is not a local variable reference + ------------------------------------ + letrec binds; y = E in y \stoptrans \startbuffer[from] @@ -1319,12 +1327,40 @@ \stopbuffer \startbuffer[to] - x = letrec x = add 1 2 in x + x = letrec y = add 1 2 in y \stopbuffer \transexample{retvalsimpl}{Return value simplification}{from}{to} + + \startbuffer[from] + x = λa. add 1 a + \stopbuffer + + \startbuffer[to] + x = λa. letrec + y = add 1 a + in + y + \stopbuffer + + \transexample{retvalsimpllam}{Return value simplification with a lambda abstraction}{from}{to} - \todo{More examples} + \startbuffer[from] + x = letrec + a = add 1 2 + in + add a 3 + \stopbuffer + + \startbuffer[to] + x = letrec + a = add 1 2 + y = add a 3 + in + y + \stopbuffer + + \transexample{retvalsimpllet}{Return value simplification with a let expression}{from}{to} \subsection[sec:normalization:argsimpl]{Representable arguments simplification} This section contains just a single transformation that deals with @@ -1347,10 +1383,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. @@ -1387,16 +1423,16 @@ 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 transformation needed. Note that this category is exactly all expressions that are not transformed by the transformations for the - previous two categories. This means that \emph{any} core expression + 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 @@ -1415,7 +1451,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. @@ -1427,7 +1463,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 @@ -1449,7 +1485,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. @@ -1479,7 +1515,7 @@ False -> b \stopbuffer - \transexample{letflat}{Case normalisation}{from}{to} + \transexample{letflat}{Case normalization}{from}{to} \placeintermezzo{}{ @@ -1495,7 +1531,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. @@ -1549,10 +1585,12 @@ \startitemize \item An extractor case with a single alternative that picks a field - from a datatype, \eg\ \lam{case x of (a, b) -> a}. + from a datatype, \eg\ \lam{case x of (a, b) -> + a}.\defref{extractor case} \item A selector case with multiple alternatives and only wild binders, that makes a choice between expressions based on the constructor of another - expression, \eg\ \lam{case x of Low -> a; High -> b}. + expression, \eg\ \lam{case x of Low -> a; High -> + b}.\defref{selector case} \stopitemize For an arbitrary case, that has \lam{n} alternatives, with @@ -1561,7 +1599,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. @@ -1680,7 +1718,7 @@ actual transformations. \subsubsection{Removing Polymorphism} - As noted in \in{section}[sec:prototype:polymporphism], + As noted in \in{section}[sec:prototype:coretypes], polymorphism is made explicit in Core through type and dictionary arguments. To remove the polymorphism from a function, we can simply specialize the polymorphic function for @@ -1750,7 +1788,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 @@ -1879,7 +1917,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 @@ -1913,10 +1951,10 @@ twice). This is discussed in more detail in \in{section}[sec:normalization:duplicatework]. - \subsubsection{Literals} + \subsubsection[sec:normalization:literals]{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. @@ -1926,7 +1964,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 @@ -1971,7 +2009,7 @@ to specialize away any unrepresentable literals that are used as function arguments. The following two transformations do exactly this. - \subsubsection{Non-representable binding inlining} + \subsubsection[sec:normalization:nonrepinline]{Non-representable binding inlining} This transform inlines let bindings that are bound to a non-representable value. Since we can never generate a signal assignment for these bindings (we cannot declare a signal assignment @@ -2020,11 +2058,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). @@ -2063,7 +2101,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. @@ -2097,7 +2135,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 @@ -2110,7 +2148,7 @@ \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 - hardware descriptions. \todo{Ref christiaan?} However, this normalization + hardware descriptions \cite[baaij09]. However, this normalization system has not seen enough review and work to be complete and work for every Core expression that is supplied to it. A number of problems have already been identified and are discussed in this section. @@ -2138,7 +2176,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 @@ -2211,14 +2249,14 @@ 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 there are probably expressions involving cast expressions that cannot be brought into intended normal form by this transformation system. - The uses of casts in the core system should be investigated more and + The uses of casts in the Core system should be investigated more and transformations will probably need updating to handle them in all cases. @@ -2229,14 +2267,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. @@ -2258,7 +2296,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 @@ -2376,7 +2414,7 @@ outgoing edges (meaning no transformation applies to it). The set of nodes without outgoing edges is called the \emph{normal set}. Similarly, the set of nodes containing expressions in intended normal form - \refdef{intended normal form} is called the \emph{intended normal set}. + \refdef{intended normal form definition} is called the \emph{intended normal set}. From such a graph, we can derive some properties easily: \startitemize[KR] @@ -2450,7 +2488,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. @@ -2466,15 +2504,15 @@ our compilation to \VHDL. The main difference seems to be that in hardware every expression is always evaluated, while in software it is only evaluated if needed, but it should be possible to - assign a meaning to core expressions that assumes neither. + 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} @@ -2506,7 +2544,7 @@ By systematically reviewing the entire Core language definition along with the intended normal form definition (both of which have a similar structure), it should be possible to identify all - possible (sets of) core expressions that are not in intended + possible (sets of) Core expressions that are not in intended normal form and identify a transformation that applies to it. This approach is especially useful for proving completeness of our @@ -2520,5 +2558,24 @@ we need to check every (set of) transformation(s) separately. \todo{Perhaps do a few steps of the proofs as proof-of-concept} + \subsection{Determinism} + A well-known technique for proving determinism in lambda calculus + and other reduction systems, is using the Church-Rosser property + \cite[church36]. A reduction system has the CR property if and only if: + + \placedefinition[here]{Church-Rosser theorem} + {\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}} + + Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In + other words, there is a set of transformations that can transform + \lam{A} to \lam{B}. \lam{=>} is used to mean \emph{implies}. + + For a transformation system holding the Church-Rosser property, it + is easy to show that it is in fact deterministic. Showing that this + property actually holds is a harder problem, but has been + done for some reduction systems in the lambda calculus + \cite[klop80]\ \cite[barendregt84]. Doing the same for our + transformation system is probably more complicated, but not + impossible. % vim: set sw=2 sts=2 expandtab: