X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=03cafcf23ed1ac11d908b283a9300328429a16e7;hp=82305479b573f29b9b8e68a51c16c44305d17026;hb=HEAD;hpb=a8cc8a42f676a1ab1ddca1c84b017d059610783d

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 8230547..03cafcf 100644
--- 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.
 
-        \todo{Do not use old-style numerals in transformations}
         \starttrans
         letrec
           a0 = E0
@@ -1952,7 +1951,7 @@
         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
@@ -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
-    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.
@@ -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}
+  \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: