Towards a Logic for Reasoning about Logic Programs Transformation

Alberto Momigliano^{∗} Department of Philosophy Carnegie Mellon University 15213 Pittsburgh PA, USA Tel. +1-412-268-1413

              am4e@andrew.cmu.edu

Mario Ornaghi Dipartimento di Scienze dell’Informazione Universita’ degli studi di Milano Via Comelico 39/41, Milano, Italy Tel. +39-2-55006331

              ornaghi@dsi.unimi.it

Abstract

We give a proof-theoretic analysis of logic programs transformations, viewed as operations on proof trees in the sense of [3, 4, 9, 10]. We present a logic for reasoning about (equivalence preserving) transformations of logic programs. 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 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 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 logic programming languages satisfying the simple requirement of regularity.

1 Introduction

We give a proof-theoretic analysis of logic programs transformations, viewed as operations on proof trees in the sense of [3, 4, 9, 10]. We present a logic for reasoning about (equivalence preserving) transformations of logic programs.

∗This work was mostly completed during a visit by the first author to the Dipartimento di Scienze dell’Informazione, Universita’ degli studi di Milano.

Our framework is natural deduction, although a totally analogous presentation can be given in terms of sequent calculi with definitional reflection [14]. We are not going to fully detail in this abstract the systems we are using, though we have shown elsewhere [9] (and it is now beginning to be common knowledge, see [4]) that,w.r.t. the language of definite clauses, interpreting : − and , as implication and conjunction yields positive intuitionistic, i.e. minimal logic. Our basic system, let us call it L_{0}, contains only the assumption rule and a rule for applying clauses (ca), similar to the rule of modus ponens.

We shall follow this path:

1. We achieve the transformation via the usage of inference rules; thus, the target program may be obtained as a set Q of clause introduction proofs with axioms from the source program P of the form:

Q = \frac{Π_{1}}{C_{1} ← Γ_{1}} r_{1}, …, \frac{Π_{n}}{C_{n} ← Γ_{n}} r_{n}

2. We show the rules to be (weakly) admissible, that is every proof Π :: A which uses those rules can be translated in a proof t(Π) of the same consequence without them in the basic system and axioms from Π. As the proofs in L_{0} correspond to SLD-derivations, this means that every derivation from Q = C_{1} ← Γ_{1}, …, C_{n} ← Γ_{n} gets translated in a derivation from P.

3. We will look for some adequacy results. Namely, verifying that the success set is preserved requires certain completeness conditions on Π_{1}, …, Π_{n}; for finite failure we need furthermore the strict monotonicity of the translation function.

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

The paper is organized as follows: in Section 2 we review the basic notions of our framework [9, 10] and we relate it to SLD-resolution w.r.t. success and failure. Section (3) presents the general transformation schema. The next Section (4) depicts the proof-theoretical reconstruction of Partial Deduction. Section 5 targets Program Transformation more in general. After a brief Conclusion

2 Background on Proof Trees

First we recall some necessary basic definitions: we assume some familiarities with standard notions of natural deduction [12] and logic programming [1].

We use a variant of the Axiom Application Rule introduced in [9]. We consider the Clause Application Rule ca, for applying axioms of the form B ← A_{1}, …, A_{n}. Using the formalism of natural deduction, ca can be expressed as follows:

\frac{θA_{1} ⋯ θA_{n}  B ← A_{1}, …, A_{n}}{θB} ca

where the applied clause is the major premise, θA_{1}, …, θA_{n} is the (possibly empty, if n = 0) sequence of the minor premises and θB is the consequence. Next, we inductively introduce the notion of proof tree (pt).

Definition 1 (Proof Tree) An atom A is a (trivial) proof tree. If Π_{1} :: θA_{1},…, Π_{n} :: θA_{n} are proof trees and C is a clause of the form B ← A_{1}, …, A_{n}, then the following is also a proof tree:

\frac{{Π_{1} \atop θA_{1};}⋯{Π_{n} \atop θA_{n};} C}{θB} ca

We say that, for the non-trivial case, a formula is an assumption of a proof tree if it is a minor premise in some leaf. We write this as

{… H … \atop Π}

The clauses of a proof tree are the ones appearing as major premises. The root of a proof tree is called its consequence and is denoted by Π :: B. A proof tree is a proof of B from a set P of clauses iff B is its consequence, its clauses belong to P and it has no assumption.

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

Definition 2 (Proof Trees Equality) Π_{1} = Π_{2} if their major premises occurrences are equivalent up to renaming, while the other formulae occurrences are identical.

