author Matthijs Kooijman Fri, 4 Dec 2009 13:03:24 +0000 (14:03 +0100) committer Matthijs Kooijman Fri, 4 Dec 2009 13:03:24 +0000 (14:03 +0100)

index 6117008..cf905c3 100644 (file)
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;
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