Remove some progress documents, they are being stored elsewhere.

[matthijs/master-project/report.git] / Chapters / Normalization.tex

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 82305479b573f29b9b8e68a51c16c44305d17026..03cafcf23ed1ac11d908b283a9300328429a16e7 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -913,7 +913,6 @@
         either. To prevent the \VHDL\ generation from breaking on these
         artifacts, this transformation removes them.
 
         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
         \starttrans
         letrec
           a0 = E0


@@ -1952,7 +1951,7 @@
         twice). This is discussed in more detail in
         \in{section}[sec:normalization:duplicatework].
 
         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
         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


@@ -2149,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
   \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.
     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.


@@ -2559,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}
       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:
 
 % vim: set sw=2 sts=2 expandtab: