Improve graph representation section a bit.

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 61170088d4b13a23166d7a7683628629f7442351..cf905c3c6155003bef0419d251ebafaef4cd1e36 100644 (file)
--- 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