\documentstyle{article}
\begin{document}
\include{tcom}
\section{Intro}

We aim to give a proof-theoretic analysis of transformations of logic 
programs, essentially vied as operations on proof trees in the sense 
of \cite{Mom97}. Our framework is natural deduction: (complete)
programs are seen as {\em rules} in the above sense. We are not 
interested here in detailing the logic we are using, though we have 
shown elsewhere \cite{??} that interpreting $:-$ and $,$ as 
implication and conjunction yields positive intuitionistic logic.

Note that the normalization theorem holds for our systems and we will 
use this fact tacitly: in fact the theorem follows from the fact
that programs (and equality axioms) are Post systems in the sense
of Prawitz\footnote{A totally analogous presentation can be given in 
terms of sequent calculus with definitional reflection \cite{SH93} 
where the author proves cut-elimination for equality rules and for 
the $\omega$-version of reflection applied to Horn programs}.
\section{Rules}


We consider {\em complete} programs.
%\begin{Def}
Let p be a $n$-ary relation symbol; we assume that it is defined by 
$n$ clauses whose head has the form $p(\dots)$ and the $i$-th clause 
has $n_i$ literals in its body, i.e.\ has the form
\beq
p(t_{i,1}\dots t_{i,n_i}) \leftarrow L_{i,1}\dots L_{i,n_i}
\eneq
 Then for all $i$ we have the rule:
\[
\frac{\q L_{i,1}\dots \q L_{i,n_i}}
	{\q p(t_{i,1}\dots t_{i,n_i})}{I_p}
\]
That we call the {\em introduction} rule for $p$.

The {\em elimination} rule for $p$ is instead given a predicate 
definition $p(\dots)$ \cite{Cla78}:by the only-if part of the 
completion, \ie the single axiom:
\beq
\forall \overline{x} (p(\overline{x}) \Imp \bigvee\limits^n_{i=1}
\exists \overline{y} (\overline{x}=\overline{t_i} \And
\bigwedge\limits^{n_i}_{k=1} L_{i,k}))\\
\eneq
where $\overline{x}$ is an array of $n$
of new variables, whereas $\overline{y_i}$ are those appearing in the 
$i$-th clause. This yields the rule
\[
\frac{p(a) \quad\quad\quad {\displaystyle{\dots [\sigma_{1} L_{i_1}}] 
\dots \atop {\vdots \atop {\displaystyle C}}}
\quad\quad{\displaystyle{\dots [\sigma_{k} L_{i_k}] \dots \atop  
{\vdots \atop {\displaystyle C}}}}}{C}{E_p}
\]
\noindent
where $a, t_1,\dots,t_n$ are terms,  and  for $1 \leq h \leq k$,  
$\sigma_{h}=mgu(t_{i_h}, a)$.  Moreover,
if $\sigma_h L_{i_h}$ contains, modulo renaming, some of the 
existentially quantified $y$, those variables must be {\em new} 
(w.r.t.\ $a$) eigenvariables. The literals between square brackets
are intended to be {\em discharged} at the conclusion of the rule.



\begin{Example} Consider the usual program for membership in lists:

MISSING *****

\[\begin{array} {l} 
member(X,X.XS). \\
member(X,Y.YS) \leftarrow member(X,YS). \\ 
\end{array} \]


Its completion is
\beq
\forall z, zs ( member(z,zs) &\Bimp &\exists x,y,xs,ys, (zs = x.xs 
\And x = z) \Or  \mbox{} \\
& & (zs = y.ys \And y = z \And member(x,ys)))
\eneq
\end{Example}

 
We note the following important properties:
\begin{enumerate}
\item
$E_p$ is the inverse of $I_p$ in the same sense of Prawitz`s 
normalization procedure for logical operators where an introduction 
followed by an elimination is cut off (reduced): in symbols that 
could be made more precise\footnote{Compare the considerations on the 
cut-property of first-order reflection in \cite{SH93}}:
\[
E_p(I_p(\Pi)) = \Pi
\]
\item  as far as uHorn axioms are concerned, the $E_p$ rule is {\em 
admissible}. This corresponds to the known fact that the only-if part 
of the completion is independent from positive 
facts\footnote{ELABORATE}
\end{enumerate}

\begin{Examplen}
Consider the following simple program and imagine the relative rules:
\beq
a &\Ift & b,c.\\
b &\Ift & e.\\
b &\Ift & f
\eneq

The following configuration reduces to $I_a$:
\beq
\frac{b\quad\quad\quad{\ova{[e]}{b\quad c}{a}}
		   \quad\quad{\ova{[f]}{b\quad c}{a}}}
{a}{E_b}
& \longrightarrow &
\frac{b\quad c}{a}{I_a}
\eneq
\end{Examplen}

For future usage we consider the following formulation of  $CET$, 
{\em 
Clark's equational 
theory}, (\cite{Cla78,Kun87}), that is the equality axioms including 
congruence (Cng), plus the axioms for finite trees

for all operators in a signature $\Sigma$, $Dec$ enforces 
injectivity, $Clh$ maintains that (the interpretation of) different 
symbols for function yields different values. $Ock$ should remind of 
the occur check in the actual unification algorithm. Indeed this 
theory is the axiomatic and proof-theoretic rendering of the latter 
algorithm, so that Clark's Lemma  is referred to as the Unification 
Lemma.
We assume the notational conventions introduced earlier.
\begin{Def}
\[
\begin{array}{llr}
(Ref): & \forall(x=x)\\
(Sym): & \forall(x=y \Imp y=x)\\
(Trn): & \forall(x=y \And y =z \Imp x=z)\\
(Cng): & \forall(\ol{\xn  = \ol{y_n}} \Imp f(\xn) = f(\ol{y_n}))
 & \mbox {for   all }   f \in \Sigma\\
(Dec): & \forall(f(\xn) = f(\ol{y_n}) \Imp \ol{\xn = \ol{y_n}}) & 
\mbox{for all }   f \in \Sigma\\
(Clh): & \forall(f(\xn) \nq g(\ym)) & \mbox{for distinct }  f,g \in 
\Sigma 
%\ \mbox{ of the same target type}
\\
(Ock): & \forall(x \nq t[x]) & \mbox{if $x$  occurs  properly  in}  \
t[x]
\end{array}
 \]
\end{Def}

Note that these axioms can also be seen as Post  systems and 
therefore preserve normalization. 
Additionally, it is convenient, when considering program 
transformation, to assume a universal language with infinite 
signature which all programs symbols are drawn from. This has also 
the advantage not to need the 

\beq
(DCA): & \forall x(\bigvee\limits_{f \in \Sigma}
\exists \vy (x=f(\vy))) 
\eneq
for completeness \cite{Mah88} which could be problematic for 
normalization.

\section{Partial Evaluation}

We now give a more abstract view of PE thanks to our framework. 
Note that we will not be concerned with the pragmatics of PE like the 
unfolding rule used the deletion of clauses depending on those  
evaluated or how to get a finite search-tree: those issues can be 
treated as usual.

First we recall some definitions. We use clauses as linear notation 
for rules


\begin{definition}[Continuation]
\label{cont}
Let $ \forall(A_1 \And \dots \And A_n \Imp B)$ be a rule
corresponding 
to a clause $C$ and 
\[
{\dots \; H  \dots} \atop \Pi
\]
be a proof-tree with an assumption $H$ s.t.~$\q B = \q H$, for some 
substitution $\q$. The  {\em continuation} of $\Pi$ {\em selecting} $ 
H$  
and {\em applying} $C$ w.r.t.\ $\q$ is the proof-tree:
\[
\frac{ \q A_1; \cdots ;\q A_n 
%\quad Ax(C)
}{{\displaystyle{\dots \; \q 
H  \dots \atop \q\Pi}}} \]
\end{definition}



**** Def of similar ???


\begin{definition}
A continuation $\Pi^*$ of a proof-tree $\Pi$ is a {\em most general 
continuation} ({\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}


PE can be equivalently described as the result of $n$-th unfold and 
fold operation or as a `pruning` of the search tree. The latter is 
more 
adequate: intuitively, given a goal $A=p(\tn)$ for a predicate 
definition, we take  the set of its mcg. We contract every tree, \ie 
we collapse a pt $\q\Pi :: \q A$ with assumptions $\q \Gamma$ to a 
$I_p$ rule $\frac{\q\Gamma}{\q A}$. Then, if $P^*$ is the result
of replacing the rules describing the predicate $p$ with the new 
definitions then the success and failure set is preserved, provided a 
closure condition is fulfilled:
\beq
SS_P = SS_P^* & and & FF_P = FF_P^*
\eneq


Usual definition

Def. 2.4 Let $P$ be a normal program, $A$ an atom and T an SLDNF-tree 
for $P\cup\{A\}$. Let $G_1\dots G_r$ be non-root goals in T 
chosen so that each non failing branch of T contains exactly one of 
them. Let $R_i$ for $i=1...r$, be the resultant of the derivation 
from 
$\If A$ down to $G_i$. Then the set of clauses $R_1\dots R_r$ is the 
partial evaluation of $A$ in $P$, denoted by $PE(P,A)$.. A partial 
evaluation of $P$ wrt $A$ is the normal program obtained from $P$ by 
replacing the set of clauses in $P$ whose head unifies with $A$, 
denoted $C_q$ with $PE(P,A)$; in symbols $PE_A(P)= P[C_q:=PE(P,A)]$, 
for each set of clause $C_q$ and $q=A$.

\newcommand{\pt}{$\Gamma \atop {\Pi \atop A}$}
\pt
In details: a contraction $cn$ is a map between proof-trees such that 
$cn(\Pi,\Gamma,A,\q)$ is
\[
  \frac{\q\Gamma}{\q A}$. The latter
is what is known as a {\em resultant} \cite{LS91} and will be called 
$R(\Pi)$. Let $Cont(A)$ be the set of mgc of $A$. Then 
\[
PE_A(P) = P[C_q :=R(\Pi)]
\]
for all $\Pi \in Cont(A)$. 

We obtain this way a possibly infinite sequence of partially 
evaluated programs can be put in a one-to-one correspondence
to  an unfolding sequence in the obvious way.


We need to prove the adequacy theorem. First,
we take as the semantic function $Sem_{S,F}(P,A)$ as the set of 
instances of $A$ which belongs to the success (resp.\ ) failure set 
of $P$.

Let us consider success.

\bit
\item
correctness follows immediately from the validity of the introduction 
rules.
\item
completeness requires a closure condition.
\enit

\begin{thebibliography}{999}

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

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

\bibitem {SH93} P. Schroeder-Heister. Rules of Definitional 
Reflection. In: LICS93, pp. 222--232.

\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.

\end{thebibliography}

\appendix
\begin{Ppn}[Admissibility of $E_p$] If there is $\Pi:: \Gamma
, [B],\Delta, p(a) \prv C$ using $E_p$, then there is another proof
from the same hypothesis withoiut $E_p$.
\end{Ppn}

\begin{proof}
By induction on the length of a subproof $\Pi_i:: \Gamma
, [B],\Delta, p(a) \prv C$
\bit
\item 
$\mid \Pi_i\mid = 0$, then $C$ is an assumption.
\item
Otherwise the last step is by $I_p$: then apply the inductive 
hypothesis to the sub-subderivation.
\enit
\end{proof}

\end{document}

