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

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 37895b3..cf905c3 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -2138,12 +2138,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 +2194,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 +2247,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,