Definition 3 (Proof Trees Substitution) θΠ is the tree obtained by simultaneously applying a substitution θ to the root and to all the formulae occurring as minor premises. The major premises are left untouched.

The class of proof trees is closed under The subsumption ordering on formulae is then lifted to proof trees as follows.

Definition 4 (Subsumption Ordering) Π_{1} is less general than Π_{2}, written Π_{1} ≤ Π_{2}, if there is a substitution σ such that σΠ_{2} = Π_{1}. We also say that Π_{2} subsumes Π_{1}. Moreover, we define Π_{1} ≡ Π_{2} ↔ Π_{1} ≤ Π_{2} ∧ Π_{2} ≤ Π_{1}.

One can easily see that ‘≡’ corresponds to equivalence on proof trees up to renaming.

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 ?? 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:

Definition 5 (Skeleton) The Skeleton sk(Π) of a proof tree Π is defined recursively as follows:

• Basis: sk(A) = []

• Step:

sk (\frac{Π_{1}; … Π_{n}; C}{B} ca) = \frac{sk(Π_{1}); … sk(Π_{n}); C}{[]} ca

That is, the skeleton of a tree is obtained by systematically replacing the root and minor premises with holes: the (equivalence class of) major premises are unchanged.

Definition 6 (Similarity) Two proof trees Π_{1}, Π_{2} are said to be similar, written Π_{1} ∼ Π_{2}, whenever sk(Π_{1}) = sk(Π_{2}).

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

Definition 7 (Most General Proof Tree) Π is a most general proof tree (mgpt) if it is maximal among similar trees.

As shown in [9], the system using the rule ca is 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 Π, i.e. similarity classes containing only continuations of Π, where the latter are thusly defined:

Definition 8 (Continuation) Let B ← A_{1}, …, A_{n} be a clause C and

{… H … \atop Π}

be a proof tree with an applicable assumption H, i.e. such that θB = θH, for some substitution θ. The one-step continuation of Π selecting H and applying C w.r.t. θ is the proof tree:

\frac{θA_{1}; ⋯; θA_{n}  B ← A_{1}, …, A_{n}}{{… θH … \atop θΠ}} ca

Π_{2} is a continuation of Π_{1}, written Π_{1} ⪯ Π_{2}, if Π_{2} can be obtained from Π_{1} by a sequence of one-step continuations.

← sum(ss0, s0, X_{0}) ⪯ \frac{sum(ss0, 0, X_{1}) C_{1}}{sum(ss0, s0, sX_{1})} ⪯ \frac{C_{0}}{\frac{sum(ss0, 0, ss0) C_{1}}{sum(ss0, s0, sss0)}}

Figure 1: Continuations of the goal ← sum(ss0, s0, X_{0})

Note that substitutions in continuation steps do not need to be most general unifiers. One can easily see that:

Proposition 9 Π_{1} ⪯ Π_{2} if and only if there is a substitution σ such that σΠ_{1} is an initial subtree of Π_{2}.

Definition 10 (Most General Continuations) A continuation Π^{∗} of Π is most general (mgc) if, for every other continuation Δ similar to Π^{∗}, Δ ≤ Π^{∗}. A continuation is canonical iff it is a one-step mgc.

Since similarity classes of Π-continuations are regular [9], every mgc Π^{∗} of a given Π is unique up to renaming. One can also see that canonical continuations are the one-step continuations that use most general unifiers.

Definition 11 (Height) The height of a proof tree, written h(Π), is defined here as the length of its minimum branch.

2.1 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 SUM, containing the following clauses:

\begin{matrix}C_{0} : & sum(X, 0, X) ← \\ C_{1} : & sum(X, s(Y), s(Z)) ← sum(X, Y, Z) \end{matrix}

An SLD-derivation for a goal ⟨← A, θ⟩ can be seen as a stepwise construction of a pt Π :: θA. Figure 1 shows the continuations corresponding to the SLDderivation:

← sum(ss0, s0, X_{0}) θ_{1} = [X/ss0, Y/0, X_{0}/s(Z)]
← sum(ss0, 0, X_{1}) θ_{2} = [Z = ss0]
← □

Notice that the formulae in the current goal correspond to the assumptions of the relative pt.

In this way every SLD-derivation can be translated into a pt and this yields the proof-theoretical equivalence between the two systems (see [9]). More formally:

Definition 12 A SLD-derivation is incomplete if at any point no literal is selected and the derivation is thusly terminated. It is relaxed if mgu’s are not necessarily used. If idempotent mgu’s are used, then it is canonical.

