X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=907411e877ef6bb9d2d1a30c67fd5d94774527a5;hp=37895b3a5543f6c189625da9b4645ae9d418bccc;hb=8ec0a2193fa53fd7bc15c2118e676f82e904f493;hpb=d081fa803ef206c6f7ffa72941ca7f008915c69f

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 37895b3..907411e 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -2060,7 +2060,7 @@
         transformations will probably need updating to handle them in all
         cases.
 
-      \subsection{Normalization of stateful descriptions}
+      \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
         Currently, the intended normal form definition\refdef{intended
         normal form definition} offers enough freedom to describe all
         valid stateful descriptions, but is not limiting enough. It is
@@ -2079,8 +2079,6 @@
         matching, causing a state input to be unpacked multiple times or
         be unpacked and repacked only in some of the code paths.
 
-        \todo{example?}
-
         Without going into detail about the exact problems (of which
         there are probably more than have shown up so far), it seems
         unlikely that these problems can be solved entirely by just
@@ -2090,6 +2088,9 @@
         of course mean that the intended normal form definition must be
         extended as well to be more specific about how state handling
         should look like in normal form.
+        \in{Section}[sec:prototype:statelimits] already contains a
+        tight description of the limitations on the use of state
+        variables, which could be adapted into the intended normal form.
 
   \section[sec:normalization:properties]{Provable properties}
     When looking at the system of transformations outlined above, there are a
@@ -2138,12 +2139,15 @@
     possible proof strategies are shown below.
 
     \subsection{Graph representation}
-      Before looking into how to prove these properties, we'll look at our
-      transformation system from a graph perspective. The nodes of the graph are
-      all possible Core expressions. The (directed) edges of the graph are
-      transformations. When a transformation α applies to an expression \lam{A} to
-      produce an expression \lam{B}, we add an edge from the node for \lam{A} to the
-      node for \lam{B}, labeled α.
+      Before looking into how to prove these properties, we'll look at
+      transformation systems from a graph perspective. We will first define
+      the graph view and then illustrate it using a simple example from lambda
+      calculus (which is a different system than the Cλash normalization
+      system). The nodes of the graph are all possible Core expressions. The
+      (directed) edges of the graph are transformations. When a transformation
+      α applies to an expression \lam{A} to produce an expression \lam{B}, we
+      add an edge from the node for \lam{A} to the node for \lam{B}, labeled
+      α.
 
       \startuseMPgraphic{TransformGraph}
         save a, b, c, d;
@@ -2191,10 +2195,10 @@
       system with β and η reduction (solid lines) and expansion (dotted lines).}
           \boxedgraphic{TransformGraph}
 
-      Of course our graph is unbounded, since we can construct an infinite amount of
-      Core expressions. Also, there might potentially be multiple edges between two
-      given nodes (with different labels), though seems unlikely to actually happen
-      in our system.
+      Of course the graph for Cλash is unbounded, since we can construct an
+      infinite amount of Core expressions. Also, there might potentially be
+      multiple edges between two given nodes (with different labels), though
+      seems unlikely to actually happen in our system.
 
       See \in{example}[ex:TransformGraph] for the graph representation of a very
       simple lambda calculus that contains just the expressions \lam{(λx.λy. (+) x
@@ -2244,7 +2248,6 @@
       Also, since there is only one node in the normal set, it must obviously be
       \emph{deterministic} as well.
 
-    \todo{Add content to these sections}
     \subsection{Termination}
       In general, proving termination of an arbitrary program is a very
       hard problem. \todo{Ref about arbitrary termination} Fortunately,