-> 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
| \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}}
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
Nevertheless, we will more precisely specify their meaning below:
\startdesc{<original expression>} 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\
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}
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
We look at the \lam{<original expression>} pattern, which is \lam{E}.
This means we bind \lam{E} to \lam{(+)}. We then replace the expression
- with the \lam{<transformed expression>}, replacing all occurences of
+ with the \lam{<transformed expression>}, replacing all occurrences of
\lam{E} with \lam{(+)}. In the \lam{<transformed expression>}, 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}).
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}
\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:
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
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
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
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
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
}
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
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).
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
\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.
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
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
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.
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
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.
False -> b
\stopbuffer
- \transexample{letflat}{Case normalisation}{from}{to}
+ \transexample{letflat}{Case normalization}{from}{to}
\placeintermezzo{}{
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.
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.
\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
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
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.
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
(λ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).
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.
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
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
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
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.
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
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.
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}
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:
projects / matthijs / master-project / report.git / blobdiff