From: Matthijs Kooijman Date: Fri, 4 Dec 2009 13:03:24 +0000 (+0100) Subject: Improve graph representation section a bit. X-Git-Tag: final-thesis~105 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=a5c24fad8b59d741bc4bafd73405bb54b5c3934e;p=matthijs%2Fmaster-project%2Freport.git Improve graph representation section a bit. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 6117008..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