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
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
data-types, a literal is just a reference to the corresponding data
\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.
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: