Ignore:
Timestamp:
Mar 2, 2012, 3:16:23 PM (8 years ago)
Author:
tranquil
Message:

small correction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1797 r1801  
    10391039
    10401040It 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.
     1041In 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
     1042decreasing 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
     1043call\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.}.
    10421044
    10431045The 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.
     
    10501052$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
    10511053\item
    1052 $\mathtt{required} \subseteq \mathtt{visited}$,
    1053 \item
    1054 $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
     1054$\mathtt{required} \subseteq \mathtt{visited}$.
     1055% \item
     1056% $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
    10551057\end{enumerate}
    10561058
Note: See TracChangeset for help on using the changeset viewer.