Let P be a definite program, ← G a goal and ← G, ← G_{1}, …, ← G_{m} an incomplete relaxed SLD-derivation for P ∪{← G} with substitutions θ_{1}, …, θ_{m}. Let θ be the restriction of θ_{1} ⋯ θ_{m} to the variables of G. We say that the derivation has resultant θG ← G_{m}.

Theorem 13 Let P be a definite program and A an atom:

a) If there is an incomplete relaxed SLD-derivation for P ∪ {← A} with resultant (δA ← G_{m}), then there is a partial proof Π :: δA in L_{0}, using only axioms from P with open assumptions G_{m}. If the derivation is canonical, then Π :: δA is a most general continuation of A.

b) If there is a partial proof Π :: θA in the L_{0} with axioms from P and open assumptions G_{m}, then there is an incomplete relaxed SLD-derivation of P ∪ {← A} with resultant (δA ← G_{m}). If Π :: θA is a most general continuation of A, then the derivation is canonical.

Proof We give the proof for G_{0} = A. (a) Let G_{0}, G_{1}, …, G_{m} (with clauses C_{1}, …, C_{m} and substitutions θ_{1}, …, θ_{m}) be a relaxed, possibly incomplete derivation, with G_{0} = ← A. For 0 ≤ i ≤ m, let δ_{i} be the composition of the θ_{1}, …, θ_{i} and ← A_{i_{1}}, …, A_{i_{h_{i}}} be the atoms in the goal G_{i}; starting with i = 0, we associate to G_{0}, …, G_{i} a proof tree Π_{i} :: δ_{i}A with assumptions A_{i_{1}}, …, A_{i_{h_{i}}}, as follows:

Step 0. Associate A to G_{0}.

Step i+1. Let Π :: δ_{i}A be the proof tree associated to G_{0}, …, G_{i} at step i and let G_{i+1} be obtained applying C_{i+1} to the selected atom A_{n_{i}}, with unifier θ_{i+1}; build the one-step continuation of Π_{i} :: δ_{i}A selecting A_{n_{i}} and applying C_{i+1} w.r.t. θ_{i+1}. If at each step in G_{0}, …, G_{n} we apply only mgu’s, the corresponding one-step continuations are canonical and we obtain a mgpt.

(b) Π :: θA can be obtained by at least one sequence A = Π_{0} ⪯ Π_{1} ⪯ … ⪯ Π_{n} = Π; the corresponding SLD-derivation is G_{0}, …, G_{n}, where G_{i} are the assumptions of Π_{i}, i = 1 … n. If Π :: θA is a mgpt, then the continuations must be canonical and therefore G_{0}, …, G_{n} is canonical.

There is a natural proof-theoretic characterization of finite failure,

Definition 14 An assumption is failed w.r.t. P iff it has no continuation with clauses from P. An ended tree w.r.t. P is either a proof or a proof tree with a failed assumption.

Definition 15 (Failed Proof Tree) A proof tree Π is failed with respect to a program P if there is at least one assumption of Π such that there are no applicable clause in P.

Proposition 16 (Finite Failure) An atom A is finitely failed if and only if there exists a k such that every ended pt Π :: σA has at least one failed assumption of height less or equal to k.

Proposition 17 ( Failure) An atom A is failed if and only if every ended pt is failed.

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, i.e. there is a sequence of proof trees with increasing height. An infinite pt can be seen as the ‘limit’ of this sequence.

3 The General Schema

a) We look for (weakly) admissible rules, that allow to derive new clauses starting from the ones of a program P. Weak admissibility means that the translation t is a partial function that is defined for all the proofs (without assumptions) and for a suitable kind of proof trees with assumptions.

b) These rules are used to transform a source program P into a derived program Q:

Q = \frac{Π_{1}}{C_{1} ← Γ_{1}} r_{1}, …, \frac{Π_{n}}{C_{n} ← Γ_{n}} r_{n}

c) Weak admissibility entails partial correctness, i.e. if there is a derivation of A in Q, then there is one in P. 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.

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

Definition 18 (Weak Admissibility) For every proof Π_{1} :: P ⊢_{C_{1}} H there is a proof Π_{0} :: P ⊢_{C_{0}} H

Definition 19 A set of atoms is G-closed if each atom containing a predicate symbol occurring in G is an instance of an atom in G.

1. Partial correctness coincides with the existence of a translation function, such that if there is a derivation of A in Q, then there is one in P.

2. Let P be a source program,

Q = \frac{Π_{1}}{A_{1} ← Γ_{1}} ci, …, \frac{Π_{n}}{A_{n} ← Γ_{n}} ci

be a derived program, and G be a finite set of atoms. We say that Q is G-complete w.r.t. success iff (i) For every Π :: P ⊢_{L_{0}} σH, that proof can be partitioned as follows:

Π1^{′} … Πn^{′}
δA_{1} … δA_{n}
Π′
δA

(ii) A_{i} ← Γ_{i} is G-closed

3. We state the following monotonicity properties of t w.r.t. continuations: (a) h(Π_{1}) < h(Π_{2}) then h(t(Π_{1})) < h(t(Π_{2})).

(b) if t is partial then for every pt with arbitrary high continuations,

there is a continuation Π^{∗} such that t(Π^{∗} is defined.

4. Let P, Q be as above. We say that Q is G-complete w.r.t. infinite tress iff

(i)′ There is a k such that every Π :: P ⊢_{L_{0}} σH, with height(Π) > k

satisfies (i) (ii)′ = (ii)

To summarize: Q may be

1. sound (partially correct)

2. G-complete w.r.t. success

3. strictly monotonic

4. G-complete w.r.t. infinite pt’s Definition 20 For a program P and a goal G, let [G] define the closure under substitution induced by the language of P, let SS_{P} be the success set and Infpt_{P} the set of infinite pt’s of P. Theorem 21 Given P and Q as above:

1. entails SS_{Q} ⊆ SS_{P}

2. entails SS_{P} ∩ [G] ⊆ SS_{Q}

3. entails Infpt_{Q} ⊆ Infpt_{P}

4. entails Infpt_{P} restricted to [G] ⊆ Infpt_{Q} Corollary 22

1. and 2. entail success is preserved over G 1.2.3. and 4. entail success and finite failure is preserved over G

c_{0} ; \overline{ca} ; e(0) c_{2} ; \overline{ca} ; o(s0) c_{1} ; \overline{ca} ; e(ss0) {Π_{0} \atop e(ssX) ← e(X)}

\overline{ca}

e(ssss0)

Figure 2: Proof tree with the ci rule

4 Partial Deduction

We are now in the position of giving a more abstract view of Partial Deduction (PD) [5, 6] thanks to our framework. Note that we will not be concerned with the pragmatics of PD [13, 11, 2] 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) Γ.

\frac{\overline{Γ}u ; Π C}{C ← Γ}ci, u

The latter allows the derivation of resultants. For instance, from the program EO in example 34 we can derive the resultant Π_{0} :: e(ssX) ← e(X):

\overline{e(X)}^{0} c_{2} ; \overline{ca} ; o(sX) c_{1}

\overline{ca}

e(ssX)

ci, 0

e(ssX) ← e(X)

The usage of ca in conjunction with ci yields a proof tree like the one in Figure 2.

As one can see, only the derived clause e(ssX) ← e(X) plays a role in the derivation of the proof tree concluded by ca. More in general, let us consider a set of pt’s Q = {Π_{i} :: C_{i} ← Γ_{i}} for i = 1 … n. Provided that each Π_{i} applies only clauses from P, then each C_{i} ← Γ_{i} is a resultant for P w.r.t. C_{i}. If in a proof tree that applies these derived resultants by ca we hide their proofs, it is apparent that we obtain a pt with clauses C_{1} ← Γ_{1}, …, C_{n} ← Γ_{n}. That is, we may forget the tree which has proved the resultant and we can consider Q as a program.

Therefore we can formalize the Partial Deduction of a source program P with respect to a set G of atoms as the derivation of a program Q = {Π_{i} :: C_{i} ← Γ_{i}}, where C_{i} are instances of formulae of G and the proofs Π_{i} may use ca and ci and the clauses of P.

We now address the problem of adequacy: the first issue is the 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 ⊃-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.

Theorem 23 (Normalization) For every proof tree Π :: Γ ⊢_{L_{1}} B with clauses from P there is a proof tree Π^{∗} :: Γ ⊢_{L_{0}} B, i.e. without occurrences of ci.

Proof We set Π^{∗} = t(Π), where t is the function defined below, by induction on the derivation Π of B.

• t(A) = A

• The applied clause is the program clause C:

t ( \frac{{Π_{1} \atop θA_{1};}⋯{Π_{n} \atop θA_{n};} C}{B} ca) = \frac{{t(Π_{1}) \atop θA_{1};}⋯{t(Π_{n}) \atop θA_{n};} C}{B} ca

• The applied clause has been introduced by ci:

t ( \frac{{Π_{1} \atop σA_{1};} ⋯ {Π_{n} \atop σA_{n};} \frac{A_{1} … A_{n} ; {Π_{0} \atop B}}{B ← A_{1} … A_{n}} ci}{σB}ca) = t(Π_{1}) … t(Π_{n}) ; σA_{1} … σA_{n} ; {σ(t(Π_{0})) \atop σB}

Therefore this mapping preserves assumptions and consequences while it eliminates every occurrences of the ci rule. Indeed, t 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.

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.

Theorem 24 (Partial Deduction Theorem) Let P be a source program, G a set of atoms and Q a derived program such that Q is G-closed and G-complete with respect to P. Then, for every θA ∈ G

1. If there is a pt in Q of the form Π :: Γ ⊢_{L_{1}} θA then there is a pt Π′ :: Γ ⊢_{L_{0}} θA from P 2. If there is a proof Π :: θA from P, then there is a proof Π′ :: θA in Q

3. If there is a pt Π :: θA from P which can be indefinitely continuated, then the same holds for Q

4. A has a A-complete finitely failed set from P iff the same holds for Q.

Proof

1. Trivial: set Π′ = t(P)

2. Let us consider a pt Π with rules from P, no assumption and conclusion σA for A ∈ G. By G-completeness there is an i such that t(Π_{i}) ⪯ Π i.e.

Π = Π_{1} … Π_{n} ; σA_{1} … σA_{n} ; {σ(t(Π_{i})) \atop σA}

Now we build the hybrid pt, for n > 0,

\frac{{Π_{1} \atop σA_{1};} ⋯ {Π_{n} \atop σA_{n};} \frac{Π_{i}^{∗}}{C←A_{1}...A_{n}}}{σC}

By G-closure each σA_{i} with predicates in G is an instance of some atom in G and we can iterate the same procedure to every Π_{i}. This process terminates since at each step the height of the current set Π_{1}, …, Π_{n} decreases.

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

4. (←) Suppose A has an A-complete finitely failed set of mgc’s in Q of the form Π_{1}, …, Π_{n}. Consider its normalization: each t(Π_{i}) has a complete and failed set of mgc’s. To show this, suppose the converse: then there would be a continuation of t(Π_{i}) which is either a proof or can be continued ad libitum. But this is impossible due to points 2 and 3. Substituting t(Π_{i}) with the correspondent complete and failed sets of mgc’s yields the A-complete and failed set of continuations with clauses in P.

(→) A has a A-complete finitely failed set of mgc’s from P. Assuming the negation of the thesis, we would have the following subcases:

– there is a proof Π :: σA from P. But thus t(Π) :: σA would be a proof of σA, continuation of some pt from P.

– There is Π :: σA with arbitrary high continuations. But for the monotonicity of t w.r.t. h there would be a proof Π^{∗} with arbitrary high continuations.

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:

Corollary 25 Let Q be derived by PD from a source program P. If Q is complete and G-closed, then it has the same success and finite failure sets of P.

5 Program Transformation

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 [11, 15, 16, 17].

5.1 Unfolding

Unfolding needs the admissible rule ci, for which we have already given the translation function t. A transformation of a program P corresponds to the derivation of a new program:

Q = \frac{Γ_{1} ; \begin{matrix}Π_{1} \\ C_{1} \end{matrix}}{C_{1} ← Γ_{1}} ci, …, \frac{Γ_{n} ; \begin{matrix}Π_{n} \\ C_{n} \end{matrix}}{C_{n} ← Γ_{n}} ci

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

Definition 26 (Unfold-Completeness) The derived program Q is unfoldcomplete with respect to P if the set of proofs t(Π_{1}), …, t(Π_{n}) is P-complete (see Definition 33).

Since t is strictly monotone, the completeness of Q allows to prove that the success and finite failure sets are preserved. The proof is identical to the one of Theorem 24 of the previous section and therefore it is omitted.

Example 27 Referring back to the program EO of Example 34 the unfolded program Q (which brings back the usual and more efficient definition of even and odd) is unfold-complete:

Q = \{ \frac{c_{0}}{\frac{e(0)}{e(0) ←}}  \frac{\overline{e(X)} c_{2}}{\frac{o(sX) c_{1}}{\frac{e(ssX)}{e(ssX) ← e(X)}}}  \frac{c_{0}}{\frac{e0 c_{1}}{\frac{o(s0)}{o(s0) ←}}}  \frac{\overline{o(X)} c_{2}}{\frac{e(sX) c_{1}}{\frac{o(ssX)}{o(ssX) ← o(X)}}} \}

