\documentstyle{article}
\include{tcom}

\begin{document}

  
\section{Trying to get rid of localities by program transformation}
  
The issue of local variables was not neglected by Sato and Tamaki: the 
reason why in their seminal paper they restricted the application of 
the transformational method to horn-closed programs is precisely 
motivated by the requirement of avoiding universal quantification in 
the target program.  
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 tried to be eliminated by means of program 
transformation.  The TS and successor�s system are devoted to the 
transformation of (even first-order)  programs to achieve 
Prolog executability first and ultimately more efficiency.  Of course you 
have to be a beliver  (and you would be in a pretty 
good company, see \cite{PP95,DK95} for surveys) in the classical cycle: logical 
specification\ldots declarative logic program\ldots program 
transformation\ldots possibly partial evaluation and eventually 
compilation.  Indeed in the original paper Sato and Tamaki introduced 
the negation technique to try to compile first-order specification 
(with what they called the double negation technique that we will not 
discuss here) into horn-closed programs and later \cite{TS88} they extended 
to a general folding-unfolding method.

Therefore the situation is more subtle: nowadays the elimination of 
localities is not necessarily linked to the negation issue.  Local 
variables can roughly be divided into two large categories:
\begin{itemize}
\item
local variables that correspond to data structures built or visited by 
intermediate computation.  Consider the typical example of how (not) 
to average a list of numbers (and its optimization that can be found 
in \cite{PP94}):
\begin{Examplen}
\[\begin{tt}\begin{tabular} {llll} 
average(Xs,A) & \Ift & length(Xs,L), sumlist(Xs,S), A is S/A.
\end{tabular}\end{tt} \]
\end{Examplen}
  \item
  variables that  `read off` some local values: see for instance the 
  typing clause for application in $\l$-calculus or the transitive 
  closure predicate.
  \end{itemize}.
  
  Typically the first case corresponds to sloppy\footnote{Or 
  `declarative' programming, as you can easily come up with an 
  equivalent linear program by yourself} program writing, namely data 
  structures that are visited more than necessary; so this is a good 
  candidate to optimization, by means of unfolding (more precisely, by 
  unfolding-definition-folding in this order as the title in 
  \cite{PP95} rhymes).  On the other hand the \texttt{path} is 
  perfectly reasonable at first sight.

 Thus, unfortunately the situation is not so clear cut: to summarize
  
\begin{itemize}
\item 
  Not every eliminable local variables represents an intermediate 
  computation: the \texttt{path} example can be solved by unfolding: 
  The treatment is particularly simple; you just need to unfold the 
  \texttt{edge} predicate until it wires the 
  asserted graph into \texttt{path}. Of course you come up with a program whose 
  size is the double of the number of edges. Then computing the complement of the 
  program is a (tedious) routine.
\begin{Examplen}
\label{path-unfolded}
\[\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}

\item
not every unnecessary computation is represented by a local variable
\end{itemize}

 Note also that the UDF method requires some ingenuity and it is only 
 semimechanical, though a lot of research has been dedicated to the 
 automatic synthesis of {\em eureka} predicates, see for example 
 \cite{PP93}.  Moreover, as we exemplified earlier, it may suffer of 
 the usual combinatorial explosion problems typically associated to 
 partial deduction.


Moral: program transformation is not an exhaustive way of getting rid 
of localities, or in other term, not every local variable can be 
eliminated in a clean and mechanical. In this case we may want to live with extensional 
quantification. Since this entails a significant change in the 
operational semantics of uniform proofs and an additional source of 
non-determinism, a fair attempt to eliminate localities may be worthwhile
 (and does not to have necessarily to be  made visible to the user)

\subsection{Lifting localities}

Given the well-known input-output nature of logical variables, an 
obvious remark is that in certain cases local variables do not need to be local, but 
maybe brought to the surface, \ie made to appear in the head of the 
clause\footnote{Compare with the idea of `allowed' program, where each 
variable in  a program must appear in a positive literal: this is 
connected to the question of \emph{floundering} and is of no 
interest to us}.

There are a couple of immediate case where the process seems 
harmless, in the specific sense that the two programs are equivalent 
\wrt an opportune semantics, say the set of computed answer 
substitutions, restricted to the set of original variables. The real trick 
is showing equivalence to (finite) failure. My gutsy feeling is 
positive for the below cases.

\begin{enumerate}
\item Hierarchical programs: the absence of recursion make the 
lifting of localities trivial: for example
\begin{Examplen}
\[\begin{tt}\begin{tabular} {llll} 
average(Xs,L,S,A) & \Ift & length(Xs,L), sumlist(Xs,S), A is S/A.
\end{tabular}\end{tt} \]
\end{Examplen}
The set of answer substitutions of the lifted program restricted to 
$Xs,A$ is clearly equivalent to the source's one.
\item
Recursive predicates where lifting does not change the arity: this means that 
the lifted variables get buried inside some already existing data 
structure whose arity is then extended; in fact for this notion not to be 
trivial, we require the exclusion of the creation of \emph{new} 
data structures like say $X+Y$ where $Y$ is local.
\end{enumerate}
\begin{Examplen}
For example, we may change the declaration of application, with the 
understanding that $T2$ is an output variable.

\[\begin{tt}\begin{tabular} {llll} 
appt : exp -> exp -> tp -> exp.\\
\\
of (appt E1 E2 T2) T1 & \Ift & of E1 (T1 => T2) ,of E2 T2.
\end{tabular}\end{tt} \]
\end{Examplen}

The general case is more problematic; although the lifted variable is 
intended to be only output and hence should not affect the 
computation, it is not clear how to treat recursion.
\begin{Examplen}
\[\begin{tt}\begin{tabular} {llll} 
path3(X,Y,Z) & \Ift & edge(X,Y). \\
path3(X,Y,Z)& \Ift & edge(X,Z), path3(Z,Y,??). 
\end{tabular}\end{tt} \]
\end{Examplen}

Putting whichever non-local variable at ??  is arbitrarious does not 
preserve the sucess set, as shown next:
\begin{Examplen}
\[\begin{tt}\begin{tabular} {ll} 
edge(a,b).
edge(a,c).
edge(c,d).
edge(d,e).
\end{tabular}\end{tt} \]
\end{Examplen}

For any assigment to ?? the query path(a,e,Z) fails, as its 
insantiation with a constant precludes the next recursive call.


\begin{thebibliography}{999}
\bibitem {D9K} Deville \& Kiu-Lau  A survey of logic program synthesis. Journal of Logic Programming.
 {\bf 19--20} (1994)
\bibitem {PP93} Pettorossi A.,  Proietti  M. Synthesis of eureka definitions\ldots
\bibitem{PP94} Pettorossi A.,  Proietti  M.: Transformation of logic
programs: foundations and techniques.  Journal of Logic Programming.
 {\bf 19--20} (1994) 261--321    

\bibitem {PP95} Pettorossi A.,  Proietti  M. unfolding-definition-folding\ldots
\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 {ST88} Tamaki H.  \& T.Sato.   Deterministic Transformations 
and Deterministic Synhesis . In  {\em  Programmingof Future Generation 
Computing}, North-Holland 1988.


\end{thebibliography}
\end{document}


