\title{Towards a Logic for Reasoning about Logic Programs Transformation}

\author{Alberto Momigliano\thanks{This work was mostly completed during a
visit by the first
author to the  Dipartimento di Scienze dell'Informazione, Universita'
degli studi di  Milano.} \\
Department of Philosophy \\
Carnegie Mellon University\\
15213 Pittsburgh PA, USA \\
Tel. +1-412-268-1413\\
{\tt am4e@andrew.cmu.edu}
\and
Mario Ornaghi\\
 Dipartimento di Scienze dell'Informazione\\
 Universita' degli studi di  Milano\\
 Via Comelico 39/41, Milano, Italy \\
Tel. +39-2-55006331\\
{\tt ornaghi@dsi.unimi.it}}

\date{}
\maketitle

\newcommand{\PQ}{\[ \cQ = \frac{\Pi_1}{C_1\If
\Gamma_1}{r_1},\dots,\frac{\Pi_n}{C_n \If
\Gamma_n}{r_n} \]}
\begin{abstract}
We  give a proof-theoretic analysis of logic
programs transformations,  viewed as operations on proof trees in the sense
of \cite{Hal90,Hod93,Mom94,Mom97}.  We  present a logic for reasoning about
(equivalence preserving) transformations of logic programs.
% We concentrate our analysis
% on \emph{Partial Deduction}, but we pursue also \emph{ Fold/Unfold}.
Our main tool is the usage of inference
rules; the target program may be obtained as a set of clause
introduction proofs with axioms from the source program.  The rules
are \emph{admissible}, that is every proof according to the latter  can be
translated
back in a derivation of the same consequence built from the source program
 \emph{without} those rules.
Finally, the proof-theoretic framework--we hope to show-- is much simpler
and direct than
the one based on resolution.  Moreover, it allows a uniform
generalization of the basic results  to other \lp languages satisfying
the simple requirement of \emph{regularity}.
\end{abstract}

\section{Introduction}

We  give a proof-theoretic analysis of logic
programs transformations,  viewed as operations on proof trees in the sense
of \cite{Hal90,Hod93,Mom94,Mom97}.  We  present a logic for reasoning about
(equivalence preserving) transformations of logic programs.
 Our framework is natural
deduction, although a totally analogous presentation can be given in
terms of sequent calculi with definitional reflection \cite{SH94}.
We are not
going to fully detail in this abstract the systems we are using, though we have
shown elsewhere \cite{Mom94} (and it is now beginning to be common
knowledge, see
\cite{Hod93}) that,\wrt the language of definite
clauses, interpreting $:-$ and $,$ as
implication and conjunction yields positive intuitionistic, \ie
minimal logic.  Our  basic system, let us call it $L_{0}$, contains only the
assumption rule and a rule for applying clauses ($\ap$), similar to the
rule of modus ponens.

 We shall follow this path:
\begin{enumerate}
        \item  We achieve the transformation  via the usage of inference
        rules; thus,  the target program may be obtained as a set $\cQ$ of
clause
        introduction proofs with axioms from the source program $\cP$ of the
        form:

 \PQ
        \item We show the rules to be (weakly) admissible, that is every
proof $\Pi
        :: A$ which uses those rules can be translated in a proof
        $\trad(\Pi)$ of the same consequence  \emph{without} them in the
basic system and
        axioms from $\Pi$.  As the proofs in $L_{0}$ correspond to
\SLD-derivations,
        this means that every derivation from $\cQ = C_1\If \Gamma_1,\dots,C_n
        \If \Gamma_n$ gets translated in a derivation from $\cP$.

        \item  We will look for some adequacy results. Namely,
        verifying that the success set is preserved requires certain
        completeness conditions on $\Pi_{1} ,\ldots,\Pi_{n}$;  for
        finite failure we need furthermore the \emph{strict} monotonicity
of the translation
        function.
\end{enumerate}

We pursue two applications PD and FU\ldots
 Our perspective and future aim is
the introduction of a general calculus tailored to the proof-theory of
the transformation of (logic) programs.  \medskip

The paper is organized as follows: in Section \ref{back} we review the
basic notions of our framework \cite{Mom94,Mom97} and we relate it to
\SLD-resolution \wrt success and failure.  Section (\ref{general}) presents
the  general
transformation schema. The next Section (\ref{pv}) depicts the
proof-theoretical reconstruction of Partial Deduction. Section
\ref{pt} targets Program Transformation more in general. After a
brief Conclusion


\section{Background on Proof Trees}
\label{back}
First we recall some necessary basic definitions: we assume some
familiarities with
standard notions of natural deduction \cite{Pra65} and \lp \cite{Ap90}.

We use a variant of the Axiom Application Rule introduced in
\cite{Mom94}.  We consider the \emph{Clause Application Rule} $\ap$,
for applying axioms of the form $B \If A_{1}, \dots, A_{n}$.  Using the
formalism
of natural deduction, $\ap$ can be expressed as follows:
\[
\frac{\theta A_1\cdots \theta A_n \quad\quad B \If A_1 , \dots ,
A_n}{\theta B}{\ap}
\]
where the applied clause is the {\em major premise}, $\q A_1,\dots,\q A_n$
is the (possibly empty, if $n=0$)
sequence of the {\em minor premises} and $\q B$ is the consequence.
Next, we inductively introduce the notion of {\em proof tree} (pt).

\begin{definition}[Proof Tree]
An atom $A$ is a (trivial) {\em proof tree}.  If $\Pi_1::\q A_1$,\ldots,
$\Pi_n::\q A_n$ are proof trees and $\cC$ is a clause of the form $B \If
A_1, \dots,
A_n$, then the following is also a {\em
proof tree}:
\[
{{{\displaystyle{\Pi_1\atop {\q A_{1};}}{\cdots}{\Pi_n\atop {\q
A_n;}}}\quad {\atop {\displaystyle \cC}}}\over \q B}\ap
\]

\noindent We say that, for the non-trivial case,  a formula is an {\em
assumption} of a proof tree
if it is a minor premise in some leaf.  We write this as
$$\ldots H \ldots\atop\Pi$$
The {\em clauses} of a
proof tree are the ones appearing as major premises.  The root of a
proof tree is called its {\em consequence} and is denoted by $\Pi :: B$.
  A proof tree is a {\em
proof} of $B$ from a set ${\cal P}$ of clauses iff $B$ is its
consequence, its clauses belong to ${\cal P}$ and it has no
assumption.
\end{definition}

Major premises (i.e.\  clauses) will be considered modulo renaming;
equality and substitutions on proof trees are instead defined as follows.

\begin{definition}[Proof Trees Equality]
$\Pi_{1}=\Pi_{2}$ if their major
premises   occurrences are equivalent up to renaming, while the other
 formulae occurrences are identical.
\end{definition}

\begin{definition}[Proof Trees Substitution]
$\theta \Pi$ is the tree obtained by simultaneously applying a
substitution $\theta$ to the root and to all the formulae occurring as
minor premises.  The major premises are left untouched.
\end{definition}

 The class of proof trees is closed under
% substitution \wrt the rule $\ap$.
 The subsumption ordering on formulae is then lifted to
proof trees as follows.

\begin{definition}[Subsumption Ordering]
$\Pi_{1}$ is less general than $\Pi_{2}$,
written $\Pi_{1} \leq \Pi_{2}$, if there is a substitution $\sigma$
such that $\sigma \Pi_{2}= \Pi_{1}$.  We also say that $\Pi_{2}$
subsumes $\Pi_{1}$.  Moreover, we define $\Pi_{1} \equiv \Pi_{2} \Bimp
\Pi_{1} \leq \Pi_{2} \And\Pi_{2} \leq \Pi_{1}$.
\end{definition}

One can easily see that `$\equiv$' corresponds to equivalence on proof
trees up to renaming.
 \smallskip

Now we introduce the notions of similarity and most general
proof tree.  This will allow us to abstract away from many details of
\SLD-derivations.  For example, we do not need a switching lemma or a
notion of fairness; analogously we  avoid some fastidious standardizing
apart.

 In \ref{Mom94} similarity was
defined via axiom/rule-occurrences.  For the more restricted class
of proof trees considered here, we can give a more intuitive
characterization, by means of the notion of a proof-skeleton:

\begin{definition}[Skeleton]
The \emph{Skeleton} $\sk(\Pi)$ of a proof tree $\Pi$ is defined
recursively as follows:
\begin{itemize}
\item
Basis:  $\sk(A) = []$
\item
Step:
\[
\sk\left({{{{\displaystyle{\Pi_1;\dots\Pi_n;}}\quad {\cC}}\over B}{\ap}}\right)
= {{{{\displaystyle{\sk (\Pi_1);\dots \sk (\Pi_n);}}\quad
{\cC}}\over []}{\ap}}
\]
\end{itemize}
\end{definition}
That is, the skeleton of a tree is obtained by systematically
replacing the root and minor premises with \emph{holes}: the (equivalence class
of) major premises are unchanged.

\begin{definition}[Similarity]
Two proof trees $\Pi_1$, $\Pi_2$ are  said to be {\em similar},
written $\Pi_1 \sim \Pi_2$, whenever $\sk(\Pi_1)=\sk(\Pi_2)$.
\end{definition}

One can easily see that $\sim$ is an equivalence relation.  Most
general proof trees are introduced as follows.

\begin{definition}[Most General Proof Tree]
 $\Pi$ is a {\em most general proof tree} (mgpt) if it is
{\em maximal}  among similar trees.
\end{definition}

As shown in \cite{Mom94}, the system using the rule $\ap$ is
\emph{regular}, i.e.\ for any two similar proof trees there is a
similar proof tree subsuming them.  In regular systems, each
similarity class contains a mgpt, which is unique up to renaming.
Regularity is a property also of similarity classes of
continuations of $\Pi$, i.e.\ similarity
classes containing only continuations of $\Pi$,  where
the latter are thusly defined:

\begin{definition}[Continuation]
\label{cont}
Let $ B \If A_1, \dots , A_n $ be a clause $\cC$ and
\[
{\dots \; H \dots} \atop \Pi
\]
be a proof tree with an \emph{applicable} assumption $H$, \ie such that $\q
B = \q H$, for some
substitution $\q$.  The {\em one-step continuation} of $\Pi$ {\em
selecting} $H$
and {\em applying} $\cC$ w.r.t.\ $\q$ is the proof tree:
\[
\frac{ \q A_1; \cdots ;\q A_n \qquad B \If A_1, \dots , A_n }
{{\displaystyle{\dots \; \q H \dots \atop \q\Pi}}} {\ap}\]
$\Pi_{2}$ is a \emph{continuation} of $\Pi_{1}$, written $\Pi_{1}
\preceq \Pi_{2}$, if $\Pi_{2}$ can be obtained from $\Pi_{1}$ by a
sequence of one-step continuations.
\end{definition}

Note that substitutions in continuation steps do not need to be most
general unifiers.  One can easily see that:
\begin{proposition}\label{prop:CNT}
$\Pi_{1} \preceq \Pi_{2}$
{\em if and only if\/} there is a substitution $\sigma$ such that
$\sigma \Pi_{1}$ is an initial subtree of $\Pi_{2}$.
\end{proposition}

\begin{definition}[Most General Continuations]
A continuation $\Pi^*$ of $\Pi$ is {\em most general} ({\em mgc}) if,
for every other continuation $\Delta$ similar to $\Pi^*$, $\Delta \leq
\Pi^*$.  A continuation is {\em canonical} iff it is a one-step mgc.
\end{definition}

Since similarity classes of $\Pi$-continuations are regular
\cite{Mom94}, every mgc $\Pi^{*}$ of a given $\Pi$ is unique up to
renaming.  One can also see that canonical continuations are the
one-step continuations that use most general unifiers.


\begin{definition}[Height]
The \emph{height} of a proof tree, written $h(\Pi)$, is defined here as the
length of its \emph{minimum} branch.
\end{definition}



\subsection{Proof Trees and SLD-Resolution}

Proof trees have been designed to give an exact proof-theoretical
version of \SLD-resolution: for example, let us consider the program
\emph{SUM}, containing the following clauses:
\[\begin{array}{ll}
C_0:& \quad sum(X,0,X) \If \\
C_1:& \quad sum(X,s(Y),s(Z)) \If sum(X,Y,Z) \\
\end{array}\]

An \SLD-derivation for a goal $\la \leftarrow A, \q\ra$ can be seen as a
stepwise construction of a pt $\Pi::\q A$.  Figure 1
%\ref{contfig}
shows the continuations corresponding to the
\SLD-derivation:
\[
 \begin{array}{ll}
        \leftarrow sum(ss0,s0,X_0) & \q_{1}= [X/ss0,Y/0,X_{0}/s(Z)]  \\
        \leftarrow sum(ss0,0,X_1) & \q_{2}=[Z=ss0]  \\
        \If \Box &
 \end{array}
  \]
 Notice that the formulae in the current goal correspond to the assumptions
of the relative pt.
\begin{figure}
        \label{contfig}
        \centering
\[
        \If sum(ss0,s0, X_0)    %corretto da sX
        \quad \preceq \quad
        \frac{sum(ss0,0,X_1) \quad C_1}{sum(ss0,s0,sX_1)}
        \quad \preceq \quad
         {\ova {C_0}{sum(ss0,0,ss0) \quad C_1}{sum(ss0,s0, sss0)}}
\]
        \caption{Continuations of the goal $\If sum(ss0,s0,X_0)$}
\end{figure}

In this way every \SLD-derivation can be translated into a pt and
this yields the proof-theoretical equivalence between the two systems
(see \cite{Mom94}). More formally:

\begin{definition}
A \SLD-derivation is {\em incomplete} if at any point no literal is
selected and the derivation is thusly terminated.  It is {\em relaxed}
if mgu's are not necessarily used.  If idempotent mgu's are used, then
it is {\em canonical}.

Let $P$ be a definite program, $\If G$ a goal and $\If G, \If G_1,
\dots, \If G_m$ an incomplete relaxed \SLD-derivation for $P \cup \{
\If G \}$ with substitutions $\q_1, \dots,\q_m$.  Let $\q$ be the
restriction of $\q_1 \cdots \q_m $ to the variables of $G$.  We say
that the derivation has {\em %length $m$ with computed answer $\q$ and
resultant $\q G\leftarrow G_m$}.
\end{definition}
\begin{theorem}
\label{ptequiv}
Let $P$ be a definite program and $A$ an atom:
\begin{itemize}
\item[a)]
If there is an incomplete relaxed \SLD-derivation for $P \cup \{\If
A\}$ with resultant $(\delta A \leftarrow G_m)$, then there is a
partial proof $\Pi :: \delta A$ in  $L_{0}$, using only axioms
from $P$ with open assumptions $G_m$.  If the derivation is
canonical, then $\Pi :: \delta A$ is a most general continuation of
$A$.
\item[b)]
If there is a partial proof $\Pi :: \q A$ in the $L_{0}$ with
axioms from $P$ and open assumptions $G_m$, then there is an
incomplete relaxed \SLD-derivation of $P \cup \{\leftarrow A\}$ with
resultant $(\delta A \leftarrow G_m)$.  If $\Pi :: \q A$ is a most
general continuation of $A$, then the derivation is canonical.
\end{itemize} \end{theorem}
\begin{proof}

We give the proof for $G_{0}=A$. (a)  Let $ G_0, G_1,\dots, G_m$ (with
clauses $C_1,\dots,C_m$ and substitutions $\q_1,\dots,\q_m$) be a
relaxed, possibly incomplete derivation, with $ G_0 = \:\leftarrow A$.
For $0 \leq i \leq m$, let $\delta_i$ be the composition of the
$\q_1,\dots, \q_i$ and $\leftarrow A_{i_1},\dots, A_{i_{h_i}}$ be the
atoms in the goal $ G_i$; starting with $i = 0$, we associate to $
G_0,\dots, G_i$ a proof tree $\Pi_i :: \delta_i A$ with assumptions $
A_{i_1},\dots, A_{i_{h_i}}$, as follows:

{\em Step 0}.  Associate $A$ to $ G_0$.

{\em Step i+1}.  Let $\Pi :: \, \delta_i A$ be the proof tree
associated to $ G_0,\dots, G_i$ at $step\;i$ and let $ G_{i+1}$ be
obtained applying $C_{i+1}$ to the selected atom $A_{n_i}$, with {\em
unifier} $\q_{i+1}$; build the one-step continuation of $\Pi_i :: \delta_i A$
selecting $ A_{n_i}$ and applying $C_{i+1}$ w.r.t.\ $\q_{i+1}$.
If at each step in $G_{0},\ldots, G_{n}$ we apply only mgu's, the
corresponding one-step continuations are canonical and we obtain a
mgpt.

(b)   $\Pi :: \q A$ can be obtained by at least one sequence $A = \Pi_{0}
\preceq \Pi_{1} \preceq \ldots \preceq \Pi_{n}=\Pi$; the
corresponding \SLD-derivation is $G_{0},\ldots, G_{n}$, where $G_{i}$
are the assumptions of $\Pi_{i}, i = 1\ldots n$. If $\Pi :: \q A$ is a
mgpt, then the continuations must be canonical and therefore $G_{0},\ldots,
G_{n}$ is canonical.
\end{proof}



There is a natural proof-theoretic characterization
of finite failure,
% thanks to complete sets of continuations.
\begin{definition}
An assumption is \emph{failed \wrt $\cP$} iff it has no continuation
with clauses from $\cP$. An \emph{ended
tree \wrt $\cP$} is either a proof or a proof tree with a failed assumption.
\end{definition}
\begin{definition}[Failed Proof Tree]
A proof tree $\Pi$ is {\em failed\/} with respect to a program $\cP$
if there is at least one assumption of $\Pi$ such that there are no
applicable  clause in $\cP$.
\end{definition}

\begin{proposition}[Finite Failure]
\label{ff}
An atom $A$ is finitely failed if and only if there exists a $k$ such that
 every ended pt  $\Pi :: \sigma A$ has at least one failed  assumption
 of height less or equal to $k$.
\end{proposition}

\begin{proposition}[ Failure]
\label{ff}
An atom $A$ is  failed if and only if  every ended pt  is  failed.
\end{proposition}



 You can  check that this definition of finite failure
 is equivalent to the usual one in terms of \SLD-trees and
 fairness.
`Infinite' failure is non-finite failure, \ie there is a sequence of
proof trees with increasing height. An infinite pt can be seen as the
`limit' of this sequence.
\section{The General Schema}
\label{general}


\begin{itemize}
\item[a)]
We look for (weakly) admissible rules, that allow to derive
new clauses
starting from the ones of a program $\cP$.  Weak admissibility means
that the translation $\trad$ is a partial function that is defined for all
the proofs (without assumptions) and for a suitable kind of
proof trees with assumptions.
\item[b)]
These rules
are used to transform a {\em source\/} program $\cP$ into
a {\em derived\/} program $\cQ$:
\[
\cQ = \ptuno{\Pi_1}{C_1\If \Gamma_1}{r_1},\dots,\ptuno{\Pi_n}{C_n \If
\Gamma_n}{r_n}
\]
\item[c)]
Weak admissibility entails partial correctness, i.e.\  if there is a
derivation of $A$ in $\cQ$, then there is one in $\cP$.
Completeness guarantees that the success set is preserved.
To preserve the finite failure set, completeness alone is not
sufficient, but we need also the strict monotonicity of the
translation function.
\end{itemize}

Reminder. $C_{0}$ is the (initial) calculus with the \ap rule. $C_{1}$
is the supersystem with the clause introduction rules (like \ci) of
the transformation system under scrutiny.

\begin{definition} [Weak Admissibility]
For every proof $\Pi_{1}::{\cP}\vdash_{C_{1}}H$ there is a proof
$\Pi_{0}::{\cP}\vdash_{C_{0}}H$

\end{definition}

 \begin{definition}
A set of atoms is \emph{G-closed} if each atom containing a predicate
symbol occurring in $G$ is an instance of an atom in $G$.
\end{definition}

\begin{enumerate}
\item
Partial correctness coincides with the existence of a translation
function, such that if there is a
derivation of $A$ in $\cQ$, then there is one in $\cP$.
\item
 Let $\cP$ be a source program,
 \[
 \cQ = \ptuno{\Pi_1}{A_1 \If \GG_1}{\ci} ,\dots, \ptuno{\Pi_n}{A_n \If
 \GG_n}{\ci}
  \]
 be a derived program, and $G$ be a finite set of atoms.  We say that
 $\cQ$ is \emph{$G$-complete \wrt success}  iff
 \begin{itemize}
 \item[(i)]
 For every $\Pi :: {\cP} \vdash_{L_{0}} \sigma H$, that proof can be
 partitioned as follows:
 \[
 \begin{array}{ccc}
         \Pi_{1}^{'} &\ldots  & \Pi_{n}^{'}  \\
         \delta A_{1} & \ldots & \delta A_{n}  \\
          & \Pi^{'} &   \\
          & \delta A &
 \end{array}
 \]
 \item[(ii)]
  $A_i \If \GG_i$ is \emph{G-closed}
 \end{itemize}
\item
We state  the following monotonicity properties of $\trad$ \wrt continuations:

\begin{enumerate}
%       \item
%       if $\Pi_{1} \preceq \Pi_{2}$ then $\trad(\Pi_{1}) \preceq
%       \trad(\Pi_2)$
\item
% if $\Pi_{1} \preceq \Pi_{2}$ and
$h(\Pi_{1})
        < h(\Pi_2)$ then $h(\trad(\Pi_{1})) < h(\trad(\Pi_{2}))$.
\item
if $\trad$ \ is partial then for every pt with arbitrary high
continuations, there is a continuation $\Pi^{*}$ such that $\trad(\Pi^{*}$
is defined.
\end{enumerate}

\item
 Let $\cP,\cQ$ be as above. We say that
 $\cQ$ is \emph{$G$-complete \wrt infinite tress}  iff
 \begin{itemize}
 \item[$(i)^{'}$]
 There is a $k$ such that  every $\Pi :: {\cP} \vdash_{L_{0}} \sigma H$,
 with height$(\Pi) > k$ satisfies (i)
 \item[$(ii)^{'}$] = (ii)
 \end{itemize}

\end{enumerate}

To summarize: $\cQ$ may be
\begin{enumerate}
\item
sound (partially correct)
\item
$G$-complete \wrt success
\item
strictly monotonic
\item
$G$-complete \wrt  infinite pt's
\end{enumerate}
\begin{definition} For a program $\cP$ and a goal $G$, let $[G]$
define the closure under substitution induced by the language of $\cP$,
let $SS_{\cP}$ be the success set and $Infpt_{\cP}$ the set of infinite
pt's of $\cP$.
\end{definition}
\begin{theorem}
% \mbox{}
Given $\cP$ and $\cQ$ as above:
\begin{enumerate}
\item
entails $SS_{\cQ} \subseteq SS_{\cP}$
\item
entails $SS_{\cP}\cap [G] \subseteq SS_{\cQ} $
\item
entails $Infpt_{\cQ}\subseteq Infpt_{\cP}$
\item
entails $Infpt_{\cP}$ restricted to $[G]$ $\subseteq Infpt_{\cQ}$
\end{enumerate}
\end{theorem}
\begin{corollary}
\mbox{}

\begin{itemize}
\item[1.\ and 2.] entail success is preserved over $G$
\item[1.2.3.\ and 4.] entail success and finite failure is preserved over $G$
\end{itemize}
\end{corollary}

\section{Partial Deduction}
\label{pv}

\newcommand{\ttt}{ \prooftree \[ \[c_{0} \justifies e(0) \using \ap\]
\quad c_{2} \justifies o(s0) \using \ap \]
\quad c_{1}  \justifies e(ss0) \using \ap \endprooftree }
\newcommand{\tttt}{ \prooftree \[ \[ \ol{e(X)}^{0} \quad c_{2} \justifies
o(sX) \using \ap
\] \quad c_{1} \justifies e(ssX) \using \ap\] \justifies e(ssX) \If e(X) \using
\ci,0 \endprooftree }

We are now in the position of giving a more abstract view of
\emph{Partial Deduction} (PD) \cite{Kom93,Kom93b} thanks to our
framework.  Note that we will not be concerned with the pragmatics of
PD \cite{Sah91,PP94,DGT96} like unfolding rules, loop detection et
cetera: those issues can be treated as usual.

PD can be expressed via the converse of the clause application rule,
called clause introduction.  The rule discharges
 the ($u$-th occurrence of
the set of) assumption(s) $\GG$.
\[
\frac{{\displaystyle {\frac{\mbox{}}{\Gamma} {u}} \atop {{\displaystyle\Pi
\atop {\displaystyle C}} }}}{C \If \Gamma}{\ci,u}
\]

The latter allows the derivation of resultants. For instance,
from the program \textsl{EO}  in example \ref{oe}
we can derive the   resultant $\Pi_{0}::e(ssX) \If e(X)$:
\[
\tttt
\]
The usage of $\ap$ in
conjunction with $\ci$ yields a proof tree like the one in Figure 2.
% \ref{fi:res}.
 \begin{figure}
        \label{fi:res}
        \centering
        \[
 \prooftree \ttt \quad { \Pi_{0} \atop {e(ssX) \If e(X)}} \justifies
 e(ssss0) \using \ap \endprooftree
 \]
        \caption{Proof tree with the $\ci$ rule}
 \end{figure}

As one can see, only the derived clause $e(ssX) \If e(X)$ plays a role
in the derivation of the proof tree concluded by $\ap$. More in general,
let us consider a set of pt's ${\cal Q} = \{\Pi_{i}::C_i \If \GG_{i}\}$
for $i=1\ldots n$.
Provided that each $\Pi_{i}$ applies only
clauses from $\cP$, then each $C_i \If \GG_{i}$ is a \emph{resultant} for
$\cP$ \wrt $C_{i}$. If
in a proof tree that applies these derived resultants by $\ap$ we hide
their proofs, it is
apparent that we obtain a pt with clauses $C_1 \If
\GG_{1},\ldots,C_n \If \GG_n$.  That is, we may forget the tree which
has proved the resultant and we can consider $\cQ$ as a program.

Therefore we can formalize the Partial Deduction of a source program
$\cP$ with respect to a set $G$ of atoms as
the derivation of a program ${\cal Q} = \{\Pi_{i}::C_i \If \GG_{i}\}$, where
$C_{i}$ are instances of formulae of $G$ and the
proofs $\Pi_{i}$ may use $\ap$ and $\ci$ and the clauses of $\cP$.

\medskip

We now address the problem of adequacy: the first issue is the
{\em admissibility of the $\ci$ rule\/} in $L_{0}$. We define a translation
map on pt's
which eliminates occurrences of the latter rule.  This procedure is
analogous to the $\supset$-reduction step of normalization in natural
deduction calculi, yet simpler, due to the restricted syntax of
definite programs.
Recall  that $L_{1}$ is the logic consisting of $L_{0}$ plus $\ci$.

\begin{theorem}[Normalization]
For every proof tree $\Pi::\Gamma \prv_{L_{1}}  B$
with clauses from $\cal P$  there is a proof tree
$\Pi^{*}::\Gamma \prv_{L_{0}} B$, \ie without occurrences of $\ci$.
\end{theorem}
\begin{proof}
We set $\Pi^{*} = \trad(\Pi)$, where $\trad$ is the function defined
below, by induction on the derivation $\Pi$ of $B$.

\begin{itemize}
        \item $\trad(A)=A$
        \item The applied clause is the program clause $\cC$:
\[
\trad\left({{{\displaystyle{\Pi_1\atop {\q A_{1};}}{\cdots}{\Pi_n\atop
{\q A_n;}}}\quad {\atop {\displaystyle \cC}}}\over B}\ap\right) =
{{{\displaystyle{\trad(\Pi_1)\atop {\q
A_{1};}}{\cdots}{\trad(\Pi_n)\atop {\q A_n;}}}\quad {\atop
{\displaystyle \cC}}}\over B}\ap
\]
        \item The applied clause has been introduced by $\ci$:
        \[
\trad\left({\frac{{\displaystyle {\Pi_1\atop \sigma A_1;}}\cdots
{\displaystyle {\Pi_n\atop {\sigma
A_n;}}}\qquad \frac{{\displaystyle {A_{1}\ldots A_n
\atop{{\displaystyle \Pi_{0} \atop {\displaystyle B}}}}}}{\displaystyle {B \If
A_1\ldots A_n}}{\ci}} {\sigma B} {\ap}}\right)  = {\trad(\Pi_1) \ldots
\trad(\Pi_n) \atop{{\displaystyle \sigma A_1\ldots \sigma A_n}
\atop{{\displaystyle \sigma(\trad(\Pi_0))} \atop{\displaystyle \sigma
B}}}}
\]
\end{itemize}
\end{proof}

Therefore this mapping preserves assumptions and consequences while it
eliminates every occurrences of the $\ci$ rule.
Indeed, $\trad$ is essentially a normalization operator which get rid
of every vicious circle out of introductions immediately followed by an
elimination with the same major premise.


\smallskip

Admissibility ensures the partial correctness of partial evaluation with
respect to a set $G$ of atoms. To get total correctness,
we need $G$-completeness and $G$-closure.

\begin{theorem}[Partial Deduction Theorem]
\label{th:pv}
Let $\cP$ be a source program, $G$ a set of atoms  and $\cal
Q$ a derived program such that $\cQ$ is $G$-closed and $G$-complete
with respect to $\cP$.  Then, for every $\theta A \in G$
\begin{enumerate}
        \item If there is a pt in $\cal Q$ of the form $ \Pi ::
        \GG\prv_{L_{1}} \q A$ then there is a pt $ \Pi^\prime ::
\GG\prv_{L_{0}} \q A$
        from $\cP$

        \item If there is a \emph{proof} $\Pi :: \q A$ from $\cP$, then there
        is a \emph{proof} $\Pi^\prime :: \q A$ in $\cal Q$

        \item If there is a pt $\Pi :: \q A$ from $\cP$ which can be
indefinitely
        continuated, then the same holds for $\cal Q$

        \item $A$ has a $A$-complete finitely failed set from $\cP$ iff
        the same holds for $\cal Q$.
\end{enumerate}
\end{theorem}
\begin{proof}
\mbox{}

\begin{enumerate}
        \item Trivial: set $\Pi^\prime = \trad(P)$

        \item Let us consider a pt $\Pi$ with rules from $\cP$, no
        assumption and conclusion $\sigma A$ for $A \in G$.  By
        $G$-completeness
        there is an $i$ such that $\trad(\Pi_{i}) \preceq \Pi$ \ie
        \[
        \Pi = {\Pi_1 \ldots \Pi_n \atop{{\displaystyle \sigma A_1\ldots
        \sigma A_n} \atop{{\displaystyle \sigma(\trad(\Pi_i))}
        \atop{\displaystyle \sigma A}}}}
        \]

Now we build the hybrid pt, for $n > 0$,
\[
\frac{ {\Pi_1\atop \sigma A_1;}\cdots {\Pi_n\atop \sigma A_n;}\qquad
{\frac{\Pi_i^*}{C \If A_1\ldots A_n}} } {\sigma C}
\]
By $G$-closure each  $\sigma A_{i}$ with predicates in $G$
is an instance of some atom in $G$ and
we can iterate the same procedure to
every $\Pi_{i}$.  This process terminates
since at each step the height of the current set
$\Pi_{1},\ldots,\Pi_{n}$ decreases.

        \item Proceed as is the previous case, with the following
        difference: once you get to the hybrid tree, recall that since
        $\Pi_{i}^{*}$ can be continued ad libitum, so are
        $\Pi_{1},\ldots,\Pi_{n}$.  This means that this procedure may be
        indefinitely iterated, continuing thusly a pt in $\cal Q$ to an
        arbitrary height.

        \item
        \begin{itemize}
                \item[($\If$)] Suppose $A$ has an $A$-complete finitely failed
                set of mgc's in $\cal Q$ of the form $\Pi_{1},\ldots,\Pi_{n}$.
                Consider its normalization: each $\trad(\Pi_{i})$ has a
                complete and failed set of mgc's.  To show this, suppose the
                converse: then there would be a continuation of
                $\trad(\Pi_{i})$ which is either a proof or can be continued
                ad libitum.  But this is impossible due to points 2 and 3.
                Substituting $\trad(\Pi_{i})$ with the correspondent complete
                and failed sets of mgc's yields the $A$-complete and failed
                set of continuations with clauses in $\cP$.

                \item[($\Imp$)] A has a $A$-complete finitely failed set of
                mgc's from $\cP$.  Assuming the negation of the thesis, we
                would have the following subcases:
                \begin{itemize}
                        \item there is a proof $\Pi :: \sigma A$ from
$\cP$.  But
                        thus $\trad(\Pi) :: \sigma A$ would be a proof of
$\sigma
                        A$, continuation of some pt from $\cP$.

                        \item There is $\Pi :: \sigma A$ with arbitrary high
                        continuations.  But for the monotonicity of $\trad$
\wrt
                        $h$ there would be a proof $\Pi^*$ with arbitrary high
                        continuations.
                \end{itemize}
        \end{itemize}
\end{enumerate}
\end{proof}

The first item corresponds to partial correctness and coincides with
admissibility. The second one ensures that the success set is
preserved, and it follows from $G$-completeness and $G$-closure.
The third and fourth ones ensure that the finite failure set is
preserved.  We obtain:

\begin{corollary}
Let $\cQ$ be derived by PD from a source program $\cP$. If $\cQ$ is
complete and $G$-closed, then it has the same success and finite
failure sets of $\cP$.
\end{corollary}


\section{Program Transformation}
\label{pt}
In this section  we give a proof theoretical analysis of some other
transformation techniques. We use the general
method presented in the introduction and shown
for partial deduction.
Let us now turn to analyzing unfolding and folding \cite{PP94,Se91,
She92,TS84}.

\subsection{Unfolding}

Unfolding needs the admissible rule $\ci$, for which we have already
given the translation function $\trad$. A transformation of a program $\cP$
corresponds to the derivation of a new program:
\[
\cQ =
% \left\{
\ptuno{\upt{\GG_{1}}{\Pi_{1}}{C_{1}}}
                      {C_{1}\If\GG_{1}}
                      {\ci}
                      ,\dots,
\ptuno{\upt{\GG_{n}}{\Pi_{n}}{C_{n}}}
                      {C_{n}\If\GG_{n}}
                      {\ci}
%                       \right\}
\]

The admissibility of $\ci$ has been already shown. The
completeness condition for unfolding is:

\begin{definition}[Unfold-Completeness]\label{def:UCS}
The derived program $\cQ$ is \emph{unfold-complete with respect to $\cP$ }
if the set of proofs $\trad(\Pi_{1}),\dots,\trad(\Pi_{n})$ is
$\cP$-complete (see Definition \ref{def:ACS}).
\end{definition}

Since $\trad$ is strictly monotone, the completeness of $\cQ$ allows
to prove that the success and finite failure sets
are preserved. The proof is identical to the one of Theorem \ref{th:pv} of
the previous section and therefore it is omitted.

\begin{example}
Referring back to the program \textsl{EO} of Example \ref{oe} the
unfolded program $\cQ$ (which brings back the usual and more
efficient definition of \texttt{even} and \texttt{odd})  is
unfold-complete:
\[
\cQ = \left\{
% \begin{prooftree}
% \[c_{0} \justifies e(0)\] \justifies e(0) \If
% \end{prooftree}
{\ova {c_{0}}{e(0)}{ e(0) \If}}
\quad\quad
{\ova{\ol{e(X)} \quad c_{2}}{ o(sX)\quad c_{1}}{\ptuno {e(ssX)}
{{\displaystyle e(ssX)
\If e(X)} }{}}}
\quad\quad
{\ova{c_{0}}{e0\quad c_{1}}{\ptuno{o(s0)}{{\displaystyle o(s0) \If}}{}}}
\quad\quad
{\ova{\ol{o(X)} \quad c_{2}}{ e(sX)\quad c_{1}}{
\ptuno{o(ssX)}{{\displaystyle o(ssX)\If o(X)}}{}}}
\right\}
\]
\end{example}
Usually \cite{TS84,PP94}, an unfolding transformation is seen as a
sequence of programs, obtained thru a sequence of single unfolding
steps, where each step preserves completeness.  Thus one obtains a
final program that preserves success and finite failure.  In our case
we can define completeness directly on the final derived program
$\cQ$, since it explicitly contains the proofs of its clauses,
starting from the ones of the source program.

\subsection{Folding}

The folding rule refers to a folding set
\[
\cF = \left\{
{\upt{\sigma_{1}\cB_{1}}
       {\Pi_{1}}
       {\sigma_{1} A}}
, \dots,
{\upt{\sigma_{k}\cB_{k}}{\Pi_{k}}{\sigma_{k}A}}
\right\}
\]
of proof trees with clauses from $\cP$, such that $\cF$ is
 $A$-complete\footnote{This requirement may be relaxed.}.

\smallskip

For such a $\cF$, we have the following rules:
\[
\ptn{H \If \GG,\sigma_1 \cB_1}
    {H \If \GG,\sigma_n \cB_n}
    {}
    {H \If \GG,A}
    {\fold(\cF)}
\]

\[
\ptn{\sigma_1(H \If \GG, \cB_1)}
    {\sigma_n(H \If \GG,\cB_n)}
    {}
    {H \If \GG,A}
    {\foldo(\cF)}
\]
In $\fold$ the condition $dom(\sigma) \cap vars(\Gamma,H) = \emptyset$
must be satisfied.  $\fold$ allows to treat, for example,
Tamaki\&Sato's \cite{TS84} and Shepherdson's \cite{She92} folding.
The rule
$\foldo$ does not have restrictions on $\sigma$.  It allows to treat
general folding \cite{PP94} (R2, p.\ 268).  Indeed, $\foldo$ is more
general than $\fold$.  We distinguish the two rules because they have
different logical explanations, as briefly remarked in the
conclusions.

\begin{example}
Given the following program \texttt{minmax} to determine the minimum and
maximum of a list, where the definition of \texttt{sup} and \texttt{inf}
are left open:
\[
\begin{array}{llll}
        m_{0}: & min([X],X) & \If &   \\
        m_{1}: & min([X|XS],Y) & \If & min(XS,Z),inf(X,Y,Z). \\
           m_{2}: & max([X],X) & \If &   \\
        m_{3}: & max([X|XS],Y) & \If & max(XS,Z),sup(X,Y,Z)). \\
        m_{4}: & minmax(XS,Min,Max) & \If & min(XS,Min),max(XS,Max).
 \end{array}
 \]
and this folding set:
\[
\cF = \left\{\frac{min(XS,Min)\quad max(XS,Max) \quad
m_{4}}{minmax(XS,Min,Max)}{\ap}\right\}
\]

The two following trees sum up the transformation process in an very compact
way, where each transformation step corresponds and is justified by an
inference in
the tree.

 \[
 \ova
{{\ptuno{ m_{0}}{min([X],X)}{}}
\quad
 {\ptuno{ m_{2}}{max([X],X)}{}}
 \quad {\mbox{} \atop {m_{3}}}}
{minmax([X],X,X)}
{minmax([X],X,X) \If }
\]

\[
 \ova{
{\ptuno{\ol{min(XS,Y)} \quad \ol{inf(X,Y,Min})}{min([X|XS],Min)}{}}
\quad
 {\ptuno{ \ol{max(XS,Z)} \quad \ol{sup(X,Z,Mmax)}}{max([X|XS],Max)}{}}
 \quad {\mbox{} \atop {m_{3}}}}
{minmax([X|XS],Min,Man)}
{\ptuno{minmax([X|XS],Min,Man) \If min(XS,Y),inf(X,Y,Min),max(XS,Z),
sup(X,Z,Max)}
{{\displaystyle minmax([X|XS],Min,Man) \If minmax(XS,Y,Z),inf(X,Y,Min),
sup(X,Z,Max)}}{fold(\cF)}}
\]
We thus obtain by folding the new recursive definition of \texttt{minmax}

\[
\begin{array}{llll}
        m_{5}: & minmax([X],X,X) &\If &   \\
        m_{6}: & minmax([X|XS],Min,Man)&  \If
         & minmax(XS,Y,Z),inf(X,Y,Min),
sup(X,Z,Max)
 \end{array}
 \]

\end{example}
\smallskip

Let $L_{2}$ be the logic $L_{1}$ plus the
folding rules.  Only weak admissibility holds, i.e.\ every
$L_{2}$-proof $\Pi$ using a given set of source clauses can be translated
into a
$L_{0}$-proof $\trad(\Pi)$ using the
same source clauses;  yet, translatability is not guaranteed for proof trees
with assumptions.

\smallskip

The partial function $\trad$ is recursively defined as follows:
\begin{itemize}
\item
The base  and the recursive cases for
source clauses and clauses introduced by $\ci$ are as in
Section \ref{pv}.
\item
If the applied clause is introduced by $fold$,
we have the following recursion, where $\Pi^{*},\Pi^{' *}$ are
sequences of pt's:
\[
\trad\left(
\pttre
    {\upt{}{\Pi^{*}}{\delta\GG}}
    {\upt{}{\Pi_{0}}{\delta A}}
    {\ptuno{\left\{{\upt{}{\Delta_{i}}{H \If \GG,\sigma_i
    \cB_i}}\right\}}
               {H \If \GG,A}
               {fold(\cF)}}
    {\delta H }
    {\ap}
 \right) =
\trad\left(
 \pttre
    {\upt{}{\Pi^{*}}{\delta'\GG}}
    {\upt{}{\Pi^{' *}}{\delta' \sigma_{h} \cB_{h}}}
    {{\upt{}{\Delta_{h}}{H \If \GG,\sigma_h \cB_h}}}
    {\delta' H }
    {\ap}
    \right) \]
provided that $\trad(\Pi_{0})$ is a continuation of a proof $\Pi_{h}\in \cF$.
 Since the latter
 has consequence $\sigma_{h} A$ and assumptions $\sigma_{h} \cB_{h}$,
 $\trad(\Pi_{0})$ has the form of an initial subproof $\delta' \Pi_{h}$,
 continued at the top by a sequence of subproofs
 $\Pi^{' *}::\delta' \sigma_{h} \cB_{h}$. The existence of the latter
 sequence allows to use it in the
 translation step.
 If $\trad(\Pi_{0})$ is not sufficiently high
 to be a continuation of any proof tree of
 $\cF$, we cannot find the sequence $\Pi^{*}_{0}$,
 and we halt the translation with an undefined result.
\item
If the applied clause is introduced by $\foldo$, the translation is
defined in a way similar to $\fold$ (omitted here for conciseness).
\end{itemize}

\begin{proposition}[Partial Correctness]
If $\Pi$ is a proof,
then $\trad(\Pi)$ successfully halts, i.e. every proof using clauses
derived in $L_{2}$ can be translated into a proof using only $L_{0}$
and clauses from $\cP$.
\end{proposition}
The proof easily follows from the fact that,
in every translation step related to the fold rules, $\trad(\Pi_{0})$ is a
proof of $\delta A$ and hence a continuation of some proof of the
$A$-complete set $\cF$.
For total correctness we need the adequate notion of completeness
with respect to $\cP$.

\begin{definition}[Fold-Completeness]
Let $\cP$ be a source program and $\cQ = \{\Pi_{j}::C_{j} \If
\GG_{j}\}_{j\in J}$ be a program derived from $\cP$ in $L_{2}$. We say that
$\cQ$ is \emph{fold-complete} with respect to $\cP$ if  every proof
tree
\[
\ptdue{\mbox{} \atop \GG}
           {\upt{}{\Pi_{j}}{C_{j} \If \GG_{j}}}
           {C_{J}}
           {\ap}
\]
has continuations that can be successfully translated and the set of all
the translations
is $\cP$-complete.
\end{definition}
% ptdue
\begin{theorem}[Total Correctness]
If $\cQ$ is fold-complete with respect to $\cP$, then for every $L_{0}$-proof
$\Pi::H$ with clauses from $\cP$ there is a $L_{2}$-proof
$\Pi^{*}::H$ with  clauses from $\cQ$.
\end{theorem}

The proof, omitted, is similar, yet more complex, to the one of Theorem
\ref{th:pv}.

\smallskip

By the last theorem, completeness with respect to $\cP$ guarantees
that the success set is preserved.
Note that there are cases of folding that are incomplete. Appealing
to that, we can explain the well-known problems related to  self-folding.
Consider the source program $\cP$
\[
\begin{array}{lll}
p \If  r \\
r  \If
\end{array}
\]
A $p$-complete $\cF$ is
\[
{\cF} = \left\{ \ptdue{r}{p \If r}{p}{\ap}\right\}
\]
and the transformed program is
\[
\cQ = \left\{
\begin{array}{lll}
{\displaystyle \frac{p \If r}{p \If p }{\mbox{\small fold(\cF)}}}   \\
        \mbox{} \\
         r  \If
\end{array}\right\}
\]
$\cQ$ is incomplete since  for every continuation in $\cQ$ of
the proof tree below, say $\Pi_{self}$
\[
\ptdue {\mbox{} \atop p} %
      {\ptuno{p \If r}{p \If p}{\mbox{\small fold(\cF)}}}
      { {\displaystyle p}}
      {\ap}
\]
the translation fails. On the other hand, the program $\cQ_{1}$
\[
\cQ_{1}=\left\{
\begin{array}{lll}
 {\displaystyle \frac{p \If r}{p \If p }{\mbox{\small fold(\cF)}} }   \\
                \mbox{} \\
        p  \If  r  \\
        r   \If
\end{array} \right\}
\]
is complete. Indeed the continuation
\[
\ptdue{\ptdue{r}{p \If r}{p}{\ap}}
      {\ptuno{p \If r}{p \If p}{\mbox{\small fold(\cF)}}}
      {p}
      {\ap}
\]
is translated into this $\Pi_{trad}$
\[
\ptdue{r}{p \If r}{p}{\ap}
\]
Finally one can prove that:

\begin{theorem}
If $\cQ$ is fold-compete and $\trad$ is strictly monotone, then finite
failure is preserved.
\end{theorem}

For example, in $\cQ_{1}$ $\trad$ is not strictly monotonic. Indeed
every translatable continuation of $\Pi_{self}$ is translated in the
same proof tree $\Pi_{trad}$. Therefore finite
failure is not preserved, while success is.

\section{Conclusions and Perspectives}
We have given a proof-theoretic analysis of some well known
transformation rules.
In particular, the benefits of a proof-theoretic analysis of Partial
Deduction are
twofold:
\begin{itemize}
        \item first, once the general proof-theoretic machinery is
        digested, the adequacy proof is much simpler and direct than the
        one based on resolution, e.g.\ \cite{Llo91}

        \item second, this framework nicely generalizes to other \lp
        languages: in fact it is possible to give general uniform Partial
        Deduction mechanism for \lp languages that can be formulated as
        \emph{Axiom Application Systems} \cite{Mom94,Mom97}, say for normal
        or disjunctive programs.
\end{itemize}

More in general, our analysis shows that one can use a very general schema,
based on
the notions of admissibility, completeness with respect to the source
program and properties of the translation function, like strict
monotonicity.

\smallskip
This paper presents  work in progress. A further main step is
the study of a set of basic logical inference rules and non-logical
principles, that allow to derive all the admissible rules
corresponding to the kind of transformations known in the literature.
In other words, we are looking for a calculus to infer
program transformation rules. In this way we achieve two main
advantages:
\begin{itemize}
\item
We can study and classify the rules from a logical point of view.
For example, one can prove that the two folding rules
have different logical justifications. In fact, $\fold$ can be
derived from the completion of $\cP$, by
using only the logical rules. To derive
$\foldo$, we need also
an $\omega$-rule, as the one given in \cite{SH94} in the
context of Partial Inductive Definitions. Moreover derivations can be
embedded in the context of a specific theory, for example in the
axiomatization of a data type. In this way transformations
 can be guided by the knowledge of a specific problem domain.
 \item
 Using a set of basic rules, we can, in principle, derive new
 transformation rules. Of course, their usefulness is a question of
 experimental work.
 \end{itemize}


 A final point that we want to exploit is the use of proof-schemas.
 For example, one could try to detect regularities in a schema: this
information could suggest the definition of suitable new eureka predicates,
to be used in transformation.
Up to now we have done only some experiments in this direction, using
the examples like the Fibonacci numbers, or  the `average' program
considered in \cite{PP94}.


\textbf{Acknowledgments}. We'd like to thanks Frank Pfenning and one anonymous
referee for having carefully read and suggested useful modifications to
the previous version of the paper.

\begin{thebibliography}{999}

\bibitem  {Ap90} K.A. Apt. Logic Programming. {\em Handbook
of Theoretical Computer Science},  Leuween J. (ed.), Elsevier, 1990.

\bibitem{DGT96} O. Danvy, R. Gluck, \& P. Thiemann. \emph{Partial Evaluation}.
International Seminar, Dagstuhl Castle, Germany, February 12-16:
Selected Papers, LNCS 1110, Springer, 1996 .

\bibitem  {Hal90} L. Halln\"as  \& P. Schroeder-Heister.   A
Proof-Theoretic Approach to Logic Programming: Clauses as Rules. {\em
Journal of Logic and Computation},  v.1 no. 2. pp. 261\--283, 1990.

\bibitem{Hod93}
W.~Hodges.
Logical features of Horn clauses.
In D.M.~Gabbay, C.J.~Hogger, and J.A.~Robinson, editors,
{\em Handbook of Logic in Artificial Intelligence and Logic Programming\/},
{\em Volume 1: Logical Foundations}, pages 449-503,
Oxford University Press, 1993.

\bibitem{Kom93} J. Komorowski. A Prolegomenon to Partial Deduction
{\em Fundamenta Informaticae: Annales Societatis Mathematicae
polonae}, V. 18, pp. 41--63, 1993.

\bibitem{Kom93b} J. Komorowski. Special Issue on   Partial
Deduction. In \emph{Journal of Logic Programming}, Guest Editor,
1993.

\bibitem {Jo96} N. D. Jones. An Introduction to Partial Evaluation. {\em
Acm Computing Surveys},  Volume 28, 3, pp. 480--531, 1996

\bibitem {Llo91}  Lloyd J.W.  \& Shepherdson J. Partial Evaluation In
Logic Programming, {\em Journal of Logic Programming}, v.11, pp.
217\--242, 1991.

\bibitem  {Mom94} A. Momigliano \& M. Ornaghi.  Regular Search
Spaces as a Foundation of Logic Programming. In: {\em Extensions of
Logic Programming},  Dyckhoff R. (ed.), LNAI n. 798, Springer Verlag,
1994.

\bibitem  {Mom97} A. Momigliano \& M. Ornaghi. Regular Search Spaces
and  Constructive Negation. {\em Journal of Logic and Computation},
to appear.

\bibitem{PP94} A. Pettorossi \& M. Proietti. Transformation of Logic
Programs: Foundation and Technique. \emph{Journal of Logic Programming},
pp. 261--321, vol. 19--20, 1994.

\bibitem{Pra65} D. Prawitz. \emph{Natural Deduction. A Proof-Theoretical
Study}. Almquist \& Wiksell, Stockholm, 1965.

\bibitem {Sah91} D. Sahlin. \emph{An Automatic Partial Evaluator for Full
Prolog}. Report, TRITA-TCS--9101, 1991.

\bibitem {SH94} P. Schroeder-Heister. Rules of Definitional Reflection.
In: {\em Proceedings of the IEEE Symposium on Logic in Computer Science},
pp. 222--232, 1993.

% \bibitem {SH94} P. Schroeder-Heister. Definitional Reflection and the
% Completion. In: {\em Extensions of Logic Programming},  Dyckhoff R.
% (ed.), pp. 333--347, LNAI no. 425, Springler Verlag, 1994.

\bibitem {Se91} H. Seki.  Unfold/Fold Transformation of Stratified Programs.
{\em TCS}, 86:107--139, 1991.

\bibitem {She92} J.C. Sheperdson. Unfold/Fold Transformations of Logic
Programs.
{\em Math. Structure Comp. Science}, 2:143--157, 1992.

\bibitem{TS84} H Tamaki \&  T. Sato. Unfold/Fold Transformation of Logic
Programs. In: {\em Proc. of ICLP84}, S-A T\"{a}rlund (Ed.),
Uppsala,pp.127--138, 1984.

\end{thebibliography}
\appendix
\section{Appendix}

\begin{definition}[A-Complete Sets] \label{def:ACS}
Let ${\cal S} = \Pi_{1},\dots, \Pi_{n}$ be a set of continuations of
$A$:  ${\cal S}$ is \emph{$A$-complete \wrt $\cP$} if there is a
constant  $h_{max}$  such that:
\begin{itemize}
\item[a)]
every proof $\Pi::\sigma A$  from $\cP$ is a continuation of at least one pt of
${\cal S}$
\item[b)]
every proof tree $\Pi::\sigma A$ with axioms from $\cP$ of height greater
than $h_{max}$ is a
continuation of at least one pt of ${\cal S}$.
\end{itemize}
\end{definition}

 \begin{example}
\label{oe}
Let us consider the program \textsl{EO}:
\[
\begin{array}{llcc}
        c_{0}: & e(0) & \If &   \\
        c_{1}: & e(s(X)) & \If & o(X) \\
        c_{2}: & o(s(X)) & \If & e(X)
\end{array}
\]
Now the following set of proof trees is $e(X)$-complete with
$h_{max}=2$.
\[
 \frac {c_{0}} { e(0)}{\ap}
 \quad\quad\quad
\Pi_{2}=
  \begin{prooftree}
  \[
e(X) \quad c_{2}
  \justifies
 o(sX)\quad c_{1}
 \using
  \ap
 \]
  \justifies
  e(ssX)
  \using \ap
  \end{prooftree}
\]
Indeed every proof of $e(s^{n}0)$ is a continuation of $\Pi_{2}$ and
 similarly for proof trees with (open) assumptions and height greater
 than 2.
   \end{example}

This notion of $A$-completeness for sets of continuations easily
generalizes to \emph{G-Completeness} (w.r.t.\ $\cP$), for $A\in G$,
and \emph{Completeness} (w.r.t.\ $\cP$) tout court, that we call
$\cP$-\emph{Completeness}.

\begin{example}[Continued]
 Now adding the following set of proof trees to those above
 we obtain a set \textsl{EO}-complete with
$h_{max}=2$.
 \[
% {\ova{c_{0}}{e0\quad c_{1}}{o(s0)}}
\begin{prooftree}
  \[
c_{0}
  \justifies
e0\quad c_{1}
 \using
  \ap
 \]
  \justifies
 o(s0)
  \using \ap
  \end{prooftree}
 \quad\quad\quad
 \begin{prooftree}
  \[
o(X) \quad c_{2}
  \justifies
e(sX)\quad c_{1}
 \using
  \ap
 \]
  \justifies
o(ssX)
  \using \ap
  \end{prooftree}
% {\ova{o(X) \quad c_{2}}{ e(sX)\quad c_{1}}{ o(ssX)}}
\]
 \end{example}
In the following we will often refer to
$\cP$-\emph{Completeness} simply as Completeness.  This
should not cause confusion with other common uses of the word.



Consider the proof of  $\If sum(ss0,s0,X_0)$:
$$ {\ova {C_0}{sum(ss0,0,ss0) \quad C_1}{sum(ss0,s0, sss0)}}$$

The most general pt in this similarity class is
\[
{\ova {C_0}{sum(X,0,X); \quad C_1}{sum(X,s0, sX)}}
\]

There is a systematic way to obtain the mgpt of a similarity class
 by an opportune
`instantiation', denoted by $ \sk(\Pi)(A)$,  of the skeleton of a member
 of the latter. This is achieved by the operator $S(A)$.

\begin{definition}[The Operator $S(\Pi,A)$]
 Let $sk(\Pi) = S$ be the skeleton of a proof tree.  $\Pi^{*} :: \q A =
 S(\Pi,A)$
 if and only if $\Pi^{*}$ is a mgc of $A$ with skeleton $S$.In other terms
 $ S(\Pi,A)$ is the mgpt of the si;ilarity class $\{ \Pi^{'} \mid
 \Pi^{'} = sk(\Pi)(\q A)\}$
\end{definition}

 We now address the question of how to convert pt's which are mgc's of
 $A$ from $\cal Q$ in their normalization from $\cP$.  Consider:
 \beq
 \sk(\Pi)(A) = {\Pi \atop \sigma A} & & \sk(\trad(\Pi))(A) = {\Pi^\prime
 \atop \delta A}
 \eneq

 \begin{theorem}
 $(\sk(\Pi)(A)) = \sk(\trad(\Pi))(A)$
 \end{theorem}

 Let $\trad_{S}$ be a map from skeletons with clauses from $\cal Q$ into
 skeletons with clauses from $\cP$: consider $\trad(S(A))$; it has
 skeleton $\sk(\trad(S(A)))$ independently from $A$.  Hence we put
 \[
  \trad_{S}(S)=_{def}\sk(\trad(S(A)))
  \]
  Note the following: \beq \sk(\Pi::A)(A) &=& \Pi::A\\
        \trad_{S}(S)(A)&=&\trad(S(A)) \eneq Hence

  \beq \trad(\sk(\Pi)(A))&=&\trad_{S} (\sk(\Pi))(A) \eneq
  If we prove
  \beq
  \sk(\trad(\Pi))(A)&=&\trad_{S} (\sk(\Pi))(A)
  \eneq
  the theorem is proven since the following diagram would commute:
    diagramma di commutazione
  \[
  \begin{array}{llll}
        \cal P_{\cal Q} & \stackrel{\trad}{\longrightarrow} & {\cal P}_{P} \\
        \stackrel{\sk}{\downarrow} & \equiv & \stackrel{\sk}{\downarrow} \\
        S_{\cal Q} & \stackrel{\trad_{S}}{\longrightarrow} & S_{P}
  \end{array}
  \]

  \begin{lemma}[Commutativity]
  \label{le:commu}
  $\sk(\trad(\Pi))(A) = \trad_{S} (\sk(\Pi))(A)$.
  \end{lemma}