Usually [17, 11], 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 Q, since it explicitly contains the proofs of its clauses, starting from the ones of the source program.

5.2 Folding

The folding rule refers to a folding set

F = \{σ_{1}B_{1} ; \begin{matrix}Π_{1} \\ σ_{1}A \end{matrix} , …, σ_{k}B_{k} ; \begin{matrix}Π_{k} \\ σ_{k}A \end{matrix} \}

of proof trees with clauses from P, such that F is A-complete^{1}.

For such a F, we have the following rules:

\frac{H ← Γ, σ_{1}B_{1} , …, H ← Γ, σ_{n}B_{n}}{H ← Γ, A} fold(F)

\frac{σ_{1}(H ← Γ, B_{1}) , …, σ_{n}(H ← Γ, B_{n})}{H ← Γ, A} fold^{ω}(F)

In fold the condition dom(σ) ∩ vars(Γ, H) = ∅ must be satisfied. fold allows to treat, for example, Tamaki&Sato’s [17] and Shepherdson’s [16] folding. The rule fold^{ω} does not have restrictions on σ. It allows to treat general folding [11] (R2, p. 268). Indeed, fold^{ω} is more general than fold. We distinguish the two rules because they have different logical explanations, as briefly remarked in the conclusions.

Example 28 Given the following program minmax to determine the minimum and maximum of a list, where the definition of sup and inf are left open:

m_{0} : min([X], X)  ←
m_{1} : min([X|XS], Y)  ← min(XS, Z), inf(X, Y, Z).
m_{2} : max([X], X)  ←
m_{3} : max([X|XS], Y)  ← max(XS, Z), sup(X, Y, Z)).
m_{4} : minmax(XS, Min, Max) ← min(XS, Min), max(XS, Max).

and this folding set:

F = \{\frac{min(XS, Min) max(XS, Max) m_{4}}{minmax(XS, Min, Max)} ca\}

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.

1This requirement may be relaxed.

\frac{\frac{m_{0}}{min([X], X)} \frac{m_{2}}{max([X], X)} m_{3}}{\frac{minmax([X], X, X)}{minmax([X], X, X) ←}}

\frac{\frac{\overline{min(XS, Y)} \overline{inf(X, Y, Min})}{min([X|XS], Min)} \frac{\overline{max(XS, Z)} \overline{sup(X, Z, Mmax)}}{max([X|XS], Max)} m_{3}}{\frac{minmax([X|XS], Min, Man)}{\frac{minmax([X|XS], Min, Man) ← min(XS, Y), inf(X, Y, Min), max(XS, Z), sup(X, Z, Max)}{minmax([X|XS], Min, Man) ← minmax(XS, Y, Z), inf(X, Y, Min), sup(X, Z, Max)}fold(F)}}

We thus obtain by folding the new recursive definition of minmax

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

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

The partial function t is recursively defined as follows:

• The base and the recursive cases for source clauses and clauses introduced by ci are as in Section 4.

• If the applied clause is introduced by fold, we have the following recursion, where Π^{∗}, Π^{′∗} are sequences of pt’s:

t ( \frac{\begin{matrix}Π^{∗} \\ δΓ \end{matrix} \begin{matrix}Π_{0} \\ δA \end{matrix} \frac{_{\{ \begin{matrix}Δ_{i} \\ H ← Γ, σ_{i}B_{i} \end{matrix} \}}}{H ← Γ, A}fold(F)}{δH}ca) = t ( \frac{\begin{matrix}Π^{∗} \\ δ′Γ \end{matrix} \begin{matrix}Π^{′∗} \\ δ′σ_{h}B_{h} \end{matrix} \begin{matrix}Δ_{h} \\ H ← Γ, σ_{h}B_{h} \end{matrix}}{δ′H} ca)

provided that t(Π_{0}) is a continuation of a proof Π_{h} ∈ F. Since the latter has consequence σ_{h}A and assumptions σ_{h}B_{h}, t(Π_{0}) has the form of an initial subproof δ′Π_{h}, continued at the top by a sequence of subproofs Π^{′∗} :: δ′σ_{h}B_{h}. The existence of the latter sequence allows to use it in the translation step. If t(Π_{0}) is not sufficiently high to be a continuation of any proof tree of F, we cannot find the sequence Π_{0}^{∗}, and we halt the translation with an undefined result.

• If the applied clause is introduced by fold^{ω}, the translation is defined in a way similar to fold (omitted here for conciseness).

