=Paper=
{{Paper
|id=Vol-1433/dc_7
|storemode=property
|title=Advances in Analyzing Coroutines by Abstract
Conjunctive Partial Deduction
|pdfUrl=https://ceur-ws.org/Vol-1433/dc_7.pdf
|volume=Vol-1433
|dblpUrl=https://dblp.org/rec/conf/iclp/Nys15
}}
==Advances in Analyzing Coroutines by Abstract
Conjunctive Partial Deduction==
https://ceur-ws.org/Vol-1433/dc_7.pdf
Technical Communications of ICLP 2015. Copyright with the Authors. 1
Advances in Analyzing Coroutines by Abstract
Conjunctive Partial Deduction
Vincent Nys
submitted 29 April 2015; accepted 5 June 2015
Abstract
The current work describes a technique for the analysis of coroutining in Logic Programs.
This provides greater insight into the execution of Logic Programs and yields a transfor-
mation from programs with nonstandard execution rules to programs with the standard
execution rule of Prolog. A technique known as Compiling Control, or CC for short, was
used to study these issues 30 years ago, but it lacked the tools to formalize a complete
procedure. Abstract Conjunctive Partial Deduction, introduced by Leuschel, provides an
appropriate setting to redefine Compiling Control for simple examples. For more elaborate
examples, we extend Leuschel’s framework with a new operator. Preliminary experiments
with the new operator show that a wide range of programs can be analyzed, opening up
possibilities for further analysis as well as program optimization.
1 Introduction
Since Kowalski’s famous equation “Algorithm = Logic + Control” (Kowalski 1979), much
research has been done into separating the logic of a program from its control. Ideally, logic
programs should be written in a purely declarative style. The control flow aspect would be
specified separately to obtain an efficient execution. To this end, many Logic Programming
systems, such as SWI Prolog (Wielemaker et al. 2012), Ciao (Bueno et al. 1997) and Gödel
(Hill and Lloyd 1994) support delay statements. Delay statements allow the programmer
to override the default resolution strategy and specify which atoms should be resolved in
particular program contexts, e.g. as soon as a program variable becomes ground. The use
of delay statements causes atoms to behave as coroutines, in that their execution may
be suspended and then later resumed, enabling intricate forms of data communication
between atoms. However, the use of separate control flow statements brings with it runtime
overhead. It also prevents the use of program analysis and program optimization techniques
developed for logic programs under a left-to-right execution rule.
A technique known as Compiling Control (Bruynooghe et al. 1989) allows for the separa-
tion of logic and control, while avoiding the drawbacks of delay statements. The technique
takes a source program, P , and synthesizes a program P 0 , so that computation with P 0
under left-to-right execution mimics the computation with P under a non-standard selec-
tion rule. To do this, Compiling Control (CC) consists of two phases: an analysis phase
and a synthesis phase. The analysis phase analyzes the computations of a program for a
given query pattern under a (non-standard) selection rule. The query pattern is expressed
in terms of a combination of type, mode and aliasing information. The analysis results in
what is called a “trace tree”, which is a finite upper part of a symbolic execution tree that
one can construct for the given query pattern, selection rule and program. In the synthesis
phase, a finite number of clauses, the resolvents, are generated. Each clause synthesizes
the computation in some branch of the trace tree and all computations in the trace tree
2 Vincent Nys
have been synthesized by some clause. The technique was implemented, formalized and
proven correct, under certain fairly technical conditions.
Despite this, CC is a rather ad hoc approach. The connection between symbolic values
and values in a concrete program was never made explicit. Furthermore, program-specific
proofs were required to show that the trace tree represented all possible concrete compu-
tations. The aim of this research is to reformulate CC in a way that allows for a rigorous
analysis of its correctness and completeness. Since the original work on CC, several im-
portant advances in program analysis and transformation have been made:
• General frameworks for Abstract Interpretation in Logic Programming were developed.
Abstract Interpretation can formalize the notion of a “symbolic computation” used in
CC. Notably, it defines an abstraction function and a concretization function to relate
abstract program executions to concrete executions.
• Partial Deduction of Logic Programs was developed. Partial Deduction seems partic-
ularly close to CC, in that it builds a finite number of finite execution trees from a
partially instantiated input. Like CC, it also synthesizes new programs from these finite
execution trees which respect the semantics of the source program. The correctness
and completeness of partial deduction were formally proven by Lloyd and Shepherd-
son (Lloyd and Shepherdson 1991). However, standard Partial Deduction assumes the
roots of its execution trees to be atoms, while coroutines are more effectively analyzed
together.
• Conjunctive Partial Deduction lifts the restriction that execution trees must start from
atoms. This allows it to analyze conjunctions, preserving interactions which cannot be
captured by Partial Deduction.
• Abstract Conjunctive Partial Deduction (Leuschel 2004), or ACPD for short, brings
the features of the above techniques together. It provides an extension of (Conjunctive)
Partial Deduction in which the analysis is based on Abstract Interpretation, rather
than on concrete evaluation.
Our aim is to recast CC as a form of Abstract Conjunctive Partial Deduction. Such
a reformulation has two major advantages: First, it provides a framework in which the
execution of coroutining Logic Programs can be better understood. Second, it enables a
transformation to from programs with delay statements to pure logic programs, allowing
for additional analysis and optimization. We show that, for simple examples, recasting the
approach is possible. For more complex examples, an extension to ACPD is required to
overcome one of the restrictions in its original formulation.
2 Related work
The CC-transformation raised challenges for a number of researchers and a range of
competing transformation and synthesis techniques. A first reformulation of the CC-
transformation was proposed in the context of the “programs-as-proofs” paradigm, in
(Wiggins 1990). It was shown that CC-transformations, to a limited extent, could be
formalized in a proof-theoretic program synthesis context.
In (Boulanger et al. 1993), the CC-transformation was revisited on the basis of a com-
bination of Abstract Interpretation and constraint processing. This improved the formal-
ization of the technique, but it did not clarify the relation with Partial Deduction.
The seminal survey paper on Unfold/Fold transformation, (Pettorossi and Proietti
1994), showed that basic CC-transformations are well in the scope of Unfold/Fold transfor-
mation. In later works (e.g. (Pettorossi and Proietti 2002)), the same authors introduced
list-introduction into the Unfold/Fold framework, whose function is very similar to that of
the multi abstraction in our approach. Also related to our work are (Puebla et al. 1997),
providing alternative transformations to improve the efficiency of dynamic scheduling,
Advances in Analyzing Coroutines by Abstract Conjunctive Partial Deduction 3
and (Vidal 2011) and (Vidal 2012), which also provide a hybrid form of partial deduction,
combining abstract and concrete levels.
3 Concepts
In order to illustrate the use of ACPD for the analysis of coroutines, we require a few
conventions, as well as an abstract domain.
3.1 Conventions
Given a program P , F unP and P redP respectively denote the sets of all functors and
predicate symbols in the language underlying P . T ermP will denote the set of all terms
belonging to the concrete domain. AtomP denotes the set of all atoms which can be
constructed from P redP and T ermP . We refer to the set of conjunctions of atoms from
AtomP as ConAtomP .
3.2 Abstract Domain
The abstract domain consists of two types of new constant symbols: ai and gj , i ∈ N0
and j ∈ N0 . The basic intuition for the symbols ai is that they represent any term of the
concrete language. The symbols gj denote any ground term in the concrete language.
The subscripts i and j in ai and gj are used to represent aliasing. If an abstract term,
abstract atom or abstract conjunction of atoms contains ai or gj several times (with the
same subscript), the denoted concrete terms, atoms or conjunctions of atoms contain the
same term in all positions corresponding to those respectively occupied by ai and gj . If
an abstract term contains subterms ak and gk , where k is some element of N0 , this has no
particular meaning: aliasing can only be specified between abstract symbols of the same
type. For instance, the abstract conjunction perm(g1 , a1 ), ord(a1 ) denotes the concrete
conjunctions {perm(t1 , t2 ), ord(t2 )|t1 , t2 ∈ T ermP , t1 is ground}.
Based on these two types of abstract constants, there is a set of abstract terms AT ermP ,
consisting of terms which can be constructed from the abstract constants and F unP .
AAtomP will denote the set of abstract atoms, being the atoms which can be constructed
from AT ermP and P redP . Finally, AConAtomP denotes the set of conjunctions of ele-
ments of AAtomP .
4 Examples
The complete formalization of our approach requires a sizeable set of abstract operations
and is outside the scope of this paper. Because the effects of these operations can be readily
understood, we will simply illustrate the analysis using two examples. The first of these,
permutation sort, fits within Leuschel’s original framework. The second, sameleaves, does
not. However, an extension to Leuschel’s framework makes it possible to deal with a larger
class of programs to which sameleaves belongs.
4.1 Permutation sort
Listing 1 contains a Prolog implementation of permutation sort. It defines the sorting
operation as a random permutation, followed by a test to see whether the result is ordered.
Assume an initial sort/2 query in which the first argument is ground. The program then
generates a complete permutation of the ground argument and subsequently checks if the
4 Vincent Nys
sort(X,Y) :- perm(X,Y), ord(Y).
perm([],[]).
perm([X|Y],[U|V]) :- del(U,[X|Y],W),perm(W,V).
del(X,[X|Y],Y).
del(X,[Y|U],[Y|V]) :- del(X,U,V).
ord([]).
ord([X]).
ord([X,Y|Z]) :- X =< Y, ord([Y|Z]).
Listing 1: Prolog implementation of permutation sort
sort(g1 , a1 )
perm(g1 , a1 ), ord(a1 )
g1 = [g2 |g3 ]
a1 = g1 a1 = [a2 |a3 ]
ord(g1 ) del(a2 , [g2 |g3 ], a4 ), perm(a4 , a3 ), ord([a2 |a3 ])
a2 = g4
a4 = g5
perm(g5 , a3 ), ord([g4 |a3 ])
Figure 1: Abstract tree for sort(g1 , a1 )
result is ordered. A more efficient approach — though still not efficient in an absolute
sense — is to interleave the generation of the permutation with the check for ordering.
Each time an element is added to the permutation, it can be compared to its predecessor
(if any). If the check fails, there is no point in completing the permutation.
ACPD requires a top-level abstract atom (or conjunction) to start the transformation.
Let sort(g, a1 ) be this atom. As in standard partial deduction, we initialize a set of analyzed
roots A as the singleton set of the top-level query, i.e. {sort(g, a1 )}.
Next, we construct a finite number of finite, ACPD derivation trees for abstract (con-
junctions of) atoms. The construction of these trees relies on operations for abstract
unification and abstract resolution.
To specify the control flow, we assume an “oracle” which decides on the selection rule
applied in the abstract derivation trees. This oracle has three functions:
• to decide whether an obtained goal should be unfolded further, or whether it should
be kept residual (to be split and added to A).
perm(g1 , a1 ), ord([g2 |a1 ])
a1 = g1 g1 = [g3 |g4 ]
a1 = [a2 |a3 ]
ord([g2 |g1 ]) del(a2 , [g3 |g4 ], a4 ), perm(a4 , a3 ), ord([g1 , a2 |a3 ])
a2 = g5
a4 = g6
perm(g6 , a3 ), ord([g1 , g5 |a3 ])
Figure 2: Abstract tree for perm(g1 , a1 ), ord([g2 |a1 ])
Advances in Analyzing Coroutines by Abstract Conjunctive Partial Deduction 5
perm(g1 , a1 ), ord([g2 , g3 |a1 ])
perm(g1 , a1 ), g2 ≤ g3 , ord([g3 |a1 ])
perm(g1 , a1 ), ord([g3 |a1 ])
Figure 3: Abstract tree for perm(g1 , a1 ), ord([g2 , g3 |a1 ])
perm(X, Y ), ord([Z|Y ])
X = [] X = [X1 |X2 ]
Y = [] Y = [U |V ]
ord([Z]) del(U, [X1 |X2 ], W ), perm(W, V ), ord([Z, U |V ])
Figure 4: Concrete tree corresponding to Figure 2
• to decide which atom of the current goal should be selected for unfolding.
• to decide whether to “fully evaluate” a selected atom.
The third type of decision is not commonly supported in partial deduction. What it
means is that we decide not to transform a certain predicate of the original program, but
merely keep its original definition in the transformed program.
In our setting, however, we want to know the effect that solving the atom has on the
remainder of the goal. Therefore, we assume that a full abstract interpretation over our
abstract domain computes the abstract bindings that solving the atom results in. These are
applied to the remainder of the goal. In (Vidal 2011), a similar functionality is integrated
in a hybrid approach to conjunctive partial deduction.
In Figures 1 through 3, in each goal, the atom selected for abstract unfolding is under-
lined. If an atom is underlined twice, this expresses that the atom was selected for full
abstract interpretation.
Both unfolding and full abstract evaluation may create bindings. These are indicated
next to the branches of the derivation trees.
A goal with no underlined atom indicates that the oracle selects no atom and decides
to keep the conjunction residual. After the construction of the tree in Figure 1, ACPD
adds the abstract conjunction perm(g5 , a3 ), ord([g4 |a3 ]) to A. ACPD starts a new tree for
(a renaming of) this atom. This tree is shown in Figure 2.
The tree looks similar to the one in Figure 1 without its root. The main difference is
that, in the residual leaf of the second tree, the ord atom now has a list argument with
two g elements. This pattern does not yet exist in the current A and is therefore added to
A. A third abstract tree is computed for perm(g1 , a1 ), ord([g2 , g3 |a1 ]), shown in Figure 3.
In Figure 3, the leaf perm(g1 , a1 ), ord([g3 |a1 ]) is a renaming of perm(g1 , a1 ), ord([g2 |a1 ]),
which is already contained in A. Therefore, ACPD terminates the analysis, concluding A
covers all possible roots for A = {sort(g1 , a1 ), ∧(perm(g1 , a1 ), ord([g2 |a1 ])), ∧(perm(g1 , a1 ),
ord([g2 , g3 |a1 ]))}.
In concrete conjunctive partial deduction, the analysis phase would now be completed.
In ACPD, however, we need an additional step. In the abstract derivation trees, we have
not collected the concrete bindings that unfolding would produce. These are required to
generate the resolvents. Therefore, we need an additional step, constructing essentially the
same three trees again by resolving the same clauses, but now using concrete terms and
concrete unification.
6 Vincent Nys
We only show one of these concrete derivation trees in Figure 4.
4.2 Sameleaves
sameleaves(T1,T2) :- collect(T1,T1L),collect(T2,T2L),eq(T1L,T2L).
eq([],[]).
eq([H|T1],[H|T2]) :- eq(T1,T2).
collect(node(X),[X]).
collect(tree(L,R),C) :- collect(L,CL), collect(R,CR), append(CL,CR,C).
append([],L,L).
append([H|T],L,[H|TR]) :- append(T,L,TR).
Listing 2: Prolog implementation of Sameleaves
Listing 2 shows a program which cannot be analyzed using the technique outlined above.
Assume a top-level query of the form sameleaves(g1 , g2 ). Trying to analyze this program
in the same way as the permutation sort program leads to an infinite derivation. This
is due to the fact that trees may be nested to an arbitrary depth. Adding each newly
derived conjunction to A would prevent the procedure from finding a fixpoint for A. We
could solve this by cutting the goal into two smaller conjunctions and adding these to A.
However, all these atoms behave as generators or testers and depend on each other. By
splitting the conjunction, we would no longer be able to analyze the coroutining behaviour.
One of the restrictions imposed by ACPD is that for any abstract conjunction of atoms,
acon ∈ AConAtomP , there exists a concrete conjunction, con ∈ ConAtomP , such that any
instantiation of acon is also an instance of con. In practice, this means that an abstract
conjunction is not allowed to represent a set of concrete conjunctions whose elements
have a distinct number of conjuncts. However, in order to solve the problem observed
in our example, we need the ability to represent conjunctions with a growing number
of atoms by an abstract conjunct. Therefore, we need to extend ACPD. We introduce a
new abstraction, multi, which makes it possible to represent growing conjunctions with a
repeating internal structure.
To specify the relationship of an abstracted set of conjunctions with the surrounding
context, as well as its internal structure, we introduce the “parameterized renaming”.
The parameterized renaming of a conjunction C is obtained by replacing every aj or gk
occurring in C by its respective parameterized naming, aId,i,j or gId,i,k . Here, Id is a
unique identifier for the multi abstraction with which the renaming will be associated, as
several multi abstractions may be needed to complete the analysis. The i is symbolic and
is used to specify data shared between abstracted conjunctions. Finally, j and k fulfill the
same function as an aliasing index, but within the local scope of a multi abstraction.
The multi abstraction is then defined as a construct of the form multi(p(C), F irst,
Consecutive, Last), where:
• p(C) is the parameterized conjunction for some C ∈ AConAtomP .
• F irst is a conjunction of equalities aId,1,j = bj and gId,1,k , where bj and bk occur
outside the abstraction and all left-hand sides of the equalities are distinct.
• Consecutive is a conjunction of equalities aId,i+1,j = aId,i,j 0 and gId,i+1,k = gId,i,k0 ,
where all left-hand sides of the equalities are distinct.
• Last is a conjunction of equalities aId,L,j = bj and gId,L,k = bk , where bj and bk occur
outside the abstraction occurs and all left-hand sides of the equalities are distinct.
Inside this abstraction, the parameterized renaming p(C) represents an arbitrary num-
ber of renamings of C. The bindings are used to specify how specific conjunctions captured
Advances in Analyzing Coroutines by Abstract Conjunctive Partial Deduction 7
sameleaves(g1 , g2 ) sameleaves(g1 , g2 )
collect(g1 , a1 ), collect(g2 , a2 ), eq(a1 , a2 ) collect(g1 , a1 ), collect(g2 , a2 ), eq(a1 , a2 )
g1 = tree(g3 , g4 ) g = tree(g3 , g4 )
collect(g3 , a3 ), collect(g4 , a4 ), append(a3 , a4 , a1 ), collect(g3 , a3 ), collect(g4 , a4 ), append(a3 , a4 , a1 ),
collect(g2 , a2 ), eq(a1 , a2 ) collect(g2 , a2 ), eq(a1 , a2 )
g3 = tree(g5 , g6 )
collect(g3 , a3 ), multi(∧(collect(g1,i,4 , a1,i,4 ), append(a1,i,3 , a1,i,4 , a1,i,1 )),
collect(g5 , a5 ), collect(g6 , a6 ), append(a5 , a6 , a3 ), {a1,1,3 = a3 }, {a1,i+1,3 = a1,i,1 }, {a1,L,1 = a1 }),
collect(g4 , a4 ), append(a3 , a4 , a1 ), collect(g2 , a2 ), eq(a1 , a2 ) collect(g, a2 ), eq(a1 , a2 )
Figure 5: Infinite derivation strategy for sameleaves Figure 6: Generalization to multi
collect(g3 , a3 ),
multi(∧(collect(g1,i,4 , a1,i,4 ), append(a1,i,3 , a1,i,4 , a1,i,1 )),
{a1,1,3 = a3 },
{a1,i+1,3 = a1,i,1 },
{a1,L,1 = a1 }),
collect(g2 , a2 ), eq(a1 , a2 )
g3 = node(g4 )
g3 = tree(g4 , g5 ) a3 = [g4 |g5 ]
multi(∧(collect(g1,i,4 , a1,i,4 ), append(a1,i,3 , a1,i,4 , a1,i,1 )),
collect(g4 , a4 ), collect(g5 , a5 ), append(a4 , a5 , a3 ), {a1,1,3 = [g4 |g5 ]},
multi(∧(collect(g1,i,4 , a1,i,4 ), append(a1,i,3 , a1,i,4 , a1,i,1 )), {a1,i+1,3 = a1,i,1 },
{a1,1,3 = a3 }, {a1,L,1 = a1 }),
{a1,i+1,3 = a1,i,1 }, collect(g2 , a2 ), eq(a1 , a2 )
{a1,L,1 = a1 })
collect(g2 , a2 ), eq(a1 , a2 ) unfold: single
collect(g6 , a5 ), append([g4 |g5 ], a5 , a1 ),
collect(g2 , a2 ), eq(a1 , a2 ) unfold: multiple
collect(g4 , a4 ),
multi(∧(collect(g1,i,4 , a1,i,4 ), append(a1,i,3 , a1,i,4 , a1,i,1 )),
{a1,1,3 = a4 },
{a1,i+1,3 = a1,i,1 },
{a1,L,1 = a1 }), collect(g6 , a5 ), append([g4 |g5 ], a5 , a6 ),
collect(g2 , a2 ), eq(a1 , a2 ) multi(∧(collect(g1,i,4 , a1,i,4 ), append(a1,i,3 , a1,i,4 , a1,i,1 )),
{a1,1,3 = a6 },
{a1,i+1,3 = a1,i,1 },
{a1,L,1 = a1 }),
collect(g2 , a2 ), eq(a1 , a2 )
Figure 7: Generalization of multi (left branch) and unfolding of multi (right branches)
by the abstraction are bound to their surrounding environment. Specifically, the F irst
bindings indicate how information is shared between the environment and the first con-
junction captured. The subscript “1” used in this set of equalities is a reminder that these
equalities pertain to the first captured conjunction. The Consecutive bindings indicate
8 Vincent Nys
which values are shared between consecutive conjunctions captured by the abstraction.
Because the abstraction represents a linear structure, we can relate values in some con-
junction i to those in its successor, i + 1. The Last bindings are similar to the F irst
bindings, but pertain to the last rather than the first captured conjunction. The subscript
“L” is also a reminder of the conjunction to which these bindings apply.
The problem of a growing recursion is illustrated in Figure 5 and generalization using
the multi abstraction is shown in Figure 6. Because the subconjunction collect(g3 , a3 ),
collect(g4 , a4 ), append(a3 , a4 , a5 ) obeys a pattern common to all growing conjunctions,
the recursion can be detected algorithmically. After generalization, the leaf of Figure
6 is added to A in the standard way. The left branch of Figure 7 demonstrates how
further unfolding followed by generalization can lead back to a renaming of this state.
The first branch to the right shows how the bindings pass information between the multi
abstraction and its environment: When a3 is bound to [g4 |g5 ] in the environment (with
g5 the most specific abstraction of the empty list), it also becomes bound in the F irst
bindings. The second level of branching shows how the multi abstraction is unfolded:
In the first case, it represents a single conjunction to which both the F irst and Last
bindings are applied. In the second, it represents a larger conjunction whose first abstracted
subconjunction is moved outside the abstraction. The current F irst bindings are applied
to this subconjunction and new F irst bindings are then computed based on the current
Consecutive bindings.
The complete analysis of sameleaves is considerably longer and involves some interesting
patterns of computation. However, the operations shown are enough find a fixpoint for A
and complete the analysis.
5 Current status
We first presented an earlier version of this research at LOPSTR 2014 and a corresponding
paper was published in (De Schreye et al. 2014). An extended journal paper was submitted
at the end of June, 2015. The latter version contains the formalizations for most of the
operations illustrated by example in this paper. It details an earlier variant of the multi
abstraction discussed here, which could not yet represent the growing sequence of atoms
found in the sameleaves program. The variant discussed here can do this, because it
abstracts linearly growing sequences of abstract conjunctions, rather than linearly growing
sequences of atoms. We conjecture that the abstraction is now general enough to deal with
any growing sequence of abstract atoms under an instantiation-based computation rule.
We have applied the technique to analyze a range of well-known “toy” problems, notably
the permutation sort, graph coloring, prime generator, N-queens and sameleaves example.
A manually synthesized standard Prolog program based on this analysis is available for the
first four problems. Such a synthesis can also be performed for the sameleaves program.
The reason it has not yet been written is simply because the analysis is quite long.
To demonstrate that the approach can be automated, we have developed an imple-
mentation which performs the complete analysis phase. It requires the user to specify the
decisions made by the oracle: For the selection rule, it uses delay declarations. For the
calls which require a full evaluation, it requires the user to map an atom to be solved onto
an output atom. Also, the analyzer requires the user to specify which conjunctions should
be generalized into a multi abstraction. This is done using a grammar of conjunctions,
with each conjunction produced by the grammar a possible instantiation of the multi
abstraction. With this information, the analyzer is capable of performing the complete
analysis phase for any example we have found, including the sameleaves program.
Advances in Analyzing Coroutines by Abstract Conjunctive Partial Deduction 9
6 Future work
First and foremost, we want to investigate the generality of the multi abstraction. No
examples which give rise to nested multi abstractions have been examined yet. These are
certain to occur in complex, real-world programs. Likewise, use of the multi abstraction to
represent disjunctions as well as conjunctions is a worthwhile avenue for future research.
Eventually, we hope to formally characterize the class of programs which can be analyzed
using our approach.
We also plan to re-examine ACPD as formulated by Leuschel, in order to fully integrate
the multi abstraction. In this way, we hope to retain all correctness results of ACPD for
the analysis and compilation of coroutines in full generality.
Improvements to the implementation can also be made. We hope to integrate the current
prototype with an existing system for abstract interpretation. This should free the user
from the need to specify the effects of a full evaluation of abstract atoms. Similarly, we
would like to investigate how the grammatical description of growing conjunctions can be
derived automatically. With both improvements, the entire analysis and synthesis could be
done algorithmically using only the program source code and delay statements. We believe
this will open up interesting new paths for further program analysis and optimization.
References
Boulanger, D., Bruynooghe, M., and De Schreye, D. 1993. Compiling control revis-
ited: A new approach based upon abstract interpretation for constraint logic programs.
In LPE. 39–51.
Bruynooghe, M., De Schreye, D., and Krekels, B. 1989. Compiling control. The
Journal of Logic Programming 6, 1, 135–162.
Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M., López-Garcıa, P., and
Puebla, G. 1997. The ciao prolog system. Reference Manual. The Ciao System Doc-
umentation Series–TR CLIP3/97.1, School of Computer Science, Technical University
of Madrid (UPM) 95, 96.
De Schreye, D., Nys, V., and Nicholson, C. 2014. Analysing and compiling coroutines
with abstract conjunctive partial deduction. In Logic-Based Program Synthesis and
Transformation. Springer, 21–38.
Hill, P. and Lloyd, J. W. 1994. The Gödel programming language. MIT press.
Kowalski, R. 1979. Algorithm=logic+ control. Communications of the ACM 22, 7,
424–436.
Leuschel, M. 2004. A framework for the integration of partial evaluation and abstract
interpretation of logic programs. ACM Transactions on Programming Languages and
Systems (TOPLAS) 26, 3, 413–463.
Lloyd, J. W. and Shepherdson, J. C. 1991. Partial evaluation in logic programming.
The Journal of Logic Programming 11, 3, 217–242.
Pettorossi, A. and Proietti, M. 1994. Transformation of logic programs: Foundations
and techniques. The Journal of Logic Programming 19, 261–320.
Pettorossi, A. and Proietti, M. 2002. The list introduction strategy for the derivation
of logic programs. Formal aspects of computing 13, 3-5, 233–251.
Puebla, G., de la Banda, M. J. G., Marriott, K., and Stuckey, P. J. 1997. Opti-
mization of logic programs with dynamic scheduling. In ICLP. Vol. 97. 93–107.
Vidal, G. 2011. A hybrid approach to conjunctive partial evaluation of logic programs.
In Logic-Based Program Synthesis and Transformation, M. Alpuente, Ed. Lecture Notes
in Computer Science, vol. 6564. Springer Berlin Heidelberg, 200–214.
10 Vincent Nys
Vidal, G. 2012. Annotation of logic programs for independent and-parallelism by partial
evaluation. Theory and Practice of Logic Programming 12, 4-5, 583–600.
Wielemaker, J., Schrijvers, T., Triska, M., and Lager, T. 2012. Swi-prolog. Theory
and Practice of Logic Programming 12, 1-2, 67–96.
Wiggins, G. A. 1990. The improvement of prolog program efficiency by compiling control:
A proof-theoretic view. Department of Artificial Intelligence, University of Edinburgh.