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 transformation 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 rede ne 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.
Since Kowalski's famous equation \Algorithm = Logic + Control"
A technique known as Compiling Control
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-speci c proofs were required to show that the trace tree represented all possible concrete computations. 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 important 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 de nes 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
particularly close to CC, in that it builds a nite number of nite execution trees from a
partially instantiated input. Like CC, it also synthesizes new programs from these nite
execution trees which respect the semantics of the source program. The correctness
and completeness of partial deduction were formally proven by Lloyd and
Shepherdson
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
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.
The CC-transformation raised challenges for a number of researchers and a range of
competing transformation and synthesis techniques. A rst reformulation of the
CCtransformation was proposed in the context of the \programs-as-proofs" paradigm, in
In
The seminal survey paper on Unfold/Fold transformation,
Advances in Analyzing Coroutines by Abstract Conjunctive Partial Deduction 3
and
In order to illustrate the use of ACPD for the analysis of coroutines, we require a few conventions, as well as an abstract domain.
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 .
The abstract domain consists of two types of new constant symbols: ai and gj, i 2 N0 and j 2 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 speci ed between abstract symbols of the same type. For instance, the abstract conjunction perm(g1; a1); ord(a1) denotes the concrete conjunctions fperm(t1; t2); ord(t2)jt1; t2 2 T ermP ; t1 is groundg.
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 elements of AAtomP .
The complete formalization of our approach requires a sizeable set of abstract operations and is outside the scope of this paper. Because the e ects of these operations can be readily understood, we will simply illustrate the analysis using two examples. The rst of these, permutation sort, ts 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.
Listing 1 contains a Prolog implementation of permutation sort. It de nes 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 rst argument is ground. The program then generates a complete permutation of the ground argument and subsequently checks if the 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]).
a1 = g1 ord(g1) Listing 1: Prolog implementation of permutation sort
sort(g1; a1) perm(g1; a1); ord(a1) g1 = [g2jg3]
a1 = [a2ja3] del(a2; [g2jg3]; a4); perm(a4; a3); ord([a2ja3]) result is ordered. A more e cient approach | though still not e cient 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. fsort(g; a1)g.
Next, we construct a nite number of nite, ACPD derivation trees for abstract (conjunctions of) atoms. The construction of these trees relies on operations for abstract uni cation and abstract resolution.
To specify the control ow, 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([g2ja1]) 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 de nition in the transformed program.
In our setting, however, we want to know the e ect 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
In Figures 1 through 3, in each goal, the atom selected for abstract unfolding is underlined. 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([g4ja3]) 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 di erence 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; g3ja1]), shown in Figure 3.
In Figure 3, the leaf perm(g1; a1); ord([g3ja1]) is a renaming of perm(g1; a1); ord([g2ja1]), which is already contained in A. Therefore, ACPD terminates the analysis, concluding A covers all possible roots for A = fsort(g1; a1); ^(perm(g1; a1); ord([g2ja1])); ^(perm(g1; a1); ord([g2; g3ja1]))g.
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 uni cation. 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 in nite 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 nding a xpoint 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 2 AConAtomP , there exists a concrete conjunction, con 2 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 identi er 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 ful ll the same function as an aliasing index, but within the local scope of a multi abstraction.
The multi abstraction is then de ned as a construct of the form multi(p(C); F irst; Consecutive; Last), where: p(C) is the parameterized conjunction for some C 2 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;j0 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 number of renamings of C. The bindings are used to specify how speci c conjunctions captured Advances in Analyzing Coroutines by Abstract Conjunctive Partial Deduction 7 by the abstraction are bound to their surrounding environment. Speci cally, the F irst bindings indicate how information is shared between the environment and the rst conjunction captured. The subscript \1" used in this set of equalities is a reminder that these equalities pertain to the rst captured conjunction. The Consecutive bindings indicate which values are shared between consecutive conjunctions captured by the abstraction. Because the abstraction represents a linear structure, we can relate values in some conjunction 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 rst 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 rst branch to the right shows how the bindings pass information between the multi abstraction and its environment: When a3 is bound to [g4jg5] in the environment (with g5 the most speci c 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 rst 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 rst 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 nd a xpoint for A and complete the analysis.
We rst presented an earlier version of this research at LOPSTR 2014 and a corresponding
paper was published in
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 rst 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 implementation 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
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 e ects 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.