Proposition 29 (Partial Correctness) If Π is a proof, then t(Π) 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 P.

The proof easily follows from the fact that, in every translation step related to the fold rules, t(Π_{0}) is a proof of δA and hence a continuation of some proof of the A-complete set F. For total correctness we need the adequate notion of completeness with respect to P.

Definition 30 (Fold-Completeness) Let P be a source program and Q = {Π_{j} :: C_{j} ← Γ_{j}}_{j∈J} be a program derived from P in L_{2}. We say that Q is fold-complete with respect to P if every proof tree

\frac{_{Γ \begin{matrix}Π_{j} \\ C_{j} ← Γ_{j} \end{matrix}}}{C_{J}} ca

has continuations that can be successfully translated and the set of all the translations is P-complete.

Theorem 31 (Total Correctness) If Q is fold-complete with respect to P, then for every L_{0}-proof Π :: H with clauses from P there is a L_{2}-proof Π^{∗} :: H with clauses from Q.

The proof, omitted, is similar, yet more complex, to the one of Theorem 24. By the last theorem, completeness with respect to P 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 selffolding. Consider the source program P

\begin{matrix}p ← r \\ r ← \end{matrix}

A p-complete F is

F = \{\frac{r p ← r}{p} ca\}

and the transformed program is

Q = \{ \begin{matrix}\frac{p ← r}{p ← p} & fold(F) \\ r ← \end{matrix} \}

Q is incomplete since for every continuation in Q of the proof tree below, say Π_{self}

\frac{p \frac{p ← r}{p ← p} fold(F)}{p}ca

the translation fails. On the other hand, the program Q_{1}

Q_{1} = \{ \begin{matrix}\frac{p ← r}{p ← p} & fold(F) \\ p ← r \\ r ← \end{matrix} \}

is complete. Indeed the continuation

\frac{\frac{r p ← r}{p} ca \frac{p ← r}{p ← p} fold(F)}{p}ca

is translated into this Π_{trad}

\frac{r p ← r}{p} ca

Finally one can prove that:

Theorem 32 If Q is fold-compete and t is strictly monotone, then finite failure is preserved.

For example, in Q_{1} t is not strictly monotonic. Indeed every translatable continuation of Π_{self} is translated in the same proof tree Π_{trad}. Therefore finite failure is not preserved, while success is.

6 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:

• 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. [8]

• second, this framework nicely generalizes to other logic programming languages: in fact it is possible to give general uniform Partial Deduction mechanism for logic programming languages that can be formulated as Axiom Application Systems [9, 10], say for normal or disjunctive programs.

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.

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:

• 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 P, by using only the logical rules. To derive fold^{ω}, we need also an ω-rule, as the one given in [14] 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.

• Using a set of basic rules, we can, in principle, derive new transformation rules. Of course, their usefulness is a question of experimental work.

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 [11].

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.

References

[1] K.A. Apt. Logic Programming. Handbook of Theoretical Computer Science, Leuween J. (ed.), Elsevier, 1990.

[2] O. Danvy, R. Gluck, & P. Thiemann. Partial Evaluation. International Seminar, Dagstuhl Castle, Germany, February 12-16: Selected Papers, LNCS 1110, Springer, 1996 .

[3] L. Hallnäs & P. Schroeder-Heister. A Proof-Theoretic Approach to Logic Programming: Clauses as Rules. Journal of Logic and Computation, v.1 no. 2. pp. 261-283, 1990.

[4] W. Hodges. Logical features of Horn clauses. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1: Logical Foundations, pages 449-503, Oxford University Press, 1993.

[5] J. Komorowski. A Prolegomenon to Partial Deduction Fundamenta Informaticae: Annales Societatis Mathematicae polonae, V. 18, pp. 41–63, 1993.

[6] J. Komorowski. Special Issue on Partial Deduction. In Journal of Logic Programming, Guest Editor, 1993.

[7] N. D. Jones. An Introduction to Partial Evaluation. Acm Computing Surveys, Volume 28, 3, pp. 480–531, 1996 [8] Lloyd J.W. & Shepherdson J. Partial Evaluation In Logic Programming,

Journal of Logic Programming, v.11, pp. 217-242, 1991.

[9] A. Momigliano & M. Ornaghi. Regular Search Spaces as a Foundation of Logic Programming. In: Extensions of Logic Programming, Dyckhoff R. (ed.), LNAI n. 798, Springer Verlag, 1994.

[10] A. Momigliano & M. Ornaghi. Regular Search Spaces and Constructive Negation. Journal of Logic and Computation, to appear.

