\documentstyle{article} 
\include{tcom}
 \begin{document} The issue of 
local variables was not neglected by Sato at al.; the reason why in 
his seminal paper he restricted the application of the 
transformational method to horn-closed programs is precisely motivated 
by the requirement of avoiding universal quantification.  Indeed in 
the broader picture of the general transformational approach initiated 
in \cite{TS84}, non-horn closed programs may not occur, as local 
variables are eliminated by means of the unfolding (more precisely, by 
unfolding-definition-folding in this order as the title in \cite{PP95} 
rhymes).  The TS and successors's system is devoted to the 
transformation of programs to achieve more efficiency; in this sense 
local variables usually correspond to data structures built by 
intermediate computation that can be optimized, % namely data 
structures that are visited more than necessary.  The treatment with 
this example is particularly simple; you just need to unfold the 
`edge' predicate until it wires into `path' the asserted graph 
example.  Then computing The complement of the program is routine.  
\begin{Examplen} \label{path-unfoldded} \[\begin{tt}\begin{tabular} 
{llll} path(a,Y) & \Ift & path(b,Y)\\ path(b,Y) & \Ift & path(c,Y)\\ 
path(a,b).\\ path(b,c).  \end{tabular}\end{tt} \] \end{Examplen} Note 
that this method requires some ingenuity and is only semimechanical, 
though a lot of research has been dedicated to the automatic synthesis 
of {\em eureka} predicates, see \cite{PP93}.  Moreover it suffers of 
the usual combinatorial explosion problems typically associated to 
partial deduction.  Note also: \begin{itemize} \item Not every local 
variables represents an intermediate computation that can be 
eliminated: see the path example \item not every unnecessary 
computation is represented by a local variable \end{itemize} Moral: 
program transformation is not an exhaustive way of getting rid of 
localities, or in other term, mot every local variable can be 
eliminated.  In this case we have to live with extensional 
quantification.  \bibitem {TS84} Tamaki H.  \& T.Sato.  Unfold/Fold 
Transformations of Logic Program.  In/ S.-A.  Tarnlund (ed.){\em Proc.  
Second Int.  Conf.  on Logic Programming}, pp.  127--139, 1984 
\bibitem {PP95} Proietti Pettirossi U-D-F \end{document}
