arXiv:cs/0307022v2 [] 20 Feb 2004

Under consideration for publication in Theory and Practice of Logic Programming

1

Transformations of Logic Programs
with Goals as Arguments
ALBERTO PETTOROSSI
Dipartimento di Informatica, Sistemi e Produzione,
Università di Roma Tor Vergata, Via del Politecnico 1, I-00133 Roma, Italy
(e-mail: alberto.pettorossi@uniroma2.it)

MAURIZIO PROIETTI
IASI-CNR, Viale Manzoni 30, I-00185 Roma, Italy
(e-mail: proietti@iasi.rm.cnr.it)

Abstract
We consider a simple extension of logic programming where variables may range over goals
and goals may be arguments of predicates. In this language we can write logic programs
which use goals as data. We give practical evidence that, by exploiting this capability
when transforming programs, we can improve program eﬃciency.
We propose a set of program transformation rules which extend the familiar unfolding
and folding rules and allow us to manipulate clauses with goals which occur as arguments of predicates. In order to prove the correctness of these transformation rules, we
formally deﬁne the operational semantics of our extended logic programming language.
This semantics is a simple variant of LD-resolution. When suitable conditions are satisﬁed
this semantics agrees with LD-resolution and, thus, the programs written in our extended
language can be run by ordinary Prolog systems.
Our transformation rules are shown to preserve the operational semantics and termination.
KEYWORDS: program transformation, unfold/fold transformation rules, higher order
logic programming, continuations

1 Introduction
Program transformation is a very powerful and widely recognized methodology
for deriving programs from specifications. The rules + strategies approach to program transformation was advocated in the 1970s by Burstall and Darlington (1977)
for developing first order functional programs. Since then Burstall and Darlington’s
approach has been followed in a variety of language paradigms, including logical languages (Tamaki and Sato 1984) and higher order functional languages (Sands 1996).
The distinctive feature of the rules + strategies approach is that it allows us to separate the concern of proving the correctness of programs with respect to specifications
from the concern of achieving computational efficiency. Indeed, the correctness of
the derived programs is ensured by the use of semantics preserving transformation
rules, whereas the computational efficiency is achieved through the use of suitable

2

A. Pettorossi and M. Proietti

strategies which guide the application of the rules. The preservation of the semantics is proved once and for all, for some given sets of transformation rules, and
if we restrict ourselves to suitable classes of programs, we can also guarantee the
effectiveness of the strategies for improving efficiency.
In this paper we will argue through some examples, that a simple extension of
logic programming may give extra power to the program transformation methodology based on rules and strategies. This extension consists in allowing the use of
variables which range over goals, called goal variables, and the use of goals which
are arguments of predicates, called goal arguments.
In the practice of logic programming the idea of having goal variables and goal arguments is not novel. The reader may look, for instance, at (Sterling and Shapiro 1986;
Warren 1982). Goal variables and goal arguments can be used for expressing the
meaning of logical connectives and for writing programs in a continuation passing
style (Tarau and Boyer 1990; Wand 1980) as the following example shows.
Example 1
The following program P 1:
F ∨G ←F
F ∨G ←G
expresses the meaning of the or connective. The following program P 2:
p([ ], Cont ) ← Cont
p([X |Xs], Cont ) ← p(Xs, q(X , Cont ))
q(0, Cont ) ← Cont
uses the goal variable Cont which denotes a continuation. The goal p(l , true) succeeds in P 2 iff the list l consists of 0’s only.

Programs with goal variables and goal arguments, such as P 1 and P 2 in the above
example, are not allowed by the usual first order syntax of Horn clauses, where
variables cannot occur as atoms and predicate symbols are distinct from function
symbols. Nevertheless, these programs can be run by ordinary Prolog systems whose
operational semantics is based on LD-resolution, that is, SLD-resolution with the
leftmost selection rule. For the concepts of LD-resolution, LD-derivation, and LDtree the reader may refer to (Apt 1997)
The extension of logic programming we consider in this paper, allows us to write
programs which use goals as data. This extension turns out to be useful for performing program manipulations which are required during program transformation
and are otherwise impossible. For instance, we will see that by using goal variables and goal arguments, we are able to perform goal rearrangements (also called
goal reorderings in (Bossi et al. 1996)) which are often required for folding, without
affecting program termination and without increasing nondeterminism.
Goal rearrangement is a long standing issue in logic program transformation.
Indeed, although the unfold/fold transformation rules by Tamaki and Sato (1984)
preserve the least Herbrand model, they may require goal rearrangements and thus,
they may not preserve the operational semantics based on LD-resolution. Moreover,
goal rearrangements may increase nondeterminism by requiring that predicate calls

Transformations of Logic Programs with Goals as Arguments

3

have to be evaluated before their arguments are sufficiently instantiated, and in
many Prolog systems, insufficiently instantiated calls of built-in predicates may
cause errors at run-time. In (Bossi and Cocco 1994) it has been proved that by ruling out goal rearrangements, if some suitable conditions hold, then the unfolding,
folding, and goal replacement transformation rules preserve the operational semantics of logic programs based on LD-resolution and, in particular, these rules preserve universal termination, that is, the finiteness of all LD-derivations (Apt 1997;
Vasak and Potter 1986). But, unfortunately, if we forbid goal rearrangements, many
useful program transformations are no longer possible.
In this paper we will show through some examples that in our simple extension
of logic programming we can restrict goal rearrangements to leftward moves of goal
equalities. We will also show that these moves preserve universal termination and
do not increase nondeterminism, and thus, the deterioration of performance of the
derived program is avoided.
The following simple example illustrates the essential idea of our technique which
is based on the use of goal equalities. More complex examples will be presented in
Sections 2 and 7.
Example 2
Suppose that during program transformation we are required to fold a clause of the
form:
1. p(X ) ← a(X ), b(X ), c(X )
by using a clause of the form:
2. q(X ) ← a(X ), c(X )
We can avoid a leftward move of the atom c(X ) by introducing, instead, an equality
between a goal variable and a goal, thereby transforming clause 1 into the following
clause:
3. p(X ) ← a(X ), G = c(X ), b(X ), G
Now we introduce the following predicate q ′ which takes the goal variable G as an
argument:
4. q ′ (X , G) ← a(X ), G = c(X )
Then we fold clause 3 using clause 4, thereby getting the clause:
5. p(X ) ← q ′ (X , G), b(X ), G
At this point we may continue the program transformation process by transforming
clause 4, which defines the predicate q ′ , instead of clause 2, which defines the
predicate q. For instance, we may want to unfold clause 4 w.r.t. the goal c(X )
occurring as an argument of the equality predicate.

As this example indicates, during program transformation we need to have at our
disposal some transformation rules which can be used when goals occur as arguments. Indeed, in this paper:
(i) we will introduce transformation rules for our logic language which allows goals
as arguments,

4

A. Pettorossi and M. Proietti

(ii) we will show through some examples that the use of these rules makes it possible to improve efficiency without performing goal rearrangements which increase
nondeterminism, and
(iii) we will prove that, under suitable conditions, our transformation rules are correct in the sense that they preserve the operational semantics of our logic language
and, in particular, they preserve universal termination.
In order to show our correctness result, we will first define the operational semantics of our logic language with goal arguments and goal variables. This semantics
will be given in terms of ordinary LD-resolution, except for the following two important cases which we now examine.
The first case occurs when, during the construction of an LD-derivation, we
generate a goal which has an occurrence of an unbound goal variable in the leftmost
position. In this case we say that the LD-derivation gets stuck. This treatment of
unbound goal variables is in accordance with that of most Prolog systems which
halt with error when trying to evaluate a call consisting of an unbound variable.
The second case occurs when we evaluate a goal equality of the form: g1 = g2 . In
this case we stipulate that g1 = g2 succeeds iff g1 is a goal variable which does not
occur in g2 and it gets stuck otherwise. (In particular, for any goal g the evaluation
of the equality g = g gets stuck.) This somewhat restricted rule for the evaluation
of goal equalities is required for the correctness of our transformation rules, as the
following example shows.
Example 3
Let us consider the program Q 1:
1. h ← p(q)
2. p(G) ← G = q
3. q ← s
where h, p, q, and s are predicate symbols and G is a goal variable. If we unfold
the goal argument q in clause 1 using clause 3, we get the clause:
4. h ← p(s)
and we have the new program Q 2 made out of clauses 2, 3, and 4. By using ordinary
LD-resolution and unification, the goal h succeeds in the original program Q 1, while
it fails in the derived program Q 2, because s does not unify with q.

This example shows that the set of successes is not preserved by unfolding w.r.t. a
goal argument. Similar incorrectness problems also arise with other transformation
rules, such as folding and goal replacement. These problems come from the fact
that operationally equivalent goals (such as q and s in the above example) are not
syntactically equal.
In contrast, if we consider our restricted rule for the evaluation of goal equalities,
the LD-derivation which starts from the goal h and uses the program Q 1, gets stuck
when the goal q = q is selected. Also the LD-derivation which starts from the goal
h and uses the derived program Q 2, gets stuck when the goal s = q is selected.
Thus, the unfolding w.r.t. the argument q has preserved the operational semantics
based on LD-resolution with our restricted rule for evaluating goal equalities.

Transformations of Logic Programs with Goals as Arguments

5

In this paper we will consider two forms of correctness for our program transformations: weak correctness and strong correctness. Suppose that we have transformed a program P1 into a program P2 by applying our transformation rules. We
say that this transformation is weakly correct iff, for any ordinary goal, that is, a
goal without occurrences of goal variables and goal arguments, the following two
properties hold: (i) if P1 universally terminates, then P2 universally terminates,
and (ii) if both P1 and P2 universally terminate, then they compute the same set
of most general answer substitutions. The transformation from P1 to P2 is strongly
correct iff (i) it is weakly correct, and (ii) for any ordinary goal, if P2 universally
terminates, then P1 universally terminates.
Thus, when a transformation is weakly correct, the transformed program may
be more defined than the original program in the sense that there may be some
goals which have no semantic value in the original program (that is, either their
evaluation does not terminate or it gets stuck), whereas they have a semantic value
in the transformed program (that is, their evaluation terminates and it does not
get stuck).
This paper is organized as follows. In Section 2 we present an introductory example to motivate the language extension we will propose in this paper, and the
transformation rules for this extended language. In Section 3 we give the definition
of the syntax of our extended logic language with goal variables and goal arguments.
In Section 4 we introduce the operational semantics of our extended language.
In Sections 5 and 6 we present the transformation rules and the conditions under
which these rules are either weakly correct or strongly correct. For this purpose it
is crucial that we assume that: (i) the evaluation of any goal variable gets stuck if
that variable is unbound, and (ii) the evaluation of goal equalities is done according
to the restricted rule we mentioned above. We will also show that, if a goal does
not get stuck in a program, and we transform this program by using our rules,
then the given goal does not get stuck in the transformed program. In this case,
as it happens in the examples given in this paper, our operational semantics agrees
with LD-resolution, and we can execute our transformed program by using ordinary
Prolog systems.
In Section 7 we give some more examples of program transformation using our
extended logic language and our transformation rules. We also give practical evidence that these transformations improve program efficiency. In Section 8 we make
some final remarks and we compare our results with related work.

2 A Motivating Example
In order to present an example which motivates the introduction of goal variables
and goal arguments, we begin by recalling a well-known program transformation
strategy, called tupling strategy (Pettorossi and Proietti 1994). Given a program
where some predicate calls require common subcomputations (detected by a suitable
program analysis), the tupling strategy is realized by the following three steps.

6

A. Pettorossi and M. Proietti

The Tupling Strategy
(Step A) We introduce a new predicate defined by a clause, say T , whose body is
the conjunction of the predicate calls with common subcomputations.
(Step B) We derive a program for the newly defined predicate which avoids redundant common subcomputations. This step can be divided into the following three
substeps: (B.1) first, we unfold clause T , (B.2) then, we apply the goal replacement
rule to avoid redundant goals, and (B.3) finally, we fold using clause T .
(Step C) By suitable folding steps using clause T , we express the predicates which
are inefficiently computed by the initial program, in terms of the predicate introduced at Step (A).
A difficulty encountered when applying the tupling strategy is that, in order to apply
the folding rule as indicated at Steps (B) and (C), it is often necessary to rearrange
the atoms in the body of the clauses and, as already discussed in the Introduction,
these rearrangements may affect program termination or increase nondeterminism.
The following example shows that this difficulty in the application of the tupling
strategy can be overcome by introducing goal variables and goal arguments.
Example 4
Let us consider the following program Deepest:
1. deepest (l (N ), N ) ←
2. deepest (t (L, R), X ) ← depth(L, DL), depth(R, DR), DL ≥ DR,
deepest (L, X )
3. deepest (t (L, R), X ) ← depth(L, DL), depth(R, DR), DL ≤ DR,
deepest (R, X )
4. depth(l (N ), 1) ←
5. depth(t (L, R), D ) ← depth(L, DL), depth(R, DR), max (DL, DR, M ),
plus(M , 1, D )
where deepest (T , X ) holds iff T is a binary tree and X is the label of one
of the deepest leaves of T . The two calls depth(L, DL) and deepest (L, X ) in
clause 2 may generate common redundant calls of the depth predicate. Indeed,
both depth(t (L1, R1), N ) and deepest (t (L1, R1), X ) generate two calls of the form
depth(L1, DL) and depth(R1, DR). In accordance with the tupling strategy, we
transform the given program as follows.
(Step A) We introduce the following new predicate:
6. dd (T , D , X ) ← depth(T , D ), deepest (T , X )
(Step B.1) We apply a few times the unfolding rule, and we derive:
7. dd (l (N ), 1, N ) ←
8. dd (t (L, R), D , X ) ← depth(L, DL), depth(R, DR),
max (DL, DR, M ), plus(M , 1, D ),
depth(L, DL1), depth(R, DR1),
DL1 ≥ DR1, deepest (L, X )

Transformations of Logic Programs with Goals as Arguments

7

9. dd (t (L, R), D , X ) ← depth(L, DL), depth(R, DR),
max (DL, DR, M ), plus(M , 1, D ),
depth(L, DL1), depth(R, DR1),
DL1 ≤ DR1, deepest (R, X )
(Step B.2) Since depth is functional with respect to its first argument, by applying
the goal replacement rule we delete the atoms depth(L, DL1) and depth(R, DR1),
in clauses 8 and 9, and we replace the occurrences of DL1 and DR1 by DL and DR,
respectively, thereby getting the following clauses 10 and 11:
10. dd (t (L, R), D , X ) ← depth(L, DL), depth(R, DR), max (DL, DR, M ),
plus(M , 1, D ), DL ≥ DR, deepest (L, X )
11. dd (t (L, R), D , X ) ← depth(L, DL), depth(R, DR), max (DL, DR, M ),
plus(M , 1, D ), DL ≤ DR, deepest (R, X )
(Step B.3) In order to fold clause 10 using clause 6, we move deepest (L, X ) immediately to the right of depth(L, DL). Similarly, in the body of clause 11 we move
deepest (R, X ) immediately to the right of depth(R, DR). Then, by folding we derive:
12. dd (t (L, R), D , X ) ← dd (L, DL, X ), depth(R, DR), max (DL, DR, M ),
plus(M , 1, D ), DL ≥ DR
13. dd (t (L, R), D , X ) ← depth(L, DL), dd (R, DR, X ), max (DL, DR, M ),
plus(M , 1, D ), DL ≤ DR
(Step C) Finally, we fold clauses 2 and 3 using clause 6, so that to evaluate the
predicates depth and deepest we use the predicate dd , instead. Also for these folding
steps we have to suitably rearrange the order of the atoms. By folding, we derive
the following program Deepest1:
deepest (l (N ), N ) ←
deepest (t (L, R), D , X ) ← dd (L, DL, X ), depth(R, DR), DL ≥ DR
deepest (t (L, R), D , X ) ← depth(L, DL), dd (R, DR, X ), DL ≤ DR
dd (l (N ), 1, N ) ←
dd (t (L, R), D , X ) ← dd (L, DL, X ), depth(R, DR), max (DL, DR, M ),
plus(M , 1, D ), DL ≥ DR
13. dd (t (L, R), D , X ) ← depth(L, DL), dd (R, DR, X ), max (DL, DR, M ),
plus(M , 1, D ), DL ≤ DR
1.
14.
15.
7.
12.

In order to evaluate a goal of the form deepest (t , X ), where t is a ground tree and
X is a variable, we may construct an LD-derivation using the program Deepest1
which does not generate redundant calls of depth. This LD-derivation performs
only one traversal of the tree t and has linear length with respect to the size
of t . However, this LD-derivation is constructed in a nondeterministic way, and if
the corresponding LD-tree is traversed in a depth-first manner, like most Prolog
systems do, the program exhibits an inefficient generate-and-test behaviour. Thus,
in practice, the tupling strategy may diminish program efficiency.
The main reason of this decrease of efficiency is that, in order to fold clause 10,
we had to move the atom deepest (L, X ) to a position to the left of DL ≥ DR, and
this move forces the evaluation of calls of deepest (L, X ) even when DL ≥ DR fails.
(Notice that the move of deepest (R, X ) to the left of DL ≤ DR is harmless because

8

A. Pettorossi and M. Proietti

DL ≤ DR is evaluated after the failure of DL ≥ DR and, thus, DL ≤ DR never
fails.)

In the following example we will present an alternative program derivation which
starts from the same initial program Deepest. In this alternative derivation we will
use our extended logic language which will be formally defined in the following
Section 3. As already mentioned in the Introduction, when writing programs in our
extended language, we may use: (i) the goal equality predicate =, (ii) goal variables
occurring at top level in the body of a clause, and (iii) the disjunction predicate
∨. This alternative program derivation avoids harmful goal rearrangements and
produces an efficient program without redundant subcomputations.
Example 5
Let us consider the program Deepest listed at the beginning of Example 4 consisting
of clauses 1–5. By using disjunction in the body of a clause, clauses 2 and 3 can be
rewritten as follows:
16. deepest (t (L, R), X ) ← depth(L, DL), depth(R, DR),
((DL ≥ DR, deepest (L,X )) ∨ (DL ≤ DR, deepest (R,X )))
After this initial transformation step the derived program, call it DeepestOr, consists
of clauses 1, 4, 5, and 16.
Now we consider an extension of the tupling strategy which makes use of the
transformation rules for logic programs with goal arguments and goal variables.
These rules will be formally presented in Section 5. We proceed as follows.
(Step A) We introduce the following new predicate g which takes a goal variable G
as an argument:
17. g(T , D , X , G) ← depth(T , D ), G = deepest (T , X )
Notice also that in clause 17 the goal deepest (T , X ) occurs as an argument of the
equality predicate.
(Step B) We derive a set of clauses for the newly defined predicate g as follows.
(Step B.1) We unfold clause 17 w.r.t. depth(T , D ) and we derive:
18. g(l (N ), 1, X , G) ← G = deepest (l (N ), X )
19. g(t (L, R), D , X , G) ← depth(L, DL), depth(R, DR), max (DL, DR, M ),
plus(M , 1, D ), G = deepest (t (L, R), X )
Now, by unfolding clauses 18 and 19 w.r.t. the atoms with the deepest predicate,
we derive:
20. g(l (N ), 1, N , true) ←
21. g(t (L, R), D , X , G) ← depth(L, DL), depth(R, DR),
max (DL, DR, M ), plus(M , 1, D ),
G = (depth(L, DL1), depth(R, DR1),
((DL1 ≥ DR1, deepest (L, X )) ∨ (DL1 ≤ DR1, deepest (R, X ))))
(Step B.2) We perform two goal replacement steps based on the functionality of
depth, and from clause 21 we derive:

Transformations of Logic Programs with Goals as Arguments

9

22. g(t (L, R), D , X , G) ← depth(L, DL), depth(R, DR),
max (DL, DR, M ), plus(M , 1, D ),
G = ((DL ≥ DR, deepest (L, X )) ∨ (DL ≤ DR, deepest (R, X )))
(Step B.3) In order to fold clause 22 using clause 17, we first introduce goal equalities
and we then perform suitable leftward moves of those goal equalities. We derive the
following clause:
23. g(t (L, R), D , X , G) ← depth(L, DL), GL = deepest (L, X ),
depth(R, DR), GR = deepest (R, X ),
max (DL, DR, M ), plus(M , 1, D ),
G = ((DL ≥ DR, GL) ∨ (DL ≤ DR, GR))
Notice that we can move the goal equality GL = deepest (L, X ) to the left of the
test DL ≥ DR without altering the operational semantics of our program. Indeed,
this goal equality succeeds and binds the goal variable GL to the goal deepest (L, X )
without evaluating it. The goal deepest (L, X ) will be evaluated only when GL is
called. A similar remark holds for the goal equality GR = deepest (L, X ). Now, by
folding twice clause 23 using clause 17, we get:
24. g(t (L, R), D , X , G) ← g(L, DL, X , GL), g(R, DR, X , GR),
max (DL, DR, M ), plus(M , 1, D ),
G = ((DL ≥ DR, GL) ∨ (DL ≤ DR, GR))
(Step C) Now we express the predicate deepest in terms of the new predicate g by
transforming clause 16 as follows: (i) we first replace the two deepest atoms by the
goal variables GL and GR, (ii) we then introduce suitable goal equalities, (iii) we
then suitably move to the left the goal equalities, and (iv) we finally fold using
clause 17. We derive the following clause:
25. deepest (t (L, R), X ) ← g(L, DL, X , GL), g(R, DR, X , GR),
((DL ≥ DR, GL) ∨ (DL ≤ DR, GR))
Our final program Deepest2 is as follows:
1. deepest (l (N ), N ) ←
25. deepest (t (L, R), X ) ← g(L, DL, X , GL), g(R, DR, X , GR),
((DL ≥ DR, GL) ∨ (DL ≤ DR, GR))
20. g(l (N ), 1, N , true) ←
24. g(t (L, R), D , X , G) ←
g(L, DL, X , GL), g(R, DR, X , GR),
max (DL, DR, M ), plus(M , 1, D ),
G = ((DL ≥ DR, GL) ∨ (DL ≤ DR, GR))
Now, when we evaluate a goal of the form deepest (t , X ), where t is a ground tree
and X is a variable, Deepest2 does not generate redundant calls and it performs
only one traversal of the tree t . Deepest2 is more efficient than Deepest because in
the worst case Deepest2 performs O (n) LD-resolution steps to compute an answer
to deepest (t , X ), where n is the number of nodes of t , while the initial program
Deepest takes O (n 2 ) LD-resolution steps. The program Deepest2 can be run by an
ordinary Prolog system and computer experiments confirm substantial efficiency
improvements with respect to the initial program Deepest (see Section 7.6).

10

A. Pettorossi and M. Proietti

Efficiency improvements, although smaller, are obtained also when comparing
the final program Deepest2 with respect to the intermediate program DeepestOr
which has been obtained from the initial program Deepest by replacing clauses 2
and 3 by clause 16, thereby avoiding the repetition of the common goals in clauses 2
and 3. Indeed, although more efficient than Deepest in the worst case, the program
DeepestOr still takes a quadratic number of LD-resolution steps to compute an
answer to deepest (t , X ).

In Section 7 we will present more examples of program derivation and we will also
provide some experimental results.
3 The Extended Logic Language with Goals as Arguments
Let us now formally define our extended logic language. Suppose that the following
pairwise disjoint sets are given: (i) individual variables: X , X1 , X2 , . . . , (ii) goal variables: G, G1 , G2 , . . . , (iii) function symbols (with arity): f , f1 , f2 , . . . , (iv) primitive
predicate symbols: true, false, =t (denoting equality between terms), =g (denoting equality between goals), and (v) predicate symbols (with arity): p, p1 , p2 , . . .
Individual and goal variables are collectively called variables, and they are ranged
over by V , V1 , V2 , . . . Occasionally, we will feel free to depart from these naming
conventions, if no confusion arises.
Terms: t , t1 , t2 , . . ., goals: g, g1 , g2 , . . ., and arguments: u, u1 , u2 , . . ., have the following syntax:
t ::= X | f (t1 , . . . , tn )
g ::= G | true | false | t1 =t t2 | g1 =g g2 | p(u1 , . . . , um ) | g1 ∧ g2 | g1 ∨ g2
u ::= t | g
The binary operators ∧ (conjunction) and ∨ (disjunction) are assumed to be associative with neutral elements true and false, respectively. Thus, a goal g is the
same as true ∧ g and g ∧ true. Similarly, g is the same as false ∨ g and g ∨ false.
Goals of the form p(u1 , . . . , um ) are also called atoms. In the sequel, for reasons of
simplicity, we will write =, instead of =t or =g , and we leave it to the reader to
distinguish between the two equalities according to the context of use. Notice that,
according to our operational semantics (see Section 4), ∨ is commutative, ∧ is not
commutative, =t is symmetric, and =g is not symmetric.
Clauses c, c1 , c2 , . . . have the following syntax:
c ::= p(V1 , . . . , Vm ) ← g
where p is a non-primitive predicate symbol and V1 , . . . , Vm are distinct variables.
The atom p(V1 , . . . , Vm ) is called the head of the clause and the goal g is called the
body of the clause. A clause of the form: p(V1 , . . . , Vm ) ← true will also be written
as p(V1 , . . . , Vm ) ←.
Programs P , P1 , P2 , . . . are sets of clauses of the form:
p1 (V1 , . . . , Vm1 ) ← g1
..
.
pk (V1 , . . . , Vmk ) ← gk

Transformations of Logic Programs with Goals as Arguments

11

where p1 , . . . , pk are distinct non-primitive predicate symbols, and every nonprimitive predicate symbol occurring in {g1 , . . . , gk } is an element of {p1 , . . . , pk }.
Each clause head has distinct variables as arguments. Given a program P and
a non-primitive predicate p occurring in P , the unique clause in P of the form
p(V1 , . . . , Vm ) ← g, is called the definition of p in P . We say that a predicate p is
defined in a program P iff p has a definition in P .
An ordinary goal is a goal without goal variables or goal arguments. Formally, an
ordinary goal has the following syntax:
g ::= true | false | t1 =t t2 | p(t1 , . . . , tm ) | g1 ∧ g2 | g1 ∨ g2
where t1 , t2 , . . . , tm are terms. Ordinary programs are programs whose goals are
ordinary goals.
Notes on syntax.
(1) When no confusion arises, we also use comma, instead of ∧, for denoting conjunction.
(2) The assumption that in our programs clause heads have only variables as arguments is not restrictive, because we may always replace a non-variable argument,
say u, by a variable argument, say V , in the head of a clause, at the expense of
adding the extra equality V = u in the body.
(3) The assumption that in every program there exists at most one clause for each
predicate symbol is not restrictive, because one may use disjunctions in the body
of clauses. In particular, every definite logic program written by using the familiar
syntax (Lloyd 1987), can be rewritten into an equivalent program of our language
by suitable introductions of equalities and ∨ operators in the bodies of clauses.
(4) Our logic language is a typed language in the sense that: (i) every individual variable has type term, (ii) every function symbol of arity n has type
term n → term, (iii) true, false, and every goal variable have type bool , (iv.1) =t
has type term × term → bool , (iv.2) =g has type bool × bool → bool , and (v) every
predicate symbol of arity n has a unique type of the form: (term | bool )n → bool .
We assume that all our programs can be uniquely typed according to the above
rules.
4 The Operational Semantics
In this section we define the operational semantics of our extended logic language.
We choose a syntax-directed style of presentation which makes use of deduction
rules. For an elementary presentation of this technique, sometimes called structural
operational semantics or natural semantics, the reader may refer to (Winskel 1993).
Before defining the semantics of our logic language, we recall the following notions. By {V1 /u1 , . . . , Vm /um } we denote the substitution of u1 , . . . , um for the
variables V1 , . . . , Vm . As usual, we assume that the Vi ’s are all distinct and for
i = 1, . . . , m, ui is distinct from Vi . By ε we denote the identity substitution. By
ϑ ↾ S we denote the restriction of the substitution ϑ to set S of variables, that
is, ϑ ↾ S = {V/u | V/u ∈ ϑ and V ∈ S }. Given the substitutions ϑ, η1 , . . . , ηk , by
ϑ ◦ {η1 , . . . , ηk } we denote the set of substitutions {ϑη1 , . . . , ϑηk } (where, as usual,

12

A. Pettorossi and M. Proietti

juxtaposition of substitutions denotes composition (Lloyd 1987)). By gϑ we denote
the application of the substitution ϑ to the goal g. By mgu(t1 , t2 ) we denote a
relevant, idempotent, most general unifier of the terms t1 and t2 .
The set of all substitutions is denoted by Subst and the set of all finite subsets of Subst is denoted by P(Subst). Given A, B ∈ P(Subst), we say that A
and B are equally general with respect to a goal g iff (i) for every α ∈ A there
exists β ∈ B such that gα is an instance of gβ, and symmetrically, (ii) for every β ∈ B there exists α ∈ A such that gβ is an instance of gα. For example,
A = {{X /t }, {X /Y }, {X /Z }} and B = {{X /W }} are equally general with respect to the goal p(X ).
Given a set of substitutions A ∈ P(Subst) and a goal g, let mostgen(A, g) denote a
largest subset of {gϑ | ϑ ∈ A} such that for any two goals g1 and g2 in mostgen(A, g),
g1 is not an instance of g2 . For example, mostgen({{X /t }, {X /Y }, {X /Z }}, p(X ))
= {p(Y )}. Notice that the set denoted by mostgen is not uniquely determined.
However, it can be shown that, whatever choice we make for the set denoted by
mostgen, any two sets of substitutions A and B are equally general with respect
to a goal g iff there exists a bijection ρ from mostgen(A, g) to mostgen(B , g) such
that for any goal h ∈ mostgen(A, g), ρ(h) is a variant of h. In this case we write
mostgen(A, g) ≈ mostgen(B , g).
We use g[u] to denote a goal g in which we have selected an occurrence of its
subconstruct u, where u may be either a term or a goal. By g[ ] we denote the
goal g[u] without the selected occurrence of its subconstruct u. We say that g[ ]
is a goal context. For any syntactic construct r , we use vars(r ) to denote the set
of variables occurring in r and, for any set {r1 , . . . , rm } of syntactic constructs,
we use vars(r1 , . . . , rm ) to denote the set of variables vars(r1 ) ∪ . . . ∪ vars(rm ). In
particular, given a substitution ϑ, a variable belongs to vars(ϑ) iff it occurs either
in the domain of ϑ or in the range of ϑ. Given two goals g and g1 and a clause c of
the form p(V1 , . . . , Vm ) ← g[g1 ], the local variables of g1 in c are those in the set
vars(g1 ) − ({V1 , . . . , Vm } ∪ vars(g[ ])).
Given a program P , we define the semantics of P as a ternary relation P ⊢ g 7→ A,
where g is a goal and A is a finite set of substitutions, meaning that for P and g
all derivations are finite and A is the finite set of answer substitutions which are
computed by these derivations. The relation P ⊢ g 7→ A is defined by the deduction
rules given in Figure 1.
A deduction tree τ for P ⊢ g 7→ A is a tree such that: (i) the root of τ is
P ⊢ g 7→ A, and (ii) for every node n of τ with sons n1 , . . . , nk (with k ≥ 0),
there exists an instance of a deduction rule, say r, whose conclusion is n and whose
premises are n1 , . . . , nk . We say that n is derived by applying rule r to n1 , . . . , nk .
A proof of P ⊢ g 7→ A is a finite deduction tree for P ⊢ g 7→ A where every leaf is
a deduction rule which has no premises.
We say that P ⊢ g 7→ A holds iff there exists a proof of P ⊢ g 7→ A. If P ⊢ g 7→ A
holds and A 6= ∅, then we say that g succeeds in P , written P ⊢ g ↓ true. Otherwise,
if P ⊢ g 7→ ∅ holds, then we say that g fails in P , written P ⊢ g ↓ false. If g
either succeeds or fails in P we say that g terminates in P . We say that a goal g is
stuck iff it is either of the form G ∧ g1 , where G is a goal variable, or of the form

Transformations of Logic Programs with Goals as Arguments
(tt)
(ff )
(teq1)

13

P ⊢ true 7→ {ε}
P ⊢ false ∧ g 7→ ∅
if t1 and t2 are non-unifiable terms

P ⊢ (t1 = t2 ) ∧ g 7→ ∅

(teq2)

P ⊢ g mgu(t1 , t2 ) 7→ A
P ⊢ (t1 = t2 ) ∧ g 7→ (mgu(t1 , t2 )◦A)

(geq)

P ⊢ g2 {G/g1 } 7→ A
P ⊢ (G = g1 ) ∧ g2 7→ ({G/g1 }◦A)

if t1 and t2 are unifiable terms

if the goal variable G is not in vars(g1 )
(at )

(or )

P ⊢ g1 {V1 /u1 , . . . , Vm /um } ∧ g 7→ A
P ⊢ p(u1 , . . . , um ) ∧ g 7→ A ↾ S
where p(V1 , . . . , Vm ) ← g1 is a renamed apart clause of P
and S is vars(p(u1 , . . . , um ) ∧ g)
P ⊢ g1 ∧ g 7→ A1
P ⊢ g2 ∧ g 7→ A2
P ⊢ (g1 ∨ g2 ) ∧ g 7→ (A1 ∪ A2 )

Fig. 1. Operational Semantics

(g0 = g1 )∧g2 , where either g0 is a non-variable goal or g0 is a goal variable occurring
in g1 . We say that g gets stuck in P iff there exist a set A of substitutions and a
(finite or infinite) deduction tree τ for P ⊢ g 7→ A such that a leaf of τ is of the
form P ⊢ g1 7→ B and g1 is stuck. For instance, the goal (G = p) ∧ (G = q) gets
stuck in any program P . We say that g is safe in P iff g does not get stuck in P .
For every program P and goal g, the three cases: (i) g succeeds in P , (ii) g fails in
P , and (iii) g gets stuck in P , are pairwise mutually exclusive, but not exhaustive.
Indeed, there is a fourth case in which the unique maximal deduction tree with root
P ⊢ g 7→ A is infinite and each of its leaves, if any, is the conclusion of a deduction
rule which has no premises. In this case no A exists such that P ⊢ g 7→ A holds
and g does not get stuck in P .
Notes on semantics.
(1) In our presentation of the deduction rules we have exploited the assumption that
∧ and ∨ are associative operators with neutral elements true and false, respectively.
because it is an
For instance, we have not introduced the rule
P ⊢ false 7→ ∅
instance of rule (ff ) for g = true.
(2) Given a program P and a goal g, if there exists a proof for P ⊢ g 7→ A for some
A, then the proof is unique up to isomorphism. More precisely, given two proofs,
say π1 for P ⊢ g 7→ A1 and π2 for P ⊢ g 7→ A2 , there exists a bijection ρ from

14

A. Pettorossi and M. Proietti

the nodes of π1 to the nodes of π2 which preserves the application of the deduction
rules and if ρ(P ⊢ g1 7→ B1 ) = P ⊢ g2 7→ B2 then
(i)
(ii)
(iii)

g1 is a variant of g2 , and
∀β1 ∈ B1 ∃β2 ∈ B2 such that g1 β1 is a variant of g2 β2 , and
∀β2 ∈ B2 ∃β1 ∈ B1 such that g2 β2 is a variant of g1 β1 .

This property is a consequence of the fact that: (i) for any program P and goal g,
there exists at most one rule instance whose conclusion is of the form P ⊢ g 7→ A
for some A, and (ii) our rules for the operational semantics are deterministic, in the
sense that no choice has to be made when one applies them during the construction
of a proof, apart from the choice of how to compute the most general unifiers and
how to rename apart the clauses.
In particular, any two sets A1 and A2 of answer substitutions for a program
P and a goal g, are related as follows: if P ⊢ g 7→ A1 and P ⊢ g 7→ A2 then
∀α1 ∈ A1 ∃α2 ∈ A2 gα1 is a variant of gα2 and ∀α2 ∈ A2 ∃α1 ∈ A1 gα2 is a variant
of gα1 . Thus, A1 and A2 are equally general with respect to g. The same property
holds also for any two sets of computed answer substitutions which are constructed
by LD-resolution (recall that by LD-resolution we can construct different sets of
computed answer substitutions by choosing different most general unifiers and different variable renamings).
Notice that, if P ⊢ g 7→ A1 and P ⊢ g 7→ A2 hold, then A1 and A2 may
have different cardinality. Indeed, let us consider the program P consisting of the
following clause only:
p(X , Y , Z ) ← (X = Y ∧ Z = Y ) ∨ (X = Z ∧ Y = Z )
In this case, since both Z /Y and Y /Z are most general unifiers of Y = Z ,
we have that both P ⊢ p(X , Y , Z ) 7→ {{X /Y , Z /Y }, {X /Z , Y /Z }} and P ⊢
p(X , Y , Z ) 7→ {{X /Y , Z /Y }} hold. Notice also that the substitution {X /Y , Z /Y }
is more general than the substitution {X /Z , Y /Z } and vice versa.
(3) If P ⊢ g 7→ A and ϑ ∈ A, then the domain of ϑ is a subset of vars(g).
(4) In the presentation of the deduction rules for the ternary relation P ⊢ g 7→ A,
the program P never changes and thus, it could have been omitted. However, the
explicit reference to P is useful for presenting our Correctness Theorem (see Theorem 2 in Section 6).
(5) We assume that in any relation P ⊢ g 7→ A, the program P and the goal g have
consistent types, that is, the type of every function and predicate symbol should be
the same in P and in g. For instance, if P = {p(G) ←} where G is a goal variable,
then P ⊢ p(0) 7→ {ε} does not hold, because in the program P the predicate p has
type bool → bool , while in the goal p(0) the predicate p has type term → bool .
Moreover, for any relation P ⊢ g1 7→ A1 occurring in the proof of P ⊢ g 7→ A, we
have that program P and goal g1 have consistent types.
Now we discuss the relationship between LD-resolution and the operational semantics defined in this section. Apart from the style of presentation (usually LDresolution is presented by means of the notions of LD-derivation and LD-tree (Apt 1997;
Lloyd 1987)), LD-resolution differs from our operational semantics only in the treat-

Transformations of Logic Programs with Goals as Arguments

15

ment of goal equality. Indeed, by using LD-resolution, the goal equality g1 = g2 is
evaluated by applying the ordinary unification algorithm also in the case where g1
is not a goal variable or g1 is a goal variable occurring in vars(g2 ). In contrast,
according to our operational semantics, a goal of the form g1 = g2 is evaluated by
unifying g1 and g2 , only if g1 is a variable which does not occur in vars(g2 ) (see
rule (geq) above).
Thus, if a goal g is safe in P , then the evaluation of g according to our operational
semantics agrees with the one which uses LD-resolution in the following sense: if
g is safe in P , then there exists a set A of answer substitutions such that P ⊢
g 7→ A holds iff: (i) all LD-derivations starting from g and using P are finite
(that is, g universally terminates in P (Apt 1997; Vasak and Potter 1986)), and
(ii) A is the set of the computed answer substitutions obtained by LD-resolution.
Point (i) follows from the fact that in our operational semantics, the evaluation of
a disjunction of goals (see the (or) rule) requires the evaluation of each disjunct.
Thus, in order to compute the relation P ⊢ g 7→ A in the case where g is safe in P ,
we can use any ordinary Prolog system which implements LD-resolution.
Notice that, given a program P and a goal g, if the LD-tree has an infinite LDderivation, then no set A of answer substitutions exists such that P ⊢ g 7→ A. In
particular, for the program P = {p(0) ←, p(X ) ← p(X )} no A exists such that
P ⊢ p(X ) 7→ A, while the set of computed answer substitutions constructed by
LD-resolution for the program P and the goal p(X ) is the singleton consisting of
the substitution {X /0} only.
It may also be the case that a goal g is not safe in a program P (thus, there
exists no set A of answer substitutions such that P ⊢ g 7→ A holds) while, by
using LD-resolution, g succeeds or fails in P . For instance, for any program and for
any two distinct nullary predicates p and q, (i) the goal p = p is not safe, while it
succeeds by using LD-resolution and (ii) the goal p = q is not safe, while it fails by
using LD-resolution.
We recall that our interpretation of goal equality is motivated by the fact that
we want the operational semantics to be preserved by program transformations
and, in particular, by unfolding. As already shown in the Introduction, unfortunately, unfolding does not preserve the operational semantics based on ordinary
LD-resolution.
The following Proposition 1 establishes an important property of our operational
semantics. This property is useful for the proof the correctness results in Section 6
(see Theorem 2). The proof of this proposition is similar to the one in the case
of LD-resolution for definite programs (see, for instance, (Lloyd 1987)) and will be
omitted.
Proposition 1
Let P be a program, g be an ordinary goal, and A be a set of substitutions such
that P ⊢ g 7→ A. Then, for all ϑ ∈ Subst, the following hold:
(i) gϑ terminates, that is, either P ⊢ gϑ ↓ true or P ⊢ gϑ ↓ false, and
(ii.1) P ⊢ gϑ ↓ true iff there exists α ∈ A such that gϑ is an instance of gα, and
(ii.2) P ⊢ gϑ ↓ false iff it does not exist α ∈ A such that gϑ is an instance of gα.

16

A. Pettorossi and M. Proietti

Let us conclude this section by introducing the notions of refinement and equivalence
between programs which we will use in Section 6 to state the weak and strong
correctness of the program transformations that can be realized by applying our
transformation rules. These rules are presented in the next section.
Definition 1 (Refinement and Equivalence)
Given two programs P1 and P2 , we say that P2 is a refinement of P1 , written
P1 ⊑ P2 , iff for every ordinary goal g and for every A ∈ P(Subst), if P1 ⊢ g 7→ A
then there exists B ∈ P(Subst) such that:
(1) P2 ⊢ g 7→ B and
(2) A and B are equally general with respect to g.
We say that P1 is equivalent to P2 , written P1 ≡ P2 , iff P1 ⊑ P2 and P2 ⊑ P1 .
Remark 1
Recall that Condition (2) can be written as mostgen(A, g) ≈ mostgen(B , g). In this
sense we will say that if P1 ⊑ P2 and the ordinary goal g terminates in P1 , then
the most general answer substitutions for g are the same in P1 and P2 , modulo
variable renaming.

Remark 2
P1 ⊑ P2 implies that, for every ordinary goal g,
- if g succeeds in P1 then g succeeds in P2 , and
- if g fails in P1 then g fails in P2 .



Theorem 2 stated in Section 6 shows that, if from program P1 we derive program
P2 by using our transformation rules and suitable conditions hold, then P1 ⊑ P2 . In
this case we say that the transformation is weakly correct. If additional conditions
hold, then we may have that P1 ≡ P2 and we say that the transformation is strongly
correct.
In Section 6 we will also show that our transformation rules preserve safety, that
is, if from program P1 we derive program P2 by using the transformation rules and
goal g is safe in P1 , then goal g is safe also in P2 .
5 The Transformation Rules
In this section we present the transformation rules for our extended logic language.
We assume that starting from an initial program P0 we have constructed the transformation sequence P0 , . . . , Pi (Pettorossi and Proietti 1994; Tamaki and Sato 1984).
By an application of a transformation rule, from program Pi we derive a new program Pi+1 .
Rule R1 (Definition Introduction)
We derive the new program Pi+1 by adding to program Pi a new clause, called a
definition, of the form:
newp(V1 , . . . , Vm ) ← g

Transformations of Logic Programs with Goals as Arguments

17

where: (i) newp is a new non-primitive predicate symbol not occurring in any program of the sequence P0 , . . . , Pi , (ii) the non-primitive predicate symbols occurring
in g are defined in P0 , and (iii) V1 , . . . , Vm are some of (possibly all) the distinct
variables occurring in g.
The set of all definitions introduced during the transformation sequence P0 , . . . , Pi ,
is denoted by Def i . Thus, Def 0 = ∅.
Rule R2 (Unfolding)
Let c1 : h ← body[p(u1 , . . . , um )] be a renamed apart clause in program Pi where
p is a non-primitive predicate symbol. Let d : p(V1 , . . . , Vm ) ← g be a clause in
P0 ∪ Def i . By unfolding c1 w.r.t. p(u1 , . . . , um ) using d we derive the new clause
c2 : h ← body[g{V1 /u1 , . . . , Vm /um }]. We derive the new program Pi+1 by replacing
in program Pi clause c1 by clause c2 .
Rule R3 (Folding)
Let c1 : h ← body[gϑ] be a renamed apart clause in program Pi and let d :
p(V1 , . . . , Vm ) ← g be a clause in Def i . Suppose that, for every local variable
V of g in d , we have that:
(1) V ϑ is a local variable of gϑ in c1 , and
(2) the variable V ϑ does not occur in W ϑ, for any variable W occurring in g
and different from V .
Then, by folding c1 using d we derive the new clause c2 : h ← body[p(V1 , . . . , Vm )ϑ].
We derive the new program Pi+1 by replacing in program Pi clause c1 by clause c2 .
In order to present the goal replacement rule (see rule R4 below) we introduce
the notion of replacement law. Basically, a replacement law denotes two goals which
can be replaced one for the other in the body of a clause. We have two kinds of
replacement laws: the weak and the strong replacement laws, which ensure weak
and strong correctness, respectively (see the end of this section for an informal
discussion and Section 6 for a formal proof of this fact).
First we need the following definition.
Definition 2 (Depth of a Deduction Tree)
Let τ be a finite deduction tree and let m be the maximal number of applications
of the (at) rule in a root-to-leaf path of τ . Then we say that τ has depth m.
Let π be a proof for P ⊢ g 7→ A, for some program P , goal g, and set A of
substitutions, and let m be the depth of π. If A = ∅ we write P ⊢ g ↓m false;
otherwise, if A 6= ∅ we write P ⊢ g ↓m true.
Recall that, given a program P and a goal g, if for some set A of substitutions
there exists a proof for P ⊢ g 7→ A, then the proof is unique up to isomorphism.
In particular, given a proof for P ⊢ g 7→ A1 and a proof for P ⊢ g 7→ A2 , they
have the same depth.
Definition 3 (Replacement Laws)
Let P be a program, let g1 and g2 be two goals, and let V be a set of variables.
(i) The relation P ⊢ ∀V (g1 −→ g2 ) holds iff for every goal context g[ ] such that
vars(g[ ]) ∩ vars(g1 , g2 ) ⊆ V , and for every b ∈ {true, false}, we have that:

18

A. Pettorossi and M. Proietti

if P ⊢ g[g1 ] ↓ b then P ⊢ g[g2 ] ↓ b.

(†)

>

(ii) The relation P ⊢ ∀V (g1 −→ g2 ), called a weak replacement law, holds iff
for every goal context g[ ] such that vars(g[ ]) ∩ vars(g1 , g2 ) ⊆ V , and for every
b ∈ {true, false}, we have that:
if P ⊢ g[g1 ] ↓m b then P ⊢ g[g2 ] ↓n b with m ≥ n.

(††)

>

(iii) The relation P ⊢ ∀V (g1 ←→ g2 ), called a strong replacement law, holds iff
>

P ⊢ ∀V (g1 −→ g2 ) and P ⊢ ∀V (g2 −→ g1 ).
= g ) to mean that the strong replacement laws
(iv) We write P ⊢ ∀V (g1 ←→
2
>

>

P ⊢ ∀V (g1 −→ g2 ) and P ⊢ ∀V (g2 −→ g1 ) hold.
>

>

If V = ∅ then P ⊢ ∀V (g1 −→ g2 ) is also written as P ⊢ g1 −→ g2 . If V =
>

>

{V1 , . . . , Vn } then P ⊢ ∀V (g1 −→ g2 ) is also written as P ⊢ ∀V1 , . . . , Vn (g1 −→ g2 ).
>

>

If V = vars(g1 , g2 ) then P ⊢ ∀V (g1 −→ g2 ) is also written as P ⊢ ∀ (g1 −→ g2 ).
A few comments on the above Definition 3 are now in order.
(1) In the relation P ⊢ ∀V (g1 −→ g2 ) we have used the set V of universally
quantified variables as a notational device for indicating that when we replace g1
by g2 in a clause h ← body [g1 ], the variables in common between h ← body[ ] and
(g1 , g2 ) are those in V (see the goal replacement rule R4 below). Thus, vars(g1 )− V
is the set of the local variables of g1 in h ← body[g1 ] and vars(g2 ) − V is the set of
the local variables of g2 in h ← body [g2 ].
(2) Implication (††) implies Implication (†).
(3) Every strong replacement law is also a weak replacement law.
= g ) then there exists A ∈ P(Subst) such that P ⊢ g 7→ A
(4) If P ⊢ ∀V (g1 ←→
2
1
1
1
has a proof of depth m iff there exists A2 ∈ P(Subst) such that P ⊢ g2 7→ A2 has
a proof of depth m. Moreover, if both proofs exist, A1 = ∅ iff A2 = ∅.
The properties listed in the next proposition follow directly from Definition 3.
Proposition 2
Let P be a program, let g1 and g2 be goals, and let V be a set of variables.
(i) P ⊢ ∀V (g1 −→ g2 ) holds iff for every goal context g[ ] such that vars(g[ ]) ∩
vars(g1 , g2 ) ⊆ V , P ⊢ ∀W (g[g1 ] −→ g[g2 ]) holds, where W = V ∪ vars(g[ ]).
(ii) P ⊢ ∀V (g1 −→ g2 ) holds iff P ⊢ ∀W (g1 −→ g2 ) holds, where W = V ∩
vars(g1 , g2 ).
(iii) P ⊢ ∀V (g1 −→ g2 ) holds iff for every W ⊆ V , P ⊢ ∀W (g1 −→ g2 ) holds.
(iv) P ⊢ ∀V (g1 −→ g2 ) holds iff for every substitution ϑ such that vars(ϑ) ∩
vars(g1 , g2 ) ⊆ V , P ⊢ ∀W (g1 ϑ −→ g2 ϑ) holds, where W = vars(V ϑ).
(v) P ⊢ ∀V (g1 −→ g2 ) holds iff for every renaming substitution ρ such that
vars(ρ) ∩ V = ∅, P ⊢ ∀V (g1 ρ −→ g2 ρ) holds.
>

The properties obtained from (i) – (v) by replacing −→ by −→ are also true.
We will refer to them as Properties (i′ ) – (v′ ), respectively.

Transformations of Logic Programs with Goals as Arguments

19

Definition 4
>

We say that a weak replacement law P ⊢ ∀V (g1 −→ g2 ) (or a strong replacement
>

law P ⊢ ∀V (g1 ←→ g2 )) preserves safety iff for every goal context g[ ] such that
vars(g[ ]) ∩ vars(g1 , g2 ) ⊆ V , we have that:
if g[g1 ] is safe in P then g[g2 ] is safe in P .
Rule R4 (Goal Replacement )
Let c1 : h ← body[g1 ] be a clause in program Pi and let g2 be a goal such that:
(i) all non-primitive predicate symbols occurring in g1 or g2 are defined in P0 , and
>

>

either (ii.1) P0 ⊢ ∀V (g1 −→ g2 ), or (ii.2) P0 ⊢ ∀V (g1 ←→ g2 ), where V =
vars(h, body [ ]) ∩ vars(g1 , g2 ).
By goal replacement we derive the new clause c2 : h ← body[g2 ], and we derive the
new program Pi+1 by replacing in program Pi clause c1 by clause c2 .
In case (ii.1) we say that the goal replacement is based on a weak replacement law.
In case (ii.2) we say that the goal replacement is based on a strong replacement
law. We say that the goal replacement preserves safety iff it is based on a (weak or
strong) replacement law which preserves safety.
>

>

Implication (††) of Definition 3 makes −→ and ←→ to be improvement relations
in the sense of (Sands 1996). As stated in Theorem 2 of Section 6, Implication (††)
is required for ensuring the weak correctness of a goal replacement step, while Implication (†) of Definition 3 does not suffice. This fact is illustrated by the following
example.
Example 6
Let us consider the program P1 :
1. p ← q
2. q ←
We have that P1 ⊢ q −→ p and thus, Implication (†) holds by taking g1 to be q, g2
to be p, and g[ ] to be the empty goal context. The replacement of q by p in clause
1 produces the following program P2 :
1*. p ← p
2. q ←
This replacement is not an application of rule R4, because Implication (††) does not
hold. (Indeed, we have that the depth of the proof for P1 ⊢ q 7→ {ε} is smaller than
the depth of the proof for P1 ⊢ p 7→ {ε}). The transformation from program P1 to
program P2 is not weakly correct (nor strongly correct), because p succeeds in P1 ,
while p does not terminate in P2 , and thus, it is not the case that P1 ⊑ P2 .

The reader may check that, for any program P , and goals g, g1 , g2 , and g3 , we
have the following replacement laws. It can be shown that these replacement laws
preserve safety.

20

A. Pettorossi and M. Proietti

1. Boolean Laws:
= g)
P ⊢ ∀ (g ∧ true ←→
= g)
P ⊢ ∀ (true ∧ g ←→
>

P ⊢ ∀ (true ∨ g −→ true)
>

P ⊢ ∀ (g ∧ false −→ false)
= false)
P ⊢ ∀ (false ∧ g ←→
= g)
P ⊢ ∀ (false ∨ g ←→

>

P ⊢ ∀ (g ∧ g −→ g)
= g)
P ⊢ ∀ (g ∨ g ←→
= g ∨g )
P ⊢ ∀ (g1 ∨ g2 ←→
2
1
P ⊢ ∀ ((g1 ∧ g2 ) ∨ (g1 ∧ g3 )
P ⊢ ∀ ((g1 ∧ g2 ) ∨ (g3 ∧ g2 )

= g ∧ (g ∨ g ))
←→
1
2
3
= (g ∨ g ) ∧ g )
←→
1
3
2
>

P ⊢ ∀ ((g1 ∨ g2 ) ∧ (g1 ∨ g3 ) −→ g1 ∨ (g2 ∧ g3 ))

In the following replacement laws 2.1 and 2.2, according to our conventions, V
stands for either an individual variable or a goal variable, and u stands for either a
term or a goal, respectively.
2.1 Introduction and elimination of equalities:
= ((V = u) ∧ g[V ]))
P ⊢ ∀U (g[u] ←→
where U = vars(g[u]) and V 6∈ U .
2.2 Rearrangement of equalities:
= ((V = u) ∧ g[g ]))
P ⊢ ∀U (g[(V = u) ∧ g1 ] ←→
1
where U = vars(g[g1 ], u) and V 6∈ U .
When referring to goal variables, laws 2.1 and 2.2 will also be called ‘Introduction
and elimination of goal equalities’ and ‘Rearrangement of goal equalities’, respectively.
3. Rearrangement of term equalities:
>

P ⊢ ∀ (g ∧ (t1 = t2 ) −→ (t1 = t2 ) ∧ g)
4. Clark Equality Theory (also called CET, see (Lloyd 1987)):
= eq )
P ⊢ ∀X (eq1 ←→
if CET ⊢ ∀X (∃Y eq 1 ↔ ∃Z eq 2 )
2
where: (i) eq1 and eq2 are goals constructed by using true, false, term equalities,
conjunctions, and disjunctions, and (ii) Y = (vars(eq1 )−X ) and Z = (vars(eq2 )−X ).
Notice that, for some program P and for some goals g, g1 , g2 , and g3 , the following
do not hold:
∀ (true −→ true ∨ g)
∀ (false −→ g ∧ false)
∀ ((t1 = t2 ) ∧ g −→ g ∧ (t1 = t2 ))
∀ (g1 ∨ (g2 ∧ g3 ) −→ (g1 ∨ g2 ) ∧ (g1 ∨ g3 ))
∀V (g2 [g1 ] −→ g2 [G] ∧ (G = g1 ))
where V = vars(g2 [g1 ]) and G 6∈ V
∀V (g[(G = g1 ) ∧ g2 ] −→ (G = g1 ) ∧ g[g2 ])
where V = (vars(g[g2 ], g1 ) − {G}) and G ∈ vars(g[ ], g1 )
P ⊢ ∀ (g[(G = g1 ) ∧ g2 ] −→ (G = g1 ) ∧ g[g2 ])
where G 6∈ vars(g[ ], g1 )
P
P
P
P
P
P

⊢
⊢
⊢
⊢
⊢
⊢

Let us now make some remarks on the goal replacement rule.
In the Weak Correctness part of Theorem 2 (see Section 6) we will prove that if
program P2 is derived from program P1 by an application of the goal replacement
rule based on a weak replacement law, then P2 is a refinement of P1 , that is,
P1 ⊑ P2 . Thus, there may be some ordinary goal g which either succeeds or fails
in P2 , while g does not terminate in P1 , as shown by the following example.

Transformations of Logic Programs with Goals as Arguments

21

Example 7
Let us consider the following two programs P1 and P2 , where P2 is derived from
P1 by applying the goal replacement rule based on the weak (and not strong)
>

replacement law P1 ⊢ ∀ (true ∨ g −→ true):
P1 :

p ← true ∨ q
q ←q

P2 :

p ← true
q ←q

We have that p does not terminate in P1 and p succeeds in P2 .
Next, let us consider the following programs:
P3 :

p ← q ∧ false
q ←q

P4 :

p ← false
q ←q

where P4 is derived from P3 by a goal replacement rule based on a weak (and
>

not strong) replacement law P ⊢ ∀ (g ∧ false −→ false). We have that p does not
terminate in P3 , while p fails in P4 .

In the Strong Correctness part of Theorem 2 we will prove that if program P2 is
derived from program P1 by an application of the goal replacement rule based on
a strong replacement law, then P1 and P2 are equivalent, that is P1 ≡ P2 . Thus, in
particular, for any goal g, g terminates in P1 iff g terminates in P2 .
Moreover, in Theorem 3 of Section 6 we will prove that if program P2 is derived
from program P1 by goal replacements which preserve safety, then every goal which
is safe in P1 , is safe also in P2 .

6 Correctness of Program Transformations
The unrestricted use of our rules for transforming programs may allow the construction of incorrect transformation sequences, as the following example shows.
Example 8
Let us consider the following initial program:
P0 :

p←q
q←

By two definition introduction steps, we get:
P1 :

p←q
q←
newp1 ← q
newp2 ← q

By three folding steps, from program P1 we get the final program:
P2 :

p ← newp1
q←
newp1 ← newp2
newp2 ← newp1

We have that p succeeds in P0 , while p does not terminate in P2 .



22

A. Pettorossi and M. Proietti

In this section we will present some conditions which ensure that every transformation sequence P0 , . . . , Pk constructed by using our rules, is:
(i) weakly correct, in the sense that P0 ∪ Defk ⊑ Pk (see Point (1) of Theorem 2),
(ii) strongly correct, in the sense that P0 ∪ Defk ≡ Pk (see Point (2) of Theorem 2),
(iii) preserves safety, in the sense that, for every goal g, if g is safe in P0 ∪ Def k
then g is safe also in Pk (see Theorem 3).
Similarly to other correctness results presented in the literature (Bossi and Cocco 1994;
Pettorossi and Proietti 1994; Sands 1996; Tamaki and Sato 1984), some of the conditions which ensure (weak or strong) correctness, require that the transformation
sequences are constructed by performing suitable unfolding steps before performing
folding steps.
In particular, Theorem 2 below ensures the (weak or strong) correctness of a
given transformation sequence in the case where this sequence is admissible, that
is, it is constructed by performing parallel leftmost unfoldings (see Definition 5) on
all definitions which are used for performing subsequent foldings.
In order to present our correctness results it is convenient to consider admissible transformation sequences which are ordered, that is, transformation sequences
constructed by:
(i) first, applying the definition introduction rule,
(ii) then, performing parallel leftmost unfoldings of the definitions that are used for
subsequent foldings, and
(iii) finally, performing unfoldings, foldings, and goal replacements in any order.
Thus, an ordered, admissible transformation sequence has all its definition introductions performed at the beginning, and it can be written in the form P0 , . . . , P0 ∪
Def k , . . . , Pk , where Def k is the set of all definitions introduced during the entire
transformation sequence P0 , . . . , P0 ∪ Def k , . . . , Pk . By Proposition 3 below we may
assume, without loss of generality, that all admissible transformation sequences are
ordered.
In order to prove that an admissible transformation sequence is weakly correct
(see Point (1) of Theorem 2), we proceed as follows.
(i) In Lemma 1 we consider a generic transformation by which we derive a program
NewP from a program P by replacing the bodies of the clauses of P by new bodies.
We show that, if these body replacements can be viewed as goal replacements based
on weak replacement laws, then the transformation from P to NewP preserves
successes and failures, that is,
- if a goal g succeeds in P then g succeeds in NewP , and
- if a goal g fails in P then g fails in NewP .
(ii) Then, in Lemma 2 we prove that in an ordered, admissible transformation
sequence P0 , . . . , P0 ∪ Def k , . . . , Pk , any application of the unfolding, folding, and
goal replacement rule is an instance of the generic transformation considered in
Lemma 1, that is, it consists in the replacement of the body of a clause by a new
body, and this replacement can be viewed as a goal replacement based on a weak
replacement law.

Transformations of Logic Programs with Goals as Arguments

23

(iii) Thus, by using Lemmata 1 and 2 we get Point (1) of Theorem 1. In particular,
we have that in any admissible transformation sequence P0 , . . . , P0 ∪ Def k , . . . , Pk ,
successes and failures are preserved, that is:
- if a goal g succeeds in P0 ∪ Def k then g succeeds in Pk , and
- if a goal g fails in P0 ∪ Def k then g fails in Pk .
(iv) Finally, Proposition 1 allows us to infer the preservation of most general answer
substitutions from the preservation of successes and failures. Indeed, by Proposition 1 and Point (1) of Theorem 1 we prove that if an ordinary goal g succeeds in
P0 ∪ Def k then the set of answer substitutions for g in P0 ∪ Def k and the set of
answer substitutions for g in Pk are equally general.
According to Definition 1, Points (iii) and (iv) mean that P0 ∪ Def k ⊑ Pk , that is,
the ordered, admissible transformation sequence P0 , . . . , P0 ∪Def k , . . . , Pk is weakly
correct (see Point (1) of Theorem 2).
In order to prove that an admissible transformation sequence is strongly correct
(see Point (2) of Theorem 2), we make the additional hypothesis that all goal
replacements performed during the construction of the transformation sequence
are based on strong replacement laws. Analogously to the proof of weak correctness
which is based on Lemmata 1 and 2, the proof of strong correctness is based on
Lemmata 3 and 4 which we give below. By using these lemmata, we prove Point (2)
of Theorem 1, that is:
- if a goal g succeeds in Pk then g succeeds in P0 ∪ Def k , and
- if a goal g fails in Pk then g fails in P0 ∪ Def k .
Finally, by Proposition 1 and Theorem 1, we prove that any admissible transformation sequence in which all goal replacements are based on strong replacement
laws, is strongly correct (see Point (2) of Theorem 2), that is, P0 ∪ Def k ≡ Pk .
Now let us formally define the notions of parallel leftmost unfolding of a clause, admissible transformation sequence, and ordered admissible transformation sequence
as follows.
Definition 5
Let c be a clause in a program P . If c is of the form:
p(V1 , . . . , Vm ) ← (a1 ∧ g1 ) ∨ . . . ∨ (as ∧ gs )
where a1 , . . . , as are atoms with non-primitive predicates, g1 , . . . , gs are goals, and
s > 0, then the parallel leftmost unfolding of clause c in program P is the program Q obtained from P by applying s times the unfolding rule w.r.t. a1 , . . . , as ,
respectively.
If clause c is not of the form indicated in Definition 5 above, then the parallel
leftmost unfolding of c is not defined.
Definition 6
A transformation sequence P0 , . . . , Pk is said to be admissible iff for every h, with
0 ≤ h < k , if Ph+1 has been obtained from Ph by folding clause c using clause d ,
then there exist i, j , with 0 ≤ i < j ≤ k , such that d ∈ Pi and Pj is obtained from
Pi by parallel leftmost unfolding of d .

24

A. Pettorossi and M. Proietti

Definition 7
An admissible transformation sequence P0 , . . . , Pk is said to be ordered iff it is of the
form P0 , . . . , Pi , . . . , Pj , . . . , Pk , where: (i) the sequence P0 , . . . , Pi is constructed by
applying the definition introduction rule, (ii) the sequence Pi , . . . , Pj is constructed
by parallel leftmost unfolding of all definitions which have been introduced during
the sequence P0 , . . . , Pi and are used for folding during the sequence Pj , . . . , Pk ,
and (iii) the definition introduction rule is never applied in the sequence Pj , . . . , Pk .
Given an ordered, admissible transformation sequence P0 , . . . , Pi , . . . , Pj , . . . , Pk ,
the set of definitions introduced during P0 , . . . , Pi is the same as the set of definitions
introduced during the entire sequence P0 , . . . , Pk , and thus, in the above Definition 7
we have that Pi is P0 ∪ Def k .
An admissible transformation sequence P0 , . . . , Pk which is ordered, is also denoted by P0 , . . . , Pi , . . . , Pj , . . . , Pk , where we explicitly indicate the program Pi
after the introduction of the definitions, and the program Pj after the parallel
leftmost unfolding steps.
Proposition 3
For any admissible transformation sequence P0 , . . . , Pn there exists an ordered,
admissible transformation sequence P0 , . . . , Pi , . . . , Pj , . . . , Pk such that Pn = Pk
and Def n = Def k .
Now, in order to prove the correctness of transformation sequences, we state the following Lemmata 1, 2, 3, and 4, whose proofs are given in the Appendix. As already
mentioned, these Lemmata 1, 2, 3, and 4 will allow us to show that, under suitable
conditions, for every admissible transformation sequence P0 , . . . , Pk , (i) successes
and failures are preserved (see Theorem 1 below), and (ii) weak correctness holds
(that is, P0 ∪ Def k ⊑ Pk ) or strong correctness holds (that is, P0 ∪ Def k ≡ Pk ) (see
Theorem 2 below).
Lemma 1
Let P and NewP be programs of the form:
P:

hd1 ← bd1
..
.
hds ← bds

NewP :

hd1 ← newbd 1
..
.
hds ← newbd s
>

For r = 1, . . . , s, let Vr be vars(hdr ) and suppose that P ⊢ ∀Vr (bdr −→ newbd r ).
Then, for every goal g and for every b ∈ {true, false}, we have that:
if P ⊢ g ↓m b then NewP ⊢ g ↓n b with m ≥ n.
Lemma 2
Let us consider an ordered, admissible transformation sequence P0 , . . . , Pi , . . . ,
Pj , . . . , Pk , where Pi is P0 ∪ Def k .
(i) For h = i, . . . , j −1 and for any pair of clauses c1 : hd ← bd in program Ph and
c2 : hd ← newbd in program Ph+1 , such that c2 is derived from c1 by applying the
unfolding rule, we have that:

Transformations of Logic Programs with Goals as Arguments

25

>

Pi ⊢ ∀V (bd −→ newbd )
where V = vars(hd ). (Notice that the unfolding rule does not change the heads of
the clauses.)
(ii) For h = j , . . . , k −1 and for any pair of clauses c1 : hd ← bd in program Ph and
c2 : hd ← newbd in program Ph+1 , such that c2 is derived from c1 by applying the
unfolding, or folding, or goal replacement rule, we have that:
>
Pj ⊢ ∀V (bd −→ newbd )
where V = vars(hd ). (Notice that the unfolding, folding, and goal replacement
rules do not change the heads of the clauses.)
Lemma 3
Let P and NewP be programs of the form:
P : hd1 ← bd1
NewP :
..
.

hd1 ← newbd1
..
.

hds ← bds
hds ← newbds
For r = 1, . . . , s, let Vr be vars(hdr ) and suppose that P ⊢ ∀Vr (newbdr −→ bdr ).
Then, for every goal g and for every b ∈ {true, false}, we have that if NewP ⊢ g ↓ b
then P ⊢ g ↓ b.
Notice that Lemma 3 is a partial converse of Lemma 1. These two lemmata imply that if we derive a program NewP from a program P by replacing the bodies
of the clauses of P by new bodies, and these body replacements are goal replacements based on strong replacement laws, then every goal terminates in NewP iff it
terminates in P .
Lemma 4
Let us consider a transformation sequence P0 , . . . , Pk and let Def k be the set of
definitions introduced during that sequence. For h = 0, . . . , k −1 and for any pair
of clauses c1 : hd ← bd in program Ph and c2 : hd ← newbd in program Ph+1 , such
that c2 is derived from c1 by applying the unfolding rule, or the folding rule, or the
goal replacement rule based on strong replacement laws, we have that:
P0 ∪ Def k ⊢ ∀V (newbd −→ bd )
where V = vars(hd ).
In particular, as a consequence of Lemma 2 and Lemma 4, we have that in any
ordered, admissible transformation sequence the unfolding and folding rules can be
viewed as goal replacements based on strong replacement laws.
The following theorem states that for every admissible transformation sequence
successes and failures are preserved.
Theorem 1 (Preservation of Successes and Failures)
Let P0 , . . . , Pk be an admissible transformation sequence and let Def k be the set
of definitions introduced during that sequence. Then for every goal g and for every
b ∈ {true, false}, we have that:
(1) if P0 ∪ Def k ⊢ g ↓m b then Pk ⊢ g ↓n b with m ≥ n, and
(2) if all applications of the goal replacement rule are based on strong replacement
laws and Pk ⊢ g ↓ b, then P0 ∪ Def k ⊢ g ↓ b.

26

A. Pettorossi and M. Proietti

Proof of Theorem 1
See Appendix. The proof of (1) is based on Proposition 3 and Lemmata 1 and 2,
and the proof of (2) is based on Proposition 3 and Lemmata 3 and 4.
The following theorem establishes the weak correctness and, under suitable conditions, the strong correctness of admissible transformation sequences.
Theorem 2 (Correctness Theorem)
Let P0 , . . . , Pk be an admissible transformation sequence. Let Def k be the set of
definitions introduced during that sequence. We have that:
(1) (Weak Correctness) P0 ∪ Def k ⊑ Pk , that is, Pk is a refinement of P0 ∪ Def k ,
and
(2) (Strong Correctness) if all applications of the goal replacement rule are based on
strong replacement laws then P0 ∪ Def k ≡ Pk , that is, Pk is equivalent to P0 ∪ Def k .
Proof of Theorem 2
See Appendix. The proof of (1) is based on Proposition 1 and Theorem 1 (Point 1),
and the proof of (2) is based on Proposition 1 and Theorem 1 (Points 1 and 2).
The following two examples show that in the statement of Theorem 2 we cannot
drop the admissibility condition. Indeed, in these examples we construct transformation sequences which are not admissible and not weakly correct.
Example 9
Let us construct a transformation sequence as follows. The initial program is:
P0 :

p ←p∧q
q ← false

By definition introduction we get:
P1 :

p ←p∧q
q ← false
newp ← false ∧ p

Then we perform the unfolding of newp ← false ∧ p w.r.t. p. (Notice that this is
not a parallel leftmost unfolding.) We get:
P2 :

p ←p∧q
q ← false
newp ← false ∧ p ∧ q

By folding we get the final program:
P3 :

p ←p∧q
q ← false
newp ← newp ∧ q

We have that newp fails in P0 ∪ Def3 (that is, P1 ), while newp does not terminate
in P3 .


Transformations of Logic Programs with Goals as Arguments

27

Example 10
Let us construct a transformation sequence as follows. The initial program is:
P0 :

p ← false
q ← true ∨ q

By definition introduction we get:
P1 :

p ← false
q ← true ∨ q
newp ← p ∨ (p ∧ q)

Then we perform the unfolding of newp ← p ∨ (p ∧ q) w.r.t. q. (Notice that this is
not a parallel leftmost unfolding.) We get:
P2 :

p ← false
q ← true ∨ q
newp ← false ∨ (p ∧ (true ∨ q))

By goal replacement based on boolean laws we get:
P3 :

p ← false
q ← true ∨ q
newp ← p ∨ (p ∧ q)

By folding we get the final program:
P4 :

p ← false
q ← true ∨ q
newp ← newp

We have that newp fails in P0 ∪ Def4 (that is, P1 ), while newp does not terminate
in P4 .

Finally, the following theorem states that a (possibly not admissible) transformation sequence preserves safety, if all goal replacements performed during that
sequence preserve safety.
Theorem 3 (Preservation of Safety)
Let P0 , . . . , Pk be a transformation sequence and let Def k be the set of definitions
introduced during that sequence. Let us also assume that all applications of the goal
replacement rule R4 preserve safety. Then, for every goal g, if g is safe in P0 ∪ Def k
then g is safe in Pk .
Proof of Theorem 3
See Appendix. The proof is based on Lemmata 5 and 6 given in the Appendix.
We end this section by making some comments about our correctness results.
Let us consider an admissible transformation sequence P0 , . . . , Pk , during which we
introduce the set Defk of definitions. Then, by Point (1) of Theorem 1 program
Pk may be more defined than program P0 ∪ Defk in the sense that there may be
a goal which terminates (i.e., succeeds or fails) in Pk , while it does not terminate
in P0 ∪ Defk . This ‘increase of termination’ is often desirable when transforming
programs and it may be achieved by goal replacements which are not based on
strong replacement laws (see, for instance, Example 7 in Section 5).

28

A. Pettorossi and M. Proietti

Now suppose that during the construction of the admissible transformation sequence P0 , . . . , Pk all applications of the goal replacement rule are based on strong
replacement laws. Then, by Theorem 1 we have that for all goals g, g terminates in
P0 ∪ Defk iff g terminates in Pk . However, safety may be not preserved, in the sense
that there may be a goal g which is safe in P0 ∪ Defk (but g neither succeeds nor
fails in P0 ∪ Defk ) and g is not safe in Pk (or vice versa), as shown by the following
example.
Example 11
Let us consider the following two programs P1 and P2 :
P1 :

p←p

P2 :

p←G

Program P2 is derived from P1 by applying the goal replacement rule based on the
= G, which does not preserve safety. We have
strong replacement law P1 ⊢ p ←→
that p is safe, p does not terminate in P1 , and p is not safe in P2 . Notice that the
= G trivially holds because, for any b ∈ {true, false},
replacement law P1 ⊢ p ←→
P1 ⊢ p ↓ b does not hold and P1 ⊢ G ↓ b does not hold.

In order to ensure that if g is safe in P1 then g is safe in P2 , it is enough to
use replacement laws which preserve safety (see Theorem 3). Indeed, unfolding and
folding always preserve safety (see Lemma 6 in the Appendix).
We have not presented any result which guarantees that if a goal is safe in the
final program Pk then it is safe in the program P0 ∪Defk . This result could have been
achieved by imposing further restrictions on the goal replacement rule. However,
we believe that this ‘inverse preservation of safety’ is not important in practice,
because usually we start from an initial program where all goals of interest are safe
and we want to derive a final program where those goals of interest are still safe. In
particular, if in the transformation sequence P0 , . . . , Pk the initial program P0 is an
ordinary program, then every ordinary goal g is safe in P0 and, by Theorem 3, we
have that g is safe also in Pk . Thus, as discussed in Section 4, we can use ordinary
implementations of LD-resolution to compute the relation Pk |= g 7→ A.
Notice also that, if P0 ∪Def k ⊑ Pk and an ordinary goal g terminates in P0 , then g
has the same most general answer substitutions in P0 ∪Def k and Pk , modulo variable
renaming (see Point (i) of Remark 1 at the end of Section 4). However, the set of all
answer substitutions may not be preserved, and in particular, there are programs
P1 and P2 such that P1 ⊑ P2 and, for some goal g, we have that P1 ⊢ g 7→ A1
and P2 ⊢ g 7→ A2 , where A1 and A2 have different cardinality, as shown by the
following example adapted from (Bossi et al. 1992). A similar property holds if we
assume that P1 ≡ P2 , instead of P1 ⊑ P2 .
Example 12
Let us consider the following two programs P1 and P2 , where P2 is derived from
P1 by applying the goal replacement rule based on the weak replacement law
>
P ⊢ ∀ (g ∧ g −→ g), which holds for every program P and and goal g:
P1 :

p(X ) ← q(X ) ∧ q(X )
q(X ) ← X = f (a, Z )
q(X ) ← X = f (Y , a)

P2 :

p(X ) ← q(X )
q(X ) ← X = f (a, Z )
q(X ) ← X = f (Y , a)

Transformations of Logic Programs with Goals as Arguments

29

We have that:
P1 ⊢ p(X ) 7→ {{X /f (a, Z )}, {X /f (a, a)}, {X /f (Y , a)}}, and
P2 ⊢ p(X ) 7→ {{X /f (a, Z )}, {X /f (Y , a)}}.



The above example shows that, if during program transformation we want to preserve the set of answer substitutions, then we should not apply goal replacements
>
based on the replacement law P ⊢ ∀ (g ∧ g −→ g) which, however, may be useful
for avoiding the computation of redundant goals and improving program efficiency.
Another replacement law which is very useful in many examples of program
transformation, is the law which expresses the functionality of a predicate. For
instance, in the Deepest example of Section 2, the depth predicate is functional
with respect to its first argument in the sense that, for every goal context g[ ], the
following replacement law holds:
>

Deepest ⊢ ∀ (depth(T , X ) ∧ g[depth(T , Y )] ←→ depth(T , X ) ∧ g[X = Y ]).
The following example, similar to Example 12, shows that in general the functionality law does not preserve the set of answer substitutions.
Example 13
Let us consider the following two programs P1 and P2 , where P2 is derived from
P1 by applying the goal replacement rule based on the (strong) replacement law
>

P1 ⊢ ∀ (q(X , Y ) ∧ q(X , Z ) ←→ q(X , Y ) ∧ Y = Z ):
P1 :

p(X ) ← q(X , Y ) ∧ q(X , Z )
q(f (a, Z ), b) ←
q(f (Y , a), b) ←

P2 :

p(X ) ← q(X , Y ) ∧ Y = Z
q(f (a, Z ), b) ←
q(f (Y , a), b) ←

As in Example 12, we have that:
P1 ⊢ p(X ) 7→ {{X /f (a, Z )}, {X /f (a, a)}, {X /f (Y , a)}}
P2 ⊢ p(X ) 7→ {{X /f (a, Z )}, {X /f (Y , a)}}.

and


Finally, notice that Theorem 2 ensures the preservation of most general answer
substitutions for ordinary goals only. Thus, the answer substitutions computed for
goals with occurrences of goal variables, may not be preserved, as shown by the
following example.
Example 14
Let us consider the following two programs P1 and P2 , where P2 is derived from
P1 by unfolding clause 1 w.r.t. p using clause 2:
P1 :

1.
2.
3.

a(G) ← (G = p) ∧ G
p←q
q←

P2 :

1*.
2.
3.

a(G) ← (G = q) ∧ G
p←q
q←

We have that P1 ⊢ a(G) 7→ {{G/p}}, and P2 ⊢ a(G) 7→ {{G/q}}.



30

A. Pettorossi and M. Proietti
7 Program Derivation in the Extended Language

In this section we present some examples which illustrate the use of our transformation rules. In these examples, by using goal variables and goal arguments, we
introduce and manipulate continuations. For this reason we have measured the improvements of program efficiency by running our programs using the BinProlog continuation passing compiler (Tarau 1996). These run-time improvements have been
reported in Section 7.6. Compilers based on different implementation methodologies, such as SICStus Prolog, may not give the same improvements. However, it
should be noticed that the efficiency improvements we get, do not come from the
use of continuations, but from the program transformations performed by applying our transformation rules (see Section 5). Indeed, in BinProlog the continuation
passing style transformation in itself gives no speed-ups.
Let us introduce the following terminology which will be useful in the sequel. We
say that: (i) a clause is in continuation passing style iff its body has no occurrences
of the conjunction operator, and (ii) a program is in continuation passing style iff all
its clauses are in continuation passing style. Thus, every program in continuation
passing style is a binary program in the sense of Tarau and Boyer (1990), that is,
a program with at most one atom in the body of its clauses.
When writing programs in this section we use the following primitive predicates:
=, 6=, ≥, and <. For the derivation of programs in continuation passing style, we
assume that, for each of these predicates there exists a corresponding primitive
predicate with an extra argument denoting a continuation. Let us call these predicates eq c, diff c, geq c, and lt c, respectively.
¯
¯
¯
¯
We assume that, for every program P , the following strong replacement laws
hold:
= eq c(X , Y , C ))
P ⊢ ∀ ((X = Y ) ∧ C ←→
¯
= diff c(M , N , C ))
P ⊢ ∀ ((M 6= N ) ∧ C ←→
¯
= geq c(M , N , C ))
P ⊢ ∀ ((M ≥ N ) ∧ C ←→
¯
= lt c(M , N , C ))
P ⊢ ∀ ((M < N ) ∧ C ←→
¯
In this section we use the following syntactical conventions:
(1) the conjunction operator ∧ is replaced by comma,
(2) a clause of the form h ← g1 ∨ g2 is also written as two clauses, namely, h ← g1
and h ← g2 , and
(3) a clause of the form h ← (V = u), g where the variable V does not occur in
the argument u, is also written as (h ← g){V /u}.
7.1 Tree Flipping
This example is borrowed from (Jørgensen et al. 1997) where it is used for showing
that conjunctive partial deduction may affect program termination when transforming programs for eliminating multiple traversals of data structures. A similar
problem arises when multiple traversals of data structures are avoided by applying Tamaki and Sato’s unfold/fold transformation rules (Tamaki and Sato 1984)

Transformations of Logic Programs with Goals as Arguments

31

according to the tupling strategy (see Section 2). In this example by using goal
arguments and introducing continuations, we are able to derive a program in continuation passing style which eliminates multiple traversals of data structures and,
at the same time, preserves universal termination.
Let us consider the initial program FlipCheck:
1.
2.
3.
4.
5.
6.
7.

flipcheck (X , Y ) ← flip(X , Y ), check (Y )
flip(l (N ), l (N )) ←
flip(t (L, N , R), t (FR, N , FL)) ← flip(L, FL), flip(R, FR)
check (l (N )) ← nat (N )
check (t (L, N , R)) ← nat(N ), check (L), check (R)
nat (0) ←
nat (s(N )) ← nat (N )

where: (i) the term l (N ) denotes a leaf with label N and the term t (L, N , R) denotes
a tree with label N and the two subtrees L and R, (ii) nat(X ) holds iff X is a natural
number, (iii) check (X ) holds iff all labels in the tree X are natural numbers, and
(iv) flip(X , Y ) holds iff the tree Y can be obtained by flipping all subtrees of the
tree X .
We would like to transform this program so to avoid the double traversal of trees
(see the double occurrence of Y in the body of clause 1). By applying the tupling
strategy (or, equivalently, conjunctive partial deduction), we derive the following
program FlipCheck1:
8. flipcheck (l (N ), l (N )) ← nat (N )
9. flipcheck (t (L, N , R), t (FR, N , FL)) ← nat(N ),
flipcheck (L, FL), flipcheck (R, FR)
Program FlipCheck1 performs only one traversal of any input tree which is the first
argument of flipcheck . However, as already mentioned, FlipCheck1 does not preserve
termination. Indeed, the goal flipcheck (t (l (N ), 0, l (a)), Y ) fails in FlipCheck, while
this goal does not terminate in the derived program FlipCheck1.
Now we present a second derivation starting from the same program FlipCheck
and producing a final program FlipCheck2 which: (i) is in continuation passing
style, (ii) traverses the input tree only once, and (iii) preserves termination. During
this second derivation we introduce goal arguments and we make use of the transformation rules introduced in Section 5. The initial step of this derivation is the
introduction of the following new clause:
10. newp(X , Y , G, C , D ) ← flip(X , Y ), G = (check (Y ), C ), D
As already mentioned, in this paper we do not illustrate the strategies needed for
guiding the application of our transformation rules and, in particular, we do not
indicate how to construct the new definitions to be introduced, such as clause 10
above. For clause 10 we notice that: (i) by introducing a definition with the goal
equality G = (check (Y ), C ), instead of the goal check (Y ), we will be able to apply
the folding rule by first performing leftward moves of goal equalities, instead of
(possibly incorrect) leftward moves of goals, and (ii) by introducing the continu-

32

A. Pettorossi and M. Proietti

ations C and D , we will avoid the expensive use of the conjunction operator for
constructing goal arguments.
We continue our derivation by unfolding clause 10 w.r.t. flip(X , Y ) and we get:
11. newp(l (N ), l (N ), G, C , D ) ← (G = (check (l (N )), C )), D
12. newp(t (L, N , R), t (FR, N , FL), G, C , D ) ← flip(L, FL), flip(R, FR)
(G = (check (t (FR, N , FL)), C )), D
We then unfold clauses 11 and 12 w.r.t. the check atoms, and after some applications
of the goal replacement rule based on boolean laws and CET, we get:
13. newp(l (N ), l (N ), G, C , D ) ← G = (nat(N ), C ), D
14. newp(t (L, N , R), t (FR, N , FL), G, C , D ) ← flip(L, FL), flip(R, FR),
(G = (nat(N ), check (FR), check (FL), C )), D
By introducing and rearranging goal equalities (see laws 2.1 and 2.2, respectively,
in Section 5), we transform clause 14 into:
15. newp(t (L, N , R), t (FR, N , FL), G, C , D ) ← flip(L, FL), U = (check (FL), C ),
flip(R, FR), V = (check (FR), U ), (G = (nat (N ), V )), D
Now we fold twice clause 15 using clause 10 and we get:
16. newp(t (L, N , R), t (FR, N , FL), G, C , D ) ←
newp(L, FL, U , C , newp(R, FR, V , U , (G = (nat (N ), V ), D ) ))
In order to express flipcheck in terms of newp we introduce a goal equality into
clause 1 and we derive:
17. flipcheck (X , Y ) ← flip(X , Y ), G = (check (Y ), true), G
Then we fold clause 17 using clause 10 and we get:
18. flipcheck (X , Y ) ← newp(X , Y , G, true, G)
The program we have derived so far consists of clauses 13, 16, and 18. Notice that
clauses 13 and 16 are not in continuation passing style because the conjunction
operator occurs in their bodies. In order to derive clauses in continuation passing
style we introduce the following new definition:
19. nat c(N , C ) ← nat(N ), C
¯
By unfolding, folding, and goal replacement steps based on the replacement law
= eq c(X , Y , C )), we derive the following final
FlipCheck ⊢ ∀ ((X = Y ), C ←→
¯
program FlipCheck2:
18. flipcheck (X , Y ) ← newp(X , Y , G, true, G)
20. newp(l (N ), l (N ), G, C , D ) ← eq c(G, nat c(N , C ), D )
¯
¯
21. newp(t (L, N , R), t (FR, N , FL), G, C , D ) ←
newp(L, FL, U , C , newp(R, FR, V , U ,
eq c(G, nat c(N , V ), D ) ))
¯
¯
22. nat c(0, C ) ← C
¯
23. nat c(s(N ), C ) ← nat c(N , C )
¯
¯
Program FlipCheck2 traverses the input tree only once. Moreover, Theorem 1 ensures that, for every goal g of the form flipcheck (t1 , t2 ), where t1 and t2 are any

Transformations of Logic Programs with Goals as Arguments

33

two terms, g terminates in FlipCheck iff g terminates in FlipCheck2 (see also Section 7.5 for a more detailed discussion of the correctness properties of our program
derivations).
7.2 Summing the Leaves of a Tree
Let us consider the following program TreeSum that, given a binary tree t whose
leaves are labeled by natural numbers, computes the sum of the labels of the leaves
of t .
1.
2.
3.
4.

treesum(l (N ), N ) ←
treesum(t (L, R), N ) ← treesum(L, NL), treesum(R, NR), plus(NL, NR, N )
plus(0, X , X ) ←
plus(s(X ), Y , s(Z )) ← plus(X , Y , Z )

By using Tamaki and Sato’s transformation rules, from program TreeSum we may
derive a more efficient program with accumulator arguments. In particular, during
this program derivation we introduce the following new predicate:
5. acc ts(T , Y , Z ) ← treesum(T , X ), plus(X , Y , Z )
¯
We also use the associativity of the predicate plus, that is, we use the following
equivalence which holds in the least Herbrand model M (TreeSum) of the given
program TreeSum:
M (TreeSum) |= ∀ X 1, X 2, X 3, S (∃I (plus(X 1, X 2, I ), plus(I , X 3, S )) ↔
∃J (plus(X 1, J , S ), plus(X 2, X 3, J )))
During the derivation, we also make suitable goal rearrangements needed for performing foldings that use clause 5. We derive the following program TreeSum1.
treesum(l (N ), N ) ←
treesum(t (L, R), N ) ← acc ts(L, NR, N ), treesum(R, NR)
¯
acc ts(l (N ), Acc, Z ) ← plus(N , Acc, Z )
¯
acc ts(t (L, R), Acc, N ) ← acc ts(L, Acc, NewAcc), acc ts(R, NewAcc, N )
¯
¯
¯
The least Herbrand models of programs TreeSum and TreeSum1 define the same
relation for the predicate treesum. However, the two programs do not have the
same termination behaviour. For instance, the goal treesum(t (l (N ), 0), Z ) fails in
TreeSum while it does not terminate in TreeSum1.
By introducing goal arguments and using the transformation rules presented in
Section 5, we are able to derive a program which: (i) is in continuation passing
style, (ii) preserves termination, and (iii) is asymptotically more efficient than the
original program TreeSum. Our derivation begins by introducing the following new
clause:
6.
7.
8.
9.

10. gen ts(T , Y , Z , G, C , D ) ← treesum(T , X ), (G = (plus(X , Y , Z ), C )), D
¯
We unfold clause 10 and we get:
11. gen ts(l (N ), Y , Z , G, C , D ) ← (G = (plus(N , Y , Z ), C )), D
¯
12. gen ts(t (L, R), Y , Z , G, C , D ) ← treesum(L, LS ), treesum(R, RS ),
¯
plus(LS , RS , S ), (G = (plus(S , Y , Z ), C )), D

34

A. Pettorossi and M. Proietti

Now we may exploit the following generalized associativity law for plus:
>

TreeSum ⊢ ∀V ((plus(X 1, X 2, I ), g[plus(I , X 3, S )]) ←→
(plus(X 1, J , S ), g[plus(X 2, X 3, J )]))
where V = {X 1, X 2, X 3, S } ∪ vars(g[ ]) and {I , J } ∩ vars(g[ ]) = ∅. By this law,
from clause 12 we get the following clause:
13. gen ts(t (L, R), Y , Z , G, C , D ) ← treesum(L, LS ), treesum(R, RS ),
¯
plus(LS , S 1, Z ), (G = (plus(RS , Y , S 1), C )), D
By introducing and rearranging goal equalities (see laws 2.1 and 2.2 in Section 5),
we transform clause 13 into:
14. gen ts(t (L, R), Y , Z , G, C , D ) ←
¯
treesum(L, LS ), (GL = (plus(LS , S 1, Z ), G = GR, D )),
treesum(R, RS ), (GR = (plus(RS , Y , S 1), C )), GL
In order to derive clauses in continuation passing style we introduce the following
new definitions:
15. ts c(T , N , C ) ← treesum(T , N ), C
¯
16. plus c(X , Y , Z , C ) ← plus(X , Y , Z ), C
¯
By unfolding clauses 15 and 16 we get:
17. ts c(l (N ), N , C ) ← C
¯
18. ts c(t (L, R), N , C ) ← treesum(L, LN ), treesum(R, RN ),
¯
plus(LN , RN , N ), C
19. plus c(0, X , X , C ) ← C
¯
20. plus c(s(X ), Y , s(Z ), C ) ← plus(X , Y , Z ), C
¯
By introducing and rearranging goal equalities, we transform clause 18 into:
21. ts c(t (L, R), N , C ) ← treesum(L, LN ), (G = (plus(LN , RN , N ), C )),
¯
treesum(R, RN ), G
By folding steps and goal replacements (based on, among others, the replacement
= eq c(X , Y , C ))), we get the following final
law TreeSum ⊢ ∀ ((X = Y ), C ←→
¯
program TreeSum2:
treesum(T , N ) ← ts c(T , N , true)
¯
ts c(l (N ), N , C ) ← C
¯
ts c(t (L, R), N , C ) ← gen ts(L, RN , N , G, C , ts c(R, RN , G))
¯
¯
¯
gen ts(l (N ), Y , Z , G, C , D ) ← eq c(G, plus c(N , Y , Z , C ), D )
¯
¯
¯
gen ts(t (L, R), Y , Z , G, C , D ) ← gen ts(L, S 1, Z , GL, eq c(G, GR, D ),
¯
¯
¯
gen ts(R, Y , S 1, GR, C , GL))
¯
19. plus c(0, X , X , C ) ← C
¯
20. plus c(s(X ), Y , s(Z ), C ) ← plus c(X , Y , Z , C )
¯
¯
This final program TreeSum2 is more efficient than TreeSum. Indeed, in the worst
case, TreeSum2 takes O (n) steps for solving a goal of the form treesum(t , N ), where
t is a ground tree and s n (0) is the sum of the labels of the leaves of t , while the initial
program TreeSum takes O (n 2 ) steps. Moreover, by our Theorem 1 of Section 6, for
every goal g of the form treesum(t1 , t2 ), where t1 and t2 are any terms, g terminates
in TreeSum iff g terminates in TreeSum2 (see also Section 7.5).
22.
18.
23.
24.
25.

Transformations of Logic Programs with Goals as Arguments

35

7.3 Matching a Regular Expression
Let us consider the following matching problem: given a string S in {0, 1, 2}∗, we
want to find the position N of an occurrence of a substring P of S such that P
is generated by the regular expression 0∗ 1. The following program RegExprMatch
computes such a position:
1.
2.
3.
4.
5.
6.
7.
8.
9.

match(S , N ) ← pattern(S ), N = 0
match([C |S ], N ) ← char (C ), match(S , M ), plus(s(0), M , N )
pattern([0|S ]) ← pattern(S )
pattern([1|S ]) ←
char (0) ←
char (1) ←
char (2) ←
plus(0, X , X ) ←
plus(s(X ), Y , s(Z )) ← plus(X , Y , Z )

If we assume the depth-first, left-to-right evaluation strategy of Prolog, the running
time of this program RegExprMatch is O (n 2 ) in the worst case, where n is the
length of the input string. For a goal of the form match(s, N ), where s is a ground
string made out of n 0’s, the program RegExprMatch performs one resolution step
using clause 1 for the call to match, and then n resolution steps using clause 3 for
the successive calls to pattern. When the computation backtracks, for the successive
call of match(s1, N ), where s1 is the tail of s, the program RegExprMatch performs
again n −1 resolution steps using clause 3.
By using the transformation rules of Section 5, we now present the derivation of
a new program RegExprMatch1 which: (i) is in continuation passing style, (ii) preserves termination, and (iii) is asymptotically more efficient than the original program RegExprMatch. Indeed, program RegExprMatch1 avoids the redundant resolution steps performed by RegExprMatch using clause 3. For our derivation we
introduce the following new predicates with goal arguments which are continuations:
10. match c(S , N , C ) ← match(S , N ), C
¯
11. newp(S , N , C 1, C 2) ← (pattern(S ), C 1) ∨ (match(S , N ), C 2)
12. plus c(X , Y , Z , C ) ← plus(X , Y , Z ), C
¯
By unfolding clauses 10, 11, and 12 we get:
13. match c([0|S ], N , C ) ← (pattern(S ), N = 0, C ) ∨
¯
(match(S , M ), plus(s(0), M , N ), C )
14. match c([1|S ], N , C ) ← (N = 0, C ) ∨
¯
(match(S , M ), plus(s(0), M , N ), C )
15. match c([2|S ], N , C ) ← match(S , M ), plus(s(0), M , N ), C
¯
16. newp([0|S ], N , C 1, C 2) ← (pattern(S ), C 1) ∨
(pattern(S ), N = 0, C 2) ∨
(match(S , M ), plus(s(0), M , N ), C 2)

36

A. Pettorossi and M. Proietti

17. newp([1|S ], N , C 1, C 2) ← C 1 ∨
(N = 0, C 2) ∨
(match(S , M ), plus(s(0), M , N ), C 2)
18. newp([2|S ], N , C 1, C 2) ← match(S , M ), plus(s(0), M , N ), C 2
19. plus c(0, X , X , C ) ← C
¯
20. plus c(s(X ), Y , s(Z ), C ) ← plus(X , Y , Z ), C
¯
By goal replacement using boolean laws, from clause 16 we get:
21. newp([0|S ], N , C 1, C 2) ← (pattern(S ), (C 1 ∨ (N = 0, C 2))) ∨
(match(S , M ), plus(s(0), M , N ), C 2)
By performing folding and goal replacement steps (based on the replacement law
= eq c(X , Y , C )) and other laws), we derive
RegExprMatch ⊢ ∀ ((X = Y ), C ←→
¯
the following program RegExprMatch1:
match(S , N ) ← match c(S , N , true)
¯
match c([0|S ], N , C ) ← newp(S , M , eq c(N , 0, C ), plus c(s(0), M , N , C ))
¯
¯
¯
match c([1|S ], N , C ) ← eq c(N , 0, C )
¯
¯
match c([1|S ], N , C ) ← match c(S , M , plus c(s(0), M , N , C ))
¯
¯
¯
match c([2|S ], N , C ) ← match c(S , M , plus c(s(0), M , N , C ))
¯
¯
¯
newp([0|S ], N , C 1, C 2) ←
newp(S , M , (C 1 ∨ eq c(N , 0, C 2)), plus c(s(0), M , N , C 2))
¯
¯
28. newp([1|S ], N , C 1, C 2) ← C 1
29. newp([1|S ], N , C 1, C 2) ← eq c(N , 0, C 2)
¯
30. newp([1|S ], N , C 1, C 2) ← match c(S , M , plus c(s(0), M , N , C 2))
¯
¯
31. newp([2|S ], N , C 1, C 2) ← match c(S , M , plus c(s(0), M , N , C 2))
¯
¯
19. plus c(0, X , X , C ) ← C
¯
32. plus c(s(X ), Y , s(Z ), C ) ← plus c(X , Y , Z , C )
¯
¯
This program RegExprMatch1 is in continuation passing style, avoids redundant
calls in case of backtracking, and takes O (n) resolution steps in the worst case,
to find an occurrence of a substring of the form 0∗ 1, where n is the length of the
input string. Moreover, by our Theorem 1 of Section 6, for every goal g of the form
match(t1 , t2 ), where t1 and t2 are any terms, g terminates in RegExprMatch iff g
terminates in RegExprMatch1 (see also Section 7.5).
22.
23.
24.
25.
26.
27.

7.4 Marking maximal elements
Let us consider the following marking problem. We are given: (i) a list L1 of the
form [x0 , . . . , xr ], where for i = 0, . . . , r , xi is a list of integers, and (ii) an integer n
(≥ 0). A list l of s +1 elements will also be denoted by [l [0], . . . , l [s]]. We assume
that for i = 0, . . . , r , the list xi has at least n +1 elements (and thus, the element
xi [n] exists) and we denote by m the maximum element of the set {x0 [n], . . . , xr [n]}.
From the list L1 we want to compute a new list L2 of the form [y0 , . . . , yr ] such
that, for i = 0, . . . , r , if xi [n] = m then yi [n] = ⊤ else yi [n] = xi [n].
For instance, if L1 = [[3, 8, −2, 4], [1, 3], [1, 8, 1]] and n = 1, then m = 8, that is,
the maximum element in {8, 3}. Thus, L2 = [[3, ⊤, 2, 4], [1, 3], [1, ⊤, 1]].

Transformations of Logic Programs with Goals as Arguments

37

The following program MaxMark computes the desired list L2 from the list L1
and the value N :
1. mmark (N , L1, L2) ← max nth(N , L1, 0, M ), mark (N , M , L1, L2)
¯
2. max nth(N , [], M , M ) ←
¯
3. max nth(N , [X |Xs], A, M ) ← nth(N , X , XN ), max (A, XN , B ),
¯
max nth(N , Xs, B , M )
¯
4. nth(0, [H |T ], H ) ←
5. nth(s(N ), [H |T ], E ) ← nth(N , T , E )
6. mark (N , M , [], []) ←
7. mark (N , M , [X |Xs], [Y |Ys]) ← mark nth(N , M , X , Y ),
¯
mark (N , M , Xs, Ys)
8. mark nth(0, M , [H 1|T ], [H 2|T ]) ← (M = H 1, H 2 = ⊤) ∨ (M 6= H 1, H 2 = H 1)
¯
9. mark nth(s(N ), M , [H |T 1], [H |T 2]) ← mark nth(N , M , T 1, T 2)
¯
¯
10. max (X , Y , X ) ← X ≥ Y
11. max (X , Y , Y ) ← X < Y
When running this program, the input list L1 = [x0 , . . . , xr ] is traversed twice: (i) the
first time L1 is traversed to compute the maximum m of the set {x0 [n], . . . , xr [n]}
(see the goal max nth(N , L1, 0, M ) in the body of clause 1), and (ii) the second time
¯
L1 is traversed to construct the list L2 by replacing, for i = 0, . . . , r , the element
xi [n] by ⊤ whenever xi [n] = m (see the goal mark (N , M , L1, L2)).
Now we use the transformation rules of Section 5 and from program MaxMark
we derive a new program MaxMark1 which: (i) is in continuation passing style,
(ii) preserves termination, and (iii) traverses the list L1 only once.
By the definition introduction rule we introduce the following new predicates
with goal arguments:
12. newp1(N , L1, L2, A, M , G, C 1, C 2) ←
max nth(N , L1, A, M ), (G = (mark (N , M , L1, L2), C 1)), C 2
¯
13. newp2(N , X , M , Y , A, B , G1, G2, C ) ←
nth(N , X , XN ), (G1 = (mark nth(N , M , X , Y ), G2)),
¯
max (A, XN , B ), C
14. max c(X , Y , Z , C ) ← max (X , Y , Z ), C
¯
We unfold clauses 12, 13, and 14, and then we move leftwards term equalities (see
law 3 in Section 5 which allows us to rearrange term equalities). We get the following
clauses:
15. newp1(N , [], [], M , M , C 1, C 1, C 2) ← C 2
16. newp1(N , [X |Xs], [Y |Ys], A, M , G, C 1, C 2) ←
nth(N , X , XN ), max (A, XN , B ), max nth(N , Xs, B , M ),
¯
(G = (mark nth(N , M , X , Y ), mark (N , M , Xs, Ys), C 1)),
¯
C2
17. newp2(0, [H 1|T ], M , [H 2|T ], A, B , G1, G2, C ) ←
(G1 = (((M = H 1, H 2 = ⊤) ∨ (M 6= H 1, H 2 = H 1)), G2)),
max (A, H 1, B ), C

38

A. Pettorossi and M. Proietti

18. newp2(s(N ), [H |T 1], M , [H |T 2], A, B , G1, G2, C ) ←
nth(N , T 1, XN ), (G1 = (mark nth(N , M , T 1, T 2), G2)),
¯
max (A, XN , B ), C
19. max c(X , Y , X , C ) ← X ≥ Y , C
¯
20. max c(X , Y , Y , C ) ← X < Y , C
¯
By introducing and rearranging goal equalities, from clause 16 we get:
21. newp1(N , [X |Xs], [Y |Ys], A, M , G, C 1, C 2) ←
nth(N , X , XN ), (G1 = (mark nth(N , M , X , Y ), G2)),
¯
max (A, XN , B ),
max nth(N , Xs, B , M ), (G2 = (mark (N , M , Xs, Ys), C 1)),
¯
(G = G1), C 2
Finally, by folding steps and goal replacements based on the replacement laws for
the primitive predicates =, 6=, ≥, and <, we derive the following final program
MaxMark1:
22. mmark (N , L1, L2) ← newp1(N , L1, L2, 0, M , G, true, G)
15. newp1(N , [], [], M , M , C 1, C 1, C 2) ← C 2
23. newp1(N , [X |Xs], [Y |Ys], A, M , G, C 1, C 2) ←
newp2(N , X , M , Y , A, B , G1, G2),
newp1(N , Xs, Ys, B , M , G2, C 1, eq c(G, G1, C 2)))
¯
24. newp2(0, [H 1|T ], M , [H 2|T ], A, B , G1, G2, C ) ←
eq c(G1, (eq c(M , H 1, eq c(H 2, ⊤, G2))∨
¯
¯
¯
diff c(M , H 1, eq c(H 2, H 1, G2))),
¯
¯
max c(A, H 1, B , C ))
¯
25. newp2(s(N ), [H |T 1], M , [H |T 2], A, B , G1, G2, C ) ←
newp2(N , T 1, M , T 2, A, B , G1, G2, C )
26. max c(X , Y , X , C ) ← geq c(X , Y , C )
¯
¯
27. max c(X , Y , Y , C ) ← lt c(X , Y , C )
¯
¯
This final program MaxMark1 is in continuation passing style and traverses the
input list L1 only once. Moreover, by our Theorem 1 of Section 6, for every goal g
of the form mmark (t1 , t2 , t3 ), where t1 , t2 , and t3 are any terms, if g terminates in
MaxMark then g terminates in MaxMark1 (see also Section 7.5).
7.5 Correctness of the Program Derivations
Let us briefly comment on the correctness properties of the program derivations we
have presented in this Section 7.
In all program derivations of Section 7, when using the transformation rules, we
have complied with the restrictions indicated at Point (1) of Theorem 2 (Weak
Correctness). Thus, for every program derivation from an initial program P0 to a
final program Pk , we have that Pk is a refinement of P0 ∪ Def k , where Def k is the
set of definitions introduced during the derivation. In particular, for every ordinary
goal g, if g terminates in P0 , then g terminates in Pk and the most general answer
substitutions for g computed by P0 are the same as those computed by Pk .
In the examples of Sections 7.1, 7.2, and 7.3 we have also complied with the

Transformations of Logic Programs with Goals as Arguments

39

restrictions of Point (2) of Theorem 2 (Strong Correctness), because all applications
of the goal replacement rule are based on strong replacement laws. Thus, in these
examples we have that Pk is equivalent to P0 ∪Def k . In particular, for every ordinary
goal g, if g terminates in Pk then g terminates in P0 ∪ Def k .
However, in the derivation of Section 7.4 we have not complied with the restrictions of Point (2) of Theorem 2. In particular, after unfolding clauses 12, 13, and
14, we have made leftward moves of term equalities by using law 3 of Section 5,
and law 3 is not a strong replacement law. Thus, there may be an ordinary goal
which does not terminate in the initial program MaxMark and terminates in the
final program MaxMark1. Indeed, the goal mmark (0, [H |T ], []) does not terminate
in MaxMark and terminates in MaxMark1.
Finally, in all program derivations of this Section 7, we have complied with the
restrictions of Theorem 3 (Preservation of Safety), because all replacement laws we
have applied preserve safety. Thus, since every ordinary goal is safe in the ordinary
initial program P0 , we have that every ordinary goal is safe in the final program Pk .
7.6 Experimental Results
In Table 1 below we have reported the speed-ups achieved in the examples presented
in this paper. The speed-up (see Column D) is defined as the ratio between the runtime of the initial program (see Column A) and the run-time of the derived, final
program (see Column B). In Columns A and B we have also indicated the asymptotic worst-case time complexity of the initial and final programs, respectively. For
each program the complexity is measured in terms of the size of the proofs relative
to that program (or, equivalently, the number of LD-resolution steps performed
using that program). The input goal is indicated in Column C. We performed our
measurements by using BinProlog on a SUN workstation. This use is justified by
the fact that every ordinary goal g is safe both in the initial program P0 and in
the final program Pk . Thus, we can use any Prolog system which implements LDresolution (and, in particular, the BinProlog system) for computing the relations
P0 ⊢ g 7→ A and Pk ⊢ g 7→ A defined by our operational semantics.
In Column C of Table 1 we have that:
(1) t1 is a random binary tree with 100,000 nodes;
(2) t2 is a random binary tree with 100,000 nodes;
(3) t3 is a random binary tree with 20,000 nodes and each node is labeled by a
numeral of the form s k (0), where 0 ≤ k ≤ 500;
(4) t4 is a random binary tree with 20,000 nodes whose leaves are labeled by numerals of the form s k (0), where 0 ≤ k ≤ 500;
(5) s is a random sequence of integers of the form: {0, 2}50000 1; and
(6) n1 is 700, l1 is a random list of 1000 lists, and each of these lists consists of 800
integers.
When measuring the speed-ups for the programs Deepest and DeepestOr in
Rows 1 and 2 we have computed the set of all answer substitutions, while for
the programs FlipCheck, TreeSum, RegExprMatch, and MaxMark in Rows 3–6 we
have computed one answer substitution only.

40

A. Pettorossi and M. Proietti

Table 1. Speed-ups of the Final Programs with respect to the Initial Programs
A. Initial Program :

B. Final Program :

Asymptotic Complexity

1.
2.
3.
4.
5.
6.

Deepest : O(n 2 )b
DeepestOr : O(n 2 )c
FlipCheck : O(n)d
TreeSum : O(n 2 )e
RegExprMatch : O(n 2 )f
MaxMark : O(n)g

C. Input goal

run-time(A)
run-time(B)

Asymptotic Complexity

Deepest2 : O(n)
Deepest2 : O(n)
FlipCheck2 : O(n)
TreeSum2: O(n)
RegExprMatch1 : O(n)
MaxMark1 : O(n)

D. Speed-up :a

deepest (t1 ,N )
deepest (t2 ,N )
flipcheck (t3 ,T )
treesum (t4 ,N )
match(s,N )
mmark (n1 ,l1 ,L2 )

5.2
2.7
1.0
9.2
1.8
1.8

a run-time(A) denotes the run-time of the program in Column A for the input goal in Column C.
run-time(B) denotes the run-time of the program in Column B for the input goal in Column C.
b n is the number of nodes of the tree t1 .
c n is the number of nodes of the tree t2 .
d n is the number of nodes of the tree t3 . For the goal flipcheck (t3 ,T ), the program FlipCheck
visits the tree t3 twice, while the program FlipCheck2 visits t3 only once.
e n is the sum of the leaves of the tree t4 .
f n is the length of the string s.
g n is the sum of the lengths of the lists in l1 .

As already mentioned at the end of Section 2, the value of the speed-up relative
to the initial program Deepest (see Row 1) is higher than the value of the speed-up
relative to the initial program DeepestOr (see Row 2), and this is not due to the use
of goals as arguments, but to the introduction of a disjunction, thereby clauses 2
and 3 have been replaced by clause 16.
The absence of speed-up for the final program FlipCheck2 (see Row 3) with respect to the initial program FlipCheck, is caused by the fact that the efficiency
improvements due to the elimination of the double traversal of the input tree t4
are cancelled out by the slowdown due to the introduction of multiple continuation arguments. However, the experimental results for the initial program MaxMark
and the final program MaxMark1 (see Row 6) show that the elimination of double
traversals of data structures may yield a significant speed-up, especially when the
access to the data structure is very costly. Recall that the program MaxMark traverses twice the list l1 , and for each list l in the list l1 , the program has to access
n1 elements of l . We have verified that the speed-up obtained by eliminating the
double traversal of l1 increases with the value of n1 .
8 Final Remarks and Related Work
We have shown that a simple extension of logic programming, where variables may
range over goals and goals may appear as arguments of predicate symbols, can be
very useful for transforming programs and improving their efficiency.
We have presented a set of transformation rules for our extended logic language
and we have shown their correctness with respect to the operational semantics
given in Section 4. In particular, in Section 6 we have shown that, under suit-

Transformations of Logic Programs with Goals as Arguments

41

able conditions, our transformation rules preserve termination (see Theorem 1),
most general answer substitutions (see Theorem 2), and safety (see Theorem 3).
As in (Bossi and Cocco 1994), for our logic programs we consider an operational
semantics based on universal termination (that is, the operational semantics of
a goal is defined iff all LD-derivations starting from that goal are finite). Theorem 2 extends the results presented in (Bossi and Cocco 1994) for definite logic
programs in that: (i) our language is an extension of definite logic programs, and
(ii) our folding rule is more powerful. Indeed, even restricting ourselves to programs that do not contain goal variables and goal arguments, we allow folding
steps which use clauses whose bodies contain disjunctions, and this is not possible
in (Bossi and Cocco 1994), where for applying the folding rule one is required to
use exactly one clause whose body is a conjunction of atoms. However, one should
notice that the transformations presented in (Bossi and Cocco 1994) preserve all
computed answer substitutions, while ours preserve the most general answer substitutions only.
Our logic language has some higher order capabilities because goals may occur as
arguments, but these capabilities are limited by the fact that the quantification of
function or predicate variables is not allowed. However, the objective of this paper
is not the design of a new higher order logic language, such as the ones presented
in (Chen et al. 1993; Hill and Gallagher 1998; Nadathur and Miller 1998). Rather,
our aim was to demonstrate the usefulness of some higher order constructs for
deriving efficient logic programs by transformation. Indeed, we have shown that
variables which range over goals are useful in the context of program transformation.
Moreover, the use of these variables may avoid the need for goal rearrangements
which could generate programs that do not preserve termination.
The approach we have proposed in this paper for avoiding incorrect goal rearrangements, is complementary to the approach described in (Bossi et al. 1996),
where the authors give sufficient conditions for goal rearrangements to preserve left
termination. (Recall that a program P is said to be left terminating iff all ground
goals universally terminate in P .) Thus, when these sufficient conditions are not
met or their validity cannot be proved, one may apply our technique which avoids
incorrect goal rearrangements by the introduction and the rearrangement of goal
equalities. Indeed, we have proved that the application of our technique preserves
universal termination, and thus, it preserves left termination as well.
The theory we have presented may also be used to give sound semantic foundations to the development of logic programs which use higher order generalizations and continuations. In (Pettorossi and Proietti 1997; Tarau and Boyer 1990)
and (Pettorossi and Skowron 1987; Wand 1980) the reader may find some examples
of use of these techniques in the case of logic and functional programs, respectively.
We leave for future work the development of suitable strategies for directing the
use of the transformation rules we have proposed in this paper.

42

A. Pettorossi and M. Proietti
Acknowledgements

We would like to thank Michael Leuschel for pointing out an error in a preliminary
version of this paper and for his helpful comments. We also thank the anonymous
referees of the LoPSTr ’99 Workshop, where a preliminary version of this paper
was presented (Pettorossi and Proietti 2000), and the referees of the Theory and
Practice of Logic Programming Journal for their suggestions.
This work has been partially supported by MURST Progetto Cofinanziato ‘Tecniche Formali per la Specifica, l’Analisi, la Verifica, la Sintesi e la Trasformazione di
Sistemi Software’ (Italy), and Progetto Coordinato CNR ‘Verifica, Analisi e Trasformazione dei Programmi Logici’ (Italy).
Appendix
This Appendix contains:
(i) Proposition 4 and its proof,
(ii) the proofs of Lemmata 1, 2, 3, and 4 (based on Propositions 2 and 4),
(iii) Lemmata 5 and 6 and their proofs (based on Proposition 4), and
(iv) the proofs of the main results, that is, (iv.1) the proof of Theorem 1 (based
on Proposition 3, Lemmata 1, 2, 3, and 4), (iv.2) the proof of Theorem 2 (based
on Proposition 1 and Theorem 1), and (iv.3) the proof of Theorem 3 (based on
Lemmata 5 and 6).
For the proofs of Proposition 4 and Lemma 1 given below, we need the following
definition.
Definition 8 (Size and µ-measure of a Deduction Tree)
Let τ be a finite deduction tree. The size of τ is the number of its nodes, and the
µ-measure of τ , denoted µ(τ ), is the pair hm, si, where m is the depth of τ and s
is the size of τ .
The values of the µ-measure can be lexicographically ordered, and we stipulate
that: hm1 , s1 i < hm2 , s2 i iff either m1 < m2 or (m1 = m2 and s1 < s2 ).
Proposition 4
Let P be a program, g1 , g2 be goals and let V be a set of variables.
(i) P ⊢ ∀V (g1 −→ g2 ) holds iff for every idempotent substitution ϑ such that
vars(ϑ) ∩ vars(g1 , g2 ) ⊆ V , for every goal g such that vars(g) ∩ vars(g1 , g2 ) ⊆ V ,
and for every b ∈ {true, false}, we have that:
if P ⊢ (g1 ϑ ∧ g) ↓ b then P ⊢ (g2 ϑ ∧ g) ↓ b.
>

(ii) P ⊢ ∀V (g1 −→ g2 ) holds iff for every idempotent substitution ϑ such that
vars(ϑ) ∩ vars(g1 , g2 ) ⊆ V , for every goal g such that vars(g) ∩ vars(g1 , g2 ) ⊆ V ,
and for every b ∈ {true, false}, we have that:
if P ⊢ (g1 ϑ ∧ g) ↓m b then P ⊢ (g2 ϑ ∧ g) ↓n b and m ≥ n.
(iii) The following two properties are equivalent:
(iii.1) for every goal context h[ ] such that vars(h[ ]) ∩ vars(g1 , g2 ) ⊆ V ,
if h[g1 ] is safe in P then h[g2 ] is safe in P , and

Transformations of Logic Programs with Goals as Arguments

43

(iii.2) for every idempotent substitution ϑ such that vars(ϑ) ∩ vars (g1 , g2 ) ⊆ V and
for every goal g such that vars(g) ∩ vars(g1 , g2 ) ⊆ V ,
if g1 ϑ ∧ g is safe in P then g2 ϑ ∧ g is safe in P .
Proof of Proposition 4
(i) only-if part. Let us consider an idempotent substitution ϑ such that vars(ϑ) ∩
vars(g1 , g2 ) ⊆ V . Let ϑ be {U1 /u1 , . . . , Uk /uk }. Since ϑ is idempotent we have
that for i = 1, . . . , k , Ui 6∈ ui . Assume that for every goal g such that vars(g) ∩
vars(g1 , g2 ) ⊆ V , and for every b ∈ {true, false}, there exists A1 ∈ P(Subst) such
that P ⊢ (g1 ϑ ∧ g) 7→ A1 . We have to show that there exists A2 ∈ P(Subst) such
that P ⊢ (g2 ϑ ∧ g) 7→ A2 and A1 = ∅ iff A2 = ∅.
By suitably renaming the variables of the goal g1 , without loss of generality we
may assume that, for i = 1, . . . , k , Ui 6∈ vars(g). Since ϑ is idempotent, by using
rules (teq2) and (geq) we may construct a proof of P ⊢ U1 = u1 ∧ . . . ∧ Uk = uk ∧
g1 ∧ g 7→ B1 , where B1 = (ϑ ◦ A1 ). By the hypothesis that P ⊢ ∀V (g1 −→ g2 ) holds
and the hypotheses that vars(ϑ) ∩ vars(g1 , g2 ) ⊆ V and vars(g) ∩ vars (g1 , g2 ) ⊆ V ,
we have that there exists B2 ∈ P(Subst) such that P ⊢ U1 = u1 ∧ . . . ∧ Uk = uk ∧
g2 ∧ g 7→ B2 has a proof and B1 = ∅ iff B2 = ∅. The only way of constructing
this proof is by using k times the rules (teq2) or (geq) and constructing a proof of
P ⊢ g2 ϑ ∧ g 7→ A2 , where B2 = (ϑ◦A2 ). Thus, A1 = ∅ iff B1 = ∅ iff B2 = ∅ iff A2 = ∅.
(i) if part. We show a slightly more general fact than the if part of (i). We assume
that for every idempotent substitution ϑ such that vars(ϑ) ∩ vars(g1 , g2 ) ⊆ V , and
for every goal g such that vars(g) ∩ vars(g1 , g2 ) ⊆ V , if there exists A1 ∈ P(Subst)
such that P ⊢ (g1 ϑ ∧ g) 7→ A1 , then there exists A2 ∈ P(Subst) such that P ⊢
(g2 ϑ ∧ g) 7→ A2 and A1 = ∅ iff A2 = ∅. Then we show that, for every goal context
h[ ] and substitution ϑ such that vars(h[ ]ϑ) ∩ vars(g1 , g2 ) ⊆ V ,
if there exists B1 ∈ P(Subst) such that P ⊢ h[g1 ]ϑ 7→ B1
then there exists B2 ∈ P(Subst) such that P ⊢ h[g2 ]ϑ 7→ B2
and B1 = ∅ iff B2 = ∅.
We prove our thesis by induction on the measure µ(π) (see Definition 8) of the
proof π of P ⊢ h[g1 ]ϑ 7→ B1 (recall that a proof is a particular finite deduction
tree). We reason by cases on the structure of the goal context h[ ]. We consider the
following four cases only. The others are similar and we omit them.
- Case 1: h[ ] is ∧ g3 .
Assume that P ⊢ g1 ϑ∧g3 ϑ 7→ B1 . Then, by hypothesis, we get: P ⊢ g2 ϑ∧g3 ϑ 7→ B2
for some B2 ∈ P(Subst) such that B1 = ∅ iff B2 = ∅.
- Case 2: h[ ] is t1 = t2 ∧ g3 [ ].
Assume that there exists a proof π1 of P ⊢ t1 ϑ = t2 ϑ ∧ g3 [g1 ]ϑ 7→ B1 .
If t1 ϑ and t2 ϑ are not unifiable then, by rule (teq1), B1 is ∅ and there exists a proof
of P ⊢ t1 ϑ = t2 ϑ ∧ g3 [g2 ]ϑ 7→ ∅.
If t1 ϑ and t2 ϑ are unifiable then, by rule (teq2), B1 is of the form (mgu(t1 ϑ, t2 ϑ)◦C1 )
for some C1 ∈ P(Subst) and there exists a proof π2 of P ⊢ g3 [g1 ]ϑ mgu(t1 ϑ, t2 ϑ) 7→
C1 . Since µ(π2 ) < µ(π1 ), by induction hypothesis P ⊢ g3 [g2 ]ϑ mgu(t1 ϑ, t2 ϑ) 7→ C2
has a proof for some C2 ∈ P(Subst) and C1 = ∅ iff C2 = ∅. Thus, by rule (teq2),

44

A. Pettorossi and M. Proietti

there exists B2 ∈ P(Subst) such that P ⊢ t1 ϑ = t2 ϑ ∧ g3 [g2 ]ϑ 7→ B2 where B2 =
mgu(t1 ϑ, t2 ϑ) ◦ C2 and B1 = ∅ iff C1 = ∅ iff C2 = ∅ iff B2 = ∅.
- Case 3: h[ ] is (G = g3 [ ]) ∧ g4 .
Assume that P ⊢ ((G = g3 [g1 ]) ∧ g4 )ϑ 7→ B1 has a proof of depth m and size s.
Then, Gϑ is a goal variable not occurring in g3 [g1 ]ϑ, the node P ⊢ (Gϑ = g3 [g1 ]ϑ) ∧
g4 ϑ 7→ B1 has been obtained by applying rule (geq), B1 is {Gϑ/g3 [g1 ]ϑ} ◦ C1 for
some C1 ∈ P(Subst), and P ⊢ g4 ϑ{Gϑ/g3 [g1 ]ϑ} 7→ C1 has a proof of depth
m and size s − 1. Now, suppose that Gϑ occurs in g4 ϑ n times. Thus, also g1
will occur n times in g4 ϑ{Gϑ/g3 [g1 ]ϑ}. Since hm, s −1i < hm, si, by applying the
induction hypothesis n times, we have that there exists C2 ∈ P(Subst) such that
P ⊢ g4 ϑ{Gϑ/g3 [g2 ]ϑ} 7→ C2 has a proof and C1 = ∅ iff C2 = ∅. By using rule
(geq), we can construct a proof of P ⊢ Gϑ = g3 [g2 ]ϑ ∧ g4 ϑ 7→ B2 , where B2 is
{Gϑ/g3 [g2 ]ϑ}◦C2 . Thus, B1 = ∅ iff C1 = ∅ iff C2 = ∅ iff B2 = ∅.
- Case 4: h[ ] is p(u1 , . . . , ui [ ], . . . , uk ) ∧ g3 .
Assume that P ⊢ p(u1 ϑ, . . . , ui [g1 ]ϑ, . . . , uk ϑ) ∧ g3 ϑ 7→ B1 has a proof of depth m
and size s. Then, in the last step of this proof rule (at ) has been used, B1 is of
the form C1 ↾ vars(p(u1 ϑ, . . . , ui [g1 ]ϑ, . . . , uk ϑ) ∧ g3 ϑ) for some C1 ∈ P(Subst), and
P ⊢ body{U1 /u1 ϑ, . . . , Ui /ui [g1 ]ϑ, . . . , Uk /uk ϑ} ∧ g3 ϑ 7→ C1 has a proof of depth
m −1 and size s −1, where p(U1 , . . . , Ui , . . . , Uk ) ← body is a renamed apart clause
of P . Since hm − 1, s − 1i < hm, si, by induction hypothesis we have that there
exists C2 ∈ P(Subst) such that P ⊢ body {U1 /u1 ϑ, . . . , Ui /ui [g2 ]ϑ, . . . , Uk /uk ϑ} ∧
g3 ϑ 7→ C2 has a proof and C1 = ∅ iff C2 = ∅. Thus, by using rule (at ), we can
construct a proof of P ⊢ p(u1 ϑ, . . . , ui [g2 ]ϑ, . . . , uk ϑ) ∧ g3 ϑ 7→ B2 , where B2 is
C2 ↾ vars(p(u1 ϑ, . . . , ui [g2 ]ϑ, . . . , uk ϑ) ∧ g3 ϑ) and B1 = ∅ iff C1 = ∅ iff C2 = ∅ iff
B2 = ∅.
(ii) The proof is similar to the one of (i) and we omit it.
(iii) Suppose that (iii.1) holds and suppose also that ϑ is an idempotent substitution
such that vars(ϑ)∩vars(g1 , g2 ) ⊆ V , g is a goal such that vars(g)∩vars(g1 , g2 ) ⊆ V ,
and g1 ϑ ∧ g is safe in P . We have to prove that g2 ϑ ∧ g is safe in P .
Suppose that g2 ϑ ∧ g is not safe in P . Then there exist A ∈ P(Subst) and a
deduction tree τ1 for P ⊢ g2 ϑ ∧ g 7→ A such that a leaf of τ1 is of the form
P ⊢ g3 7→ B and g3 is stuck. Let ϑ be the substitution {U1 /u1 , . . . , Uk /uk } such
that, for i = 1, . . . , k , Ui 6∈ ui . Without loss of generality, we may assume that,
for i = 1, . . . , k , Ui 6∈ vars(g). By using rules (teq2) and (geq), we can construct
a deduction tree τ2 for P ⊢ U1 = u1 ∧ . . . ∧ Uk = uk ∧ g2 ∧ g 7→ A such that
τ2 has P ⊢ g3 7→ B at a leaf. Thus, U1 = u1 ∧ . . . ∧ Uk = uk ∧ g2 ∧ g is not
safe in P . Since vars(ϑ) ∩ vars(g1 , g2 ) ⊆ V and vars(g) ∩ vars(g1 , g2 ) ⊆ V , we
have that vars(U1 = u1 ∧ . . . ∧ Uk = uk ∧ g) ∩ vars(g1 , g2 ) ⊆ V and, thus, by (iii.1)
U1 = u1 ∧. . .∧Uk = uk ∧g1 ∧g is not safe in P . None of the goals U1 = u1 , . . . , Uk = uk
is stuck and, thus, a descendant node of g1 ϑ ∧ g is stuck, that is, g1 ϑ ∧ g is not safe
in P .
The proof that (iii.2) implies (iii.1) can be done by induction on deduction trees
ordered by the µ-measure. We omit this proof.

Transformations of Logic Programs with Goals as Arguments

45

Proof of Lemma 1
Recall that, by definition, for every b ∈ {true, false}, P ⊢ g ↓m b means that there
exists A ∈ P(Subst) such that P ⊢ g 7→ A has a proof of depth m and b = true iff
A 6= ∅. We prove the thesis by induction on the µ-measure (see Definition 8) of the
proof of P ⊢ g 7→ A which, by hypothesis, has depth m and size s.
Our induction hypothesis is that, for all hm1, s1i < hm, si, for all goals g, and for
all A1 ∈ P(Subst), if P ⊢ g 7→ A1 has a proof of depth m1 and size s1, then there
exists B1 ∈ P(Subst) such that NewP ⊢ g 7→ B1 has a proof of depth n1, with
m1 ≥ n1, and A1 = ∅ iff B1 = ∅. We have to show that there exists B ∈ P(Subst)
such that NewP ⊢ g 7→ B has a proof of depth n, with m ≥ n, and A = ∅ iff
B = ∅. We proceed by cases on the structure of g. We first notice that, since ∧ is
associative with neutral element true, the grammar for generating goals given in
Section 2 can be replaced by the following one:
g ::= G ∧ g1 | true | false ∧ g1 | (t1 = t2 ) ∧ g1 | (g1 = g2 ) ∧ g3 |
p(u1 , . . . , um ) ∧ g1 | (g1 ∨ g2 ) ∧ g3
We consider the following two cases only. The others are similar and we omit them.
- Case 1: g is (g1 = g2 )∧g3 . Assume that P ⊢ (g1 = g2 )∧g3 7→ A has a proof of depth
m and size s. Then, g1 is a goal variable, say G, G 6∈ vars(g2 ), P ⊢ (G = g2 ) ∧ g3 7→
A has been derived by applying rule (geq), and there exists A1 ∈ P(Subst) such
that A = ({G/g2 } ◦ A1 ) and P ⊢ g3 {G/g2 } 7→ A1 has a proof of depth m and size
s − 1. Since hm, s−1i < hm, si, by induction hypothesis there exists B1 ∈ P(Subst)
such that NewP ⊢ g3 {G/g2 } 7→ B1 has a proof of depth n with m ≥ n and
A1 = ∅ iff B1 = ∅. By rule (geq), we have that NewP ⊢ (G = g2 ) ∧ g3 7→ B , where
B = ({G/g2 } ◦ B1 ), has a proof of depth n with m ≥ n. By the definition of the ◦
operator, we have that A = ∅ iff A1 = ∅ iff B1 = ∅ iff B = ∅.
- Case 2: g is p(u1 , . . . , um ) ∧ g1 . Assume that P ⊢ p(u1 , . . . , um ) ∧ g1 7→ A has
a proof of depth m and size s. Then, P ⊢ p(u1 , . . . , um ) ∧ g1 7→ A has been
derived by using rule (at ), and there exists A1 ∈ P(Subst) such that A = (A1 ↾
vars(p(u1 , . . . , uk ) ∧ g1 )) and P ⊢ bd r {V1 /u1 , . . . , Vm /um } ∧ g1 7→ A1 has a proof
of depth m − 1 and size s − 1, where p(V1 , . . . , Vm ) ← bd r is a renamed apart
>

clause of P . Now, by the hypothesis that P ⊢ ∀V1 , . . . , Vm (bdr −→ newbd r ), by
the fact that vars({V1 /u1 , . . . , Vm /um }) ∩ vars(bd r , newbd r ) ⊆ {V1 , . . . , Vm } and
vars(g1 ) ∩ vars(bd r , newbd r ) ⊆ {V1 , . . . , Vm }, and by Proposition 4 (ii), we have
that there exists A2 ∈ P(Subst) such that P ⊢ newbd r {V1 /u1 , . . . , Vm /um }∧g1 7→
A2 has a proof of depth n1 and size s1, with m − 1 ≥ n1 and A1 = ∅ iff A2 = ∅.
Since hn1, s1i < hm, si, by induction hypothesis there exists B1 ∈ P(Subst) such
that NewP ⊢ newbd r {V1 /u1 , . . . , Vm /um } ∧ g1 7→ B1 has a proof of depth n2
with n1 ≥ n2 and A2 = ∅ iff B1 = ∅. Since hd r is p(V1 , . . . , Vm ), by using rule (at )
we can construct a proof for NewP ⊢ p(u1 , . . . , um ) ∧ g1 7→ B of depth n = n2+1
where B = (B1 ↾ vars(p(u1 , . . . , uk ) ∧ g1 )). Thus, m ≥ n and, by the definition of
the ↾ operator, A = ∅ iff A1 = ∅ iff A2 = ∅ iff B1 = ∅ iff B = ∅.
Proof of Lemma 2
(i) Let us consider the transformation sequence Pi , . . . , Pj . Let us also consider

46

A. Pettorossi and M. Proietti

any index h in {i, . . . , j −1} and any two clauses c1 : hd ← bd in program Ph and
c2 : hd ← newbd in program Ph+1 . Since Pi , . . . , Pj is constructed by using the
unfolding rule only, we have that:
bd = b[p(u1 , . . . , um )]

and newbd = b[g{V1 /u1 , . . . , Vm /um }]

for some clause p(V1 , . . . , Vm ) ← g in Pi , some goal context b[ ], and some m-tuple
of arguments (u1 , . . . , um ). To prove this lemma we have to show that:
>

Pi ⊢ ∀V (b[p(u1 , . . . , um )] −→ b[g{V1 /u1 , . . . , Vm /um }])

(α)

where V = vars(hd ). Now, for every clause p(V1 , . . . , Vm ) ← g in Pi we have that:
>

Pi ⊢ ∀V1 , . . . , Vm (p(V1 , . . . , Vm ) −→ g)

(β)

′

From (β), by Point (iv ) of Proposition 2 we get:
>

Pi ⊢ ∀W (p(u1 , . . . , um ) −→ g{V1 /u1 , . . . , Vm /um })

(γ)

′

where W = vars(u1 , . . . , um ). From (γ), by Point (i ) of Proposition 2 we get:
>

Pi ⊢ ∀Z (b[p(u1 , . . . , um )] −→ b[g{V1 /u1 , . . . , Vm /um }])
′

(δ)
′

where Z = vars(b[p(u1 , . . . , um )]). From (δ), by Points (ii ) and (iii ) of Proposition 2 we get (α), as desired.
(ii) In order to prove Point (ii) of the thesis, we first show the following property.
Property (A): For every clause d : newp(V1 , . . . , Vm ) ← g in Def k which is used
for folding during the construction of the sequence Pj , . . . , Pk , we have that the
= g) holds.
replacement law Pj ⊢ ∀V1 , . . . , Vm (newp(V1 , . . . , Vm ) ←→
Property (A) is a consequence of the fact that during the sequence Pi , . . . , Pj we
have performed the parallel leftmost unfolding of every clause which is used for
folding during Pj , . . . , Pk .
Now we prove Point (ii) of the thesis by cases with respect to the transformation
rule which is used to derive program Ph+1 from program Ph , for h = j , . . . , k −1.
- Case 1: Ph+1 is derived from Ph by the unfolding rule using a clause which is
among those also used for folding (in a previous transformation step). The thesis
follows from Property (A) and Points (i′ ), (ii′ ), (iii′ ), and (iv′ ) of Proposition 2.
- Case 2: Ph+1 is derived from Ph by the unfolding rule using a clause c which
is not among those used for folding. Thus, c belongs to P0 because the only way
of introducing in the body of a clause an occurrence of a non-primitive predicate
which is not defined in P0 , is by an application of the folding rule. Hence, c belongs
to Pj as well. Now, for every clause c of the form: p(V1 , . . . , Vm ) ← g in Pj we
have that:
>

Pj ⊢ ∀V1 , . . . , Vm (p(V1 , . . . , Vm ) −→ g)
The thesis follows from Property (A) and Points (i′ ), (ii′ ), (iii′ ), and (iv′ ) of Proposition 2.
- Case 3: Ph+1 is derived from Ph by the folding rule. The thesis follows from
Property (A) and Points (i′ ), (ii′ ), (iii′ ), and (iv′ ) of Proposition 2.
- Case 4: Ph+1 is derived from Ph by the goal replacement rule based on a replace>

ment law of the form P0 ⊢ ∀V (g1 −→ g2 ). The thesis follows from Points (i′ ), (ii′ ),

Transformations of Logic Programs with Goals as Arguments

47

>

and (iii′ ) of Proposition 2 and the fact that also Pj ⊢ ∀ V (g1 −→ g2 ) holds, because
the non-primitive predicates of {g1 , g2 } are defined in P0 , and for each predicate p
defined in P0 , the definition of p in P0 is equal to the definition of p in Pj .
Proof of Lemma 3
We assume that there exists A ∈ P(Subst) such that NewP ⊢ g 7→ A has a proof
of size n. We have to show that there exists B ∈ P(Subst) such that P ⊢ g 7→ B
holds, and A = ∅ iff B = ∅. We proceed by induction on n. We assume that, for all
m < n, for all goals h, and for all A1 ∈ P(Subst), if NewP ⊢ h 7→ A1 has a proof
of size m, then P ⊢ h 7→ B1 has a proof for some B1 ∈ P(Subst) such that A1 = ∅
iff B1 = ∅. Now we proceed by cases on the structure of g. We consider the following
two cases. The other cases are similar and we omit them.
- Case 1: g is (g1 = g2 ) ∧ g3 . Assume that NewP ⊢ (g1 = g2 ) ∧ g3 7→ A has a
proof of size n. Then, g1 is a goal variable, say G, G 6∈ vars(g2 ), and NewP ⊢
(G = g2 ) ∧ g3 7→ A has been derived by applying rule (geq). Thus, there exists
A1 ∈ P(Subst) such that A is ({G/g2 } ◦ A1 ) and NewP ⊢ g3 {G/g2 } 7→ A1 has a
proof of size n −1. By induction hypothesis there exists B1 ∈ P(Subst) such that
P ⊢ g3 {G/g2 } 7→ B1 has a proof and A1 = ∅ iff B1 = ∅. By using rule (geq), we
can construct a proof of P ⊢ (G = g2 ) ∧ g3 7→ B where B is {G/g2 } ◦ B1 . By the
definition of the ◦ operator, we have that A = ∅ iff A1 = ∅ iff B1 = ∅ iff B = ∅.
- Case 2: g is p(u1 , . . . , um )∧g1 . Assume that NewP ⊢ p(u1 , . . . , um )∧g1 7→ A has a
proof of size n. Then, NewP ⊢ p(u1 , . . . , um )∧g1 7→ A has been derived by applying
rule (at ), and there exists a proof of size n − 1 of NewP ⊢ newbdr {V1 /u1 , . . . ,
Vm /um } ∧ g1 7→ A1 where p(V1 , . . . , Vm ) ← newbdr is a renamed apart clause
of NewP and A is (A1 ↾ vars(p(u1 , . . . , uk ) ∧ g1 )). By induction hypothesis there
exists a proof of P ⊢ newbdr {V1 /u1 , . . . , Vm /um } ∧ g1 7→ B1 such that A1 = ∅
iff B1 = ∅. Now, by the hypothesis that P ⊢ ∀V1 , . . . , Vm (newbdr −→ bdr ), by
the fact that vars({V1 /u1 , . . . , Vm /um }) ∩ vars(bdr , newbdr ) ⊆ {V1 , . . . , Vm } and
vars(g1 )∩vars(bdr , newbdr ) ⊆ {V1 , . . . , Vm }, and by Proposition 4 (i), we have that
P ⊢ bdr {V1 /u1 , . . . , Vm /um } ∧ g1 7→ B2 has a proof for some B2 ∈ P(Subst) such
that B1 = ∅ iff B2 = ∅. Since hd r is p(V1 , . . . , Vm ), by using rule (at ) we can construct
a proof for P ⊢ p(u1 , . . . , um ) ∧ g1 7→ B where B is (B2 ↾ vars(p(u1 , . . . , uk ) ∧ g1 )).
By the definition of the ↾ operator, we have that A = ∅ iff A1 = ∅ iff B1 = ∅ iff B2 = ∅
iff B = ∅.
Proof of Lemma 4
If Ph+1 is derived from Ph by the unfolding rule using a clause of the form
p(V1 , . . . , Vm ) ← g in P0 ∪ Def k , then the thesis follows from Points (i), (ii), (iii),
and (iv) of Proposition 2, and the fact that the replacement law P0 ∪ Def k ⊢
∀V1 , . . . , Vm (g −→ p(V1 , . . . , Vm )) holds. Similarly, if Ph+1 is derived from Ph by
the folding rule using a clause of the form newp(V1 , . . . , Vm ) ← g in Def k , then the
thesis follows from Points (i), (ii), (iii), and (iv) of Proposition 2, and the fact that
the replacement law P0 ∪ Def k ⊢ ∀V1 , . . . , Vm (newp(V1 , . . . , Vm ) −→ g) holds.

48

A. Pettorossi and M. Proietti

Finally, if Ph+1 is derived from Ph by the goal replacement rule, then the thesis follows from the fact that it is based on a strong replacement law and from Points (i),
(ii), and (iii) of Proposition 2.
The following Lemma 5 and Lemma 6 are necessary for proving that a transformation sequence preserves safety (see Theorem 3).
Lemma 5
Let P and NewP be programs of the form:
P:

hd1 ← bd1
..
.
hds ← bds

NewP :

hd1 ← newbd 1
..
.
hds ← newbd s

Suppose that for r = 1, . . . , s and for every goal context b[ ] such that vars(b[ ]) ∩
vars(bdr , newbdr ) ⊆ vars(hdr ), we have that if b[bd r ] is safe in P then b[newbd r ] is
safe in P . Then, for every goal g, if g is safe in P then g is safe in NewP .

Proof of Lemma 5
We assume that g is not safe in NewP and we prove that g is not safe in P .
Since g is not safe in NewP, there exist A ∈ P(Subst) and a deduction tree τ for
NewP ⊢ g 7→ A such that a leaf of τ is of the form NewP ⊢ gstuck 7→ B and
the goal gstuck is stuck. We proceed by induction on the size of τ . We consider the
following two cases only. The others are similar and we omit them.
- Case 1: g is (g1 = g2 ) ∧ g3 . Assume that the deduction tree τ for NewP ⊢
(g1 = g2 )∧g3 7→ A has size s. If g1 is not a goal variable or it is a goal variable
occurring in g2 , then (g1 = g2 ) ∧ g3 is not safe in P . Otherwise, g1 is a goal variable,
say G, and G 6∈ vars(g2 ). Thus, NewP ⊢ (G = g2 ) ∧ g3 7→ A has been derived by
applying rule (geq), and there exists A1 ∈ P(Subst) such that: (a) the subtree τ1 of
τ rooted at NewP ⊢ g3 {G/g2 } 7→ A1 has size s−1, and (b) NewP ⊢ gstuck 7→ B is
a leaf of τ1 . By induction hypothesis g3 {G/g2 } is not safe in P and, by rule (geq),
also (G = g2 ) ∧ g3 is not safe in P .
- Case 2: g is p(u1 , . . . , um ) ∧ g1 . Assume that the deduction tree τ for NewP ⊢
p(u1 , . . . , um ) ∧ g1 7→ A has size s. Thus, NewP ⊢ p(u1 , . . . , um ) ∧ g1 7→ A
has been derived by using rule (at ), and there exist A′ ∈ P(Subst) and a renamed apart clause p(V1 , . . . , Vm ) ← newbd r of NewP such that: (a) the subtree τ1 of τ rooted at NewP ⊢ newbd r {V1 /u1 , . . . , Vm /um } ∧ g1 7→ A′ has
size s − 1 and (b) NewP ⊢ gstuck 7→ B is a leaf of τ1 . By induction hypothesis newbd r {V1 /u1 , . . . , Vm /um } ∧ g1 is not safe in P . Now, by hypothesis, by
the fact that vars({V1 /u1 , . . . , Vm /um }) ∩ vars(bdr , newbdr ) ⊆ {V1 , . . . , Vm } and
vars(g1 ) ∩ vars(bdr , newbdr ) ⊆ {V1 , . . . , Vm }, and by Proposition 4 (iii), we have
that bd r {V1 /u1 , . . . , Vm /um } ∧ g1 is not safe in P . Since p(V1 , . . . , Vm ) ← bd r is a
renamed apart clause of P , by rule (at ), also p(u1 , . . . , um ) ∧ g1 is not safe in P .

Transformations of Logic Programs with Goals as Arguments

49

Lemma 6
Let P0 , . . . , Pk be a transformation sequence and let Def k be the set of definitions
introduced during that sequence. For h = 0, . . . , k − 1, for any pair of clauses c1 :
hd ← bd in program Ph and c2 : hd ← newbd in program Ph+1 , such that c2 is
derived from c1 by an application of the unfolding rule, or folding rule, or goal
replacement rule which preserves safety, and for every goal context b[ ] such that
vars(b[ ]) ∩ vars(bd , newbd ) ⊆ vars(hd ), we have that:
if b[bd ] is safe in P0 ∪ Def k then b[newbd ] is safe in P0 ∪ Def k .
Proof of Lemma 6
First we notice that, for every clause hd0 ← bd0 in P0 ∪ Def k and for every goal
context b[ ] such that vars(b[ ]) ∩ vars(bd0 ) ⊆ vars(hd0 ), we have the following:
Property (S): b[hd0 ] is safe in P0 ∪ Def k iff b[bd0 ] is safe in P0 ∪ Def k .
Now, take any h = 0, . . . , k − 1. We reason by cases on the transformation rule
applied for deriving the clause hd ← newbd in Ph+1 from the clause hd ← bd in
Ph .
If hd ← newbd is derived from hd ← bd by the unfolding rule using a clause
hd0 ← bd0 in P0 ∪ Def k , then for some goal context g[ ], bd is of the form g[hd0 ϑ]
and newbd is of the form g[bd0 ϑ]. Then the thesis follows from the only-if part of
Property (S).
Similarly, if hd ← newbd is derived from hd ← bd by the folding rule using a
clause hd0 ← bd0 in P0 ∪ Def k , then for some goal context g[ ], bd is of the form
g[bd0 ϑ] and newbd is of the form g[hd0 ϑ]. Then the thesis follows from the if part
of Property (S).
Finally, if hd ← newbd is derived from hd ← bd by the goal replacement rule, then
the thesis follows from the hypothesis that every application of the goal replacement
rule preserves safety.
Proof of Theorem 1 (Preservation of Successes and Failures).
By Proposition 3, without loss of generality we may assume that the admissible
sequence P0 , . . . , Pk is ordered. Let Pj be the program obtained at the end of the
second subsequence of P0 , . . . , Pk , that is, after unfolding every clause in Def k which
is used for folding. Point (1) of this theorem is a consequence of the following two
facts:
(F1) by Lemma 1 and Point (i) of Lemma 2, we have that, for every goal g and for
every b ∈ {true, false}, if P0 ∪ Def k ⊢ g ↓m b then Pj ⊢ g ↓n1 b with m ≥ n1,
and
(F2) by Lemma 1 and Point (ii) of Lemma 2, we have that: for every goal g and
for every b ∈ {true, false}, if Pj ⊢ g ↓n1 b then Pk ⊢ g ↓n b with n1 ≥ n.
Point (2) of this theorem is a straightforward consequence of Lemmata 3 and 4.
Proof of Theorem 2 (Correctness Theorem).
(1) First we prove that P0 ∪ Def k ⊑ Pk . Let g be an ordinary goal and let A be
a set of substitutions such that P0 ∪ Def k ⊢ g 7→ A. We have to prove that there

50

A. Pettorossi and M. Proietti

exists B ∈ P(Subst) such that Pk ⊢ g 7→ B and A and B are equally general with
respect to g.
Since P0 ∪ Def k ⊢ g 7→ A, by definition there exists b ∈ {true, false} such that
P0 ∪ Def k ⊢ g ↓ b. By Point (1) of Theorem 1, we have that Pk ⊢ g ↓ b and, thus,
there exists B ∈ P(Subst) such that Pk ⊢ g 7→ B .
In order to prove that A and B are equally general with respect to g, we have to
show that: (a) for every substitution α ∈ A there exists a substitution β ∈ B such
that gα is an instance of gβ, and (b) for every β ∈ B there exists α ∈ A such that
gβ is an instance of gα.
(a) Let α be a substitution in A. From P0 ∪ Def k ⊢ g 7→ A, by Proposition 1 (ii.1),
we have that P0 ∪ Def k ⊢ gα ↓ true. Thus, by Point (1) of Theorem 1, we have
that Pk ⊢ gα ↓ true. Since Pk ⊢ g 7→ B holds, by Proposition 1 (ii.1), there exists
a substitution β ∈ B such that gα is an instance of gβ.
(b) Let β be a substitution in B . From Pk ⊢ g 7→ B , by Proposition 1 (ii.1), we have
that Pk ⊢ gβ ↓ true. From P0 ∪ Def k ⊢ g 7→ A, by Proposition 1 (i), we have that
either P0 ∪ Def k ⊢ gβ ↓ true or P0 ∪ Def k ⊢ gβ ↓ false. Now P0 ∪ Def k ⊢ gβ ↓ false
is impossible because by Point (1) of Theorem 1, we would have Pk ⊢ gβ ↓ false.
Thus, P0 ∪ Def k ⊢ gβ ↓ true. Since P0 ∪ Def k ⊢ g 7→ A, by Proposition 1 (ii.1),
there exists α ∈ A such that gβ is an instance of gα.
(2) We have to prove that if all applications of the goal replacement rule in the
sequence P0 , . . . , Pk are based on strong replacement laws, then P0 ∪ Def k ≡ Pk .
Since P0 ∪ Def k ⊑ Pk has been shown at Point (1) of this proof, it remains to show
that: Pk ⊑ P0 ∪ Def k . The proof is similar to that of Point (1) and it is based on
Point (2) of Theorem 1 and Proposition 1 (ii.1).
Proof of Theorem 3 (Preservation of Safety).
Let hd ← bd be a clause in P0 ∪ Def k and let hd ← newbd be the clause in Pk with
the same head. By Lemma 6 we have that, for every goal context b[ ] such that
vars(b[ ]) ∩ vars(bd , newbd) ⊆ vars(hd ), if b[bd ] is safe in P0 ∪ Def k then b[newbd ]
is safe in P0 ∪ Def k . Then, by Lemma 5, for every goal g, if g is safe in P0 ∪ Def k
then g is safe in Pk .
References
Apt, K. R. 1997. From Logic Programming to Prolog. Prentice Hall, London, UK.
Bossi, A. and Cocco, N. 1994. Preserving universal termination through unfold/fold. In
Proceedings ALP ’94. Lecture Notes in Computer Science 850. Springer-Verlag, Berlin,
269–286.
Bossi, A., Cocco, N., and Etalle, S. 1992. Transforming normal programs by replacement. In Proceedings 3rd International Workshop on Meta-Programming in Logic,
Meta ’92, Uppsala, Sweden, A. Pettorossi, Ed. Lecture Notes in Computer Science 649.
Springer-Verlag, Berlin, 265–279.
Bossi, A., Cocco, N., and Etalle, S. 1996. Transforming left-terminating programs:
The reordering problem. In Logic Program Synthesis and Transformation, Proceedings
LoPSTr ’95, Utrecht, The Netherlands, M. Proietti, Ed. Lecture Notes in Computer
Science 1048. Springer, Berlin, 33–45.

Transformations of Logic Programs with Goals as Arguments

51

Burstall, R. M. and Darlington, J. 1977. A transformation system for developing
recursive programs. Journal of the ACM 24, 1 (January), 44–67.
Chen, W., Kifer, M., and Warren, D. S. 1993. HILOG: A foundation for higher-order
logic programming. Journal of Logic Programming 15, 3, 187–230.
Hill, P. M. and Gallagher, J. 1998. Meta-programming in logic programming. In
Handbook of Logic in Artificial Intelligence and Logic Programming, D. M. Gabbay,
C. J. Hogger, and J. A. Robinson, Eds. Vol. 5. Oxford University Press, Oxford, UK,
421–497.
Jørgensen, J., Leuschel, M., and Martens, B. 1997. Conjunctive partial deduction
in practice. In Logic Program Synthesis and Transformation, Proceedings of LoPSTr
’96, Stockholm, Sweden, J. Gallagher, Ed. Lecture Notes in Computer Science 1207.
Springer-Verlag, Berlin, 59–82.
Lloyd, J. W. 1987. Foundations of Logic Programming. Springer-Verlag, Berlin. Second
Edition.
Nadathur, G. and Miller, D. A. 1998. Higher-order logic programming. In Handbook
of Logic in Artificial Intelligence and Logic Programming, D. M. Gabbay, C. J. Hogger,
and J. A. Robinson, Eds. Vol. 5. Oxford University Press, Oxford, UK, 499–590.
Pettorossi, A. and Proietti, M. 1994. Transformation of logic programs: Foundations
and techniques. Journal of Logic Programming 19,20, 261–320.
Pettorossi, A. and Proietti, M. 1997. Flexible continuations in logic programs via
unfold/fold transformations and goal generalization. In Proceedings of the 2nd ACM
SIGPLAN Workshop on Continuations, January 14, 1997, ENS, Paris (France) 1997,
O. Danvy, Ed. BRICS Notes Series, N6-93-13, Aahrus, Denmark, 9.1–9.22.
Pettorossi, A. and Proietti, M. 2000. Transformation rules for logic programs with
goals as arguments. In Proceedings 9th International Workshop on Logic-based Program
Synthesis and Transformation, LoPSTr ’99, Venezia, Italy, A. Bossi, Ed. Lecture Notes
in Computer Science 1817. Springer, Berlin, 177–196.
Pettorossi, A. and Skowron, A. 1987. Higher order generalization in program derivation. In International Joint Conference on Theory and Practice of Software Development, TAPSOFT ’87. Lecture Notes in Computer Science 250. Springer-Verlag, Berlin,
182–196.
Sands, D. 1996. Total correctness by local improvement in the transformation of functional programs. ACM Toplas 18, 2, 175–234.
Sterling, L. S. and Shapiro, E. 1986. The Art of Prolog. The MIT Press, Cambridge,
Massachusetts.
Tamaki, H. and Sato, T. 1984. Unfold/fold transformation of logic programs. In Proceedings of the Second International Conference on Logic Programming, S.-Å. Tärnlund,
Ed. Uppsala University, Uppsala, Sweden, 127–138.
Tarau, P. 1996. BinProlog 5.25. User Guide. Technical report, University of Moncton,
Moncton, Canada, E1A 3E9.
Tarau, P. and Boyer, M. 1990. Elementary logic programs. In Proceedings PLILP’90,
P. Deransart and J. Maluszyński, Eds. Lecture Notes in Computer Science 456. SpringerVerlag, Berlin, 159–173.
Vasak, T. and Potter, J. 1986. Characterization of terminating logic programs. In
Proceedings of the Third IEEE Int’l Symp. on Logic Programming, Salt Lake City,
Utah. IEEE Comp. Soc. Press, Washington, DC, 140–147.
Wand, M. 1980. Continuation-based program transformation strategies. Journal of the
ACM 27, 1, 164–180.
Warren, D. H. D. 1982. Higher-order extensions to Prolog: are they needed? In Machine
Intelligence, Y.-H. P. J.E. Hayes, D. Michie, Ed. Vol. 10. Ellis Horwood Ltd., Chichester,
441–454.

52

A. Pettorossi and M. Proietti

Winskel, G. 1993. The Formal Semantics of Programming Languages: An Introduction.
The MIT Press, Cambridge, Massachusetts.