[11] A. Pettorossi & M. Proietti. Transformation of Logic Programs: Foundation and Technique. Journal of Logic Programming, pp. 261–321, vol. 19–20, 1994.

[12] D. Prawitz. Natural Deduction. A Proof-Theoretical Study. Almquist & Wiksell, Stockholm, 1965.

[13] D. Sahlin. An Automatic Partial Evaluator for Full Prolog. Report, TRITA-TCS–9101, 1991.

[14] P. Schroeder-Heister. Rules of Definitional Reflection. In: Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 222–232, 1993.

[15] H. Seki. Unfold/Fold Transformation of Stratified Programs. TCS, 86:107– 139, 1991.

[16] J.C. Sheperdson. Unfold/Fold Transformations of Logic Programs. Math. Structure Comp. Science, 2:143–157, 1992.

[17] H Tamaki & T. Sato. Unfold/Fold Transformation of Logic Programs. In: Proc. of ICLP84, S-A Tärlund (Ed.), Uppsala,pp.127–138, 1984.

A Appendix

Definition 33 (A-Complete Sets) Let S = Π_{1}, …, Π_{n} be a set of continuations of A: S is A-complete w.r.t. P if there is a constant h_{max} such that:

a) every proof Π :: σA from P is a continuation of at least one pt of S

b) every proof tree Π :: σA with axioms from P of height greater than h_{max} is a continuation of at least one pt of S.

Example 34 Let us consider the program EO:

c_{0} : e(0)  ←
c_{1} : e(s(X)) ← o(X)
c_{2} : o(s(X)) ← e(X)

Now the following set of proof trees is e(X)-complete with h_{max} = 2.

\frac{c_{0}}{e(0)}ca Π_{2} = e(X) c_{2} ; \overline{ca} ; o(sX) c_{1} ; \overline{ca} ; e(ssX)

Indeed every proof of e(s^{n}0) is a continuation of Π_{2} and similarly for proof trees with (open) assumptions and height greater than 2.

This notion of A-completeness for sets of continuations easily generalizes to G-Completeness (w.r.t. P), for A ∈ G, and Completeness (w.r.t. P) tout court, that we call P-Completeness.

Example 35 (Continued) Now adding the following set of proof trees to those above we obtain a set EO-complete with h_{max} = 2.

c_{0} ; \overline{ca} ; e0 c_{1} ; \overline{ca} ; o(s0)  o(X) c_{2} ; \overline{ca} ; e(sX) c_{1} ; \overline{ca} ; o(ssX)

In the following we will often refer to P-Completeness simply as Completeness. This should not cause confusion with other common uses of the word.

Consider the proof of ← sum(ss0, s0, X_{0}):

\frac{C_{0}}{\frac{sum(ss0, 0, ss0) C_{1}}{sum(ss0, s0, sss0)}}

The most general pt in this similarity class is

\frac{C_{0}}{\frac{sum(X, 0, X); 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(Π)(A), of the skeleton of a member of the latter. This is achieved by the operator S(A).

Definition 36 (The Operator S(Π, A)) Let sk(Π) = S be the skeleton of a proof tree. Π^{∗} :: θA = S(Π, A) if and only if Π^{∗} is a mgc of A with skeleton S.In other terms S(Π, A) is the mgpt of the si;ilarity class {Π′ | Π′ = sk(Π)(θA)}

We now address the question of how to convert pt’s which are mgc’s of A from Q in their normalization from P. Consider:

sk(Π)(A) = {Π \atop σA}  sk(t(Π))(A) = {Π′ \atop δA}

Theorem 37 (sk(Π)(A)) = sk(t(Π))(A)

Let t_{S} be a map from skeletons with clauses from Q into skeletons with clauses from P: consider t(S(A)); it has skeleton sk(t(S(A))) independently from A. Hence we put

t_{S}(S) =_{def} sk(t(S(A)))

Note the following:

sk(Π :: A)(A) = Π :: A
t_{S}(S)(A) = t(S(A))

Hence

t(sk(Π)(A)) = t_{S}(sk(Π))(A)

If we prove

sk(t(Π))(A) = t_{S}(sk(Π))(A)

the theorem is proven since the following diagram would commute: diagramma di commutazione

\begin{matrix}P_{Q} & ⟶^{t} & P_{P} \\ ↓^{sk} & ≡ & ↓^{sk} \\ S_{Q} & ⟶^{t_{S}} & S_{P} \end{matrix}

Lemma 38 (Commutativity) sk(t(Π))(A) = t_{S}(sk(Π))(A).