comments

[Matthew Fluet]

> I am reading Theorem 2 and not having any luck understanding it.  I can not for
> the life of me understand why the following statement is true.
> 
> Anyways, it's getting late enough, and we're hurting for space enough that I'm
> inclined to drop the proof of theorem 2 (possibly replacing it by a short
> sketch, which you write, since I am confused).
> 
> Thoughts?

I'm very wary of dropping the entire proof, because the transformation
section is a little weak on solid guarantees as it is.  I've rewritten all
but the first paragraph of the proof to the following, which hopefully is
a clearer proof. 

Consider a fixed path $p$ from \main{} to $l_i$, composed of nontail
calls $(g_j,g_{j+1},k_j) \in \Nontail$ and tail calls $(g_j,g_{j+1})
\in \Tail$.  There is a least $j$ such that $g_j \in
\{l_0,\ldots,l_n\}$, say $g_j = l_{i'}$.  Furthermore, the prefix of
$p$ with $j' < j$ forms a path $p'$ from \main{} to $g_{j}$.  By the
minimality of $j$ and condition (2), $g_{j'} \neq l_{i'+1}$ for each
$(g_{j'}, g_{j'+1}) \in \Tail$ on $p'$.  Likewise, by the minimality
of $j$ and condition (1), $k_{j'} \neq l_{i'+1}$ for each $(g_{j'},
g_{j'+1},k_{j'}) \in \Nontail$ on $p'$.

A simple argument by induction on the length of the path $p'$, similar
to the one used in the proof of Lemma~\ref{lem:reach_iff_neqUncalled},
shows that $\A(g_{j'}) \neq l_{i'+1}$ for all functions $g_{j'}$ on
the path from \main{} to $l_{i'}$.  Thus $\A(l_{i'}) \neq l_{i'+1}$,
which is a contradiction.


I also reinstated the sentence about G being two trees, because it fits
and I dislike ending a section with a proof.

I'm starting a last readthrough of the whole paper with these changes.