Changeset 1801 for Deliverables/D1.2/CompilerProofOutline/outline.tex
 Timestamp:
 Mar 2, 2012, 3:16:23 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1797 r1801 1039 1039 1040 1040 It is easy to see that this linearisation process eventually terminates. 1041 In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising. 1041 In particular, the size of the visited label set is non decreasing and bounded above by the size of the graph that we are linearising. Moreover when it remains the same we are 1042 decreasing the size of the todo list. So the lexicographic measure $(n  \mathtt{visited}, \mathtt{todo})$ (where $n$ is the number of nodes in the graph) strictly decreases upon each 1043 call\footnote{The use of a lexicographic measure can be avoided by taking the first element in $\mathtt{todo}$ not in $\mathtt{visited}$ and discarding all preceding nodes before making the recursive call.}. 1042 1044 1043 1045 The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph. … … 1050 1052 $\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$, 1051 1053 \item 1052 $\mathtt{required} \subseteq \mathtt{visited}$ ,1053 \item1054 $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.1054 $\mathtt{required} \subseteq \mathtt{visited}$. 1055 % \item 1056 % $\mathtt{visited} \cap \mathtt{todo} = \emptyset$. 1055 1057 \end{enumerate} 1056 1058
Note: See TracChangeset
for help on using the changeset viewer.