1 Trying to get rid of localities by program transformation

The issue of local variables was not neglected by Sato and Tamaki: the reason why in their seminal paper they restricted the application of the transformational method to horn-closed programs is precisely motivated by the requirement of avoiding universal quantification in the target program. Indeed in the broader picture of the general transformational approach initiated in [1], non-horn closed programs may not occur, as local variables are tried to be eliminated by means of program transformation. The TS and successors system are devoted to the transformation of (even first-order) programs to achieve Prolog executability first and ultimately more efficiency. Of course you have to be a beliver in the classical cycle: logical specification… declarative logic program… program transformation… possibly partial evaluation and eventually compilation. Indeed in the original paper Sato and Tamaki introduced the negation technique to try to compile first-order specification (with what they called the double negation technique that we will not discuss here) into horn-closed programs and later [?] they extended to a general folding-unfolding method.

Therefore the situation is more subtle: nowadays the elimination of localities is not necessarily linked to the negation issue. Local variables can roughly be divided into two large categories:

• local variables that correspond to data structures built by intermediate computation. Consider the typical example of how (not) to average a list of numbers (and its treatment) that can be found in [3]:

Example 1

      average(Xs,A)  :-  length(Xs,L), sumlist(Xs,S), A is S/A.

◇

• variables that ‘read off‘ some local values: see for instance the typing clause for application in λ-calculus.

.

Typically the first case corresponds to sloppy^{1} program writing, namely data structures that are visited more than necessary; so this is a good candidate to optimization, by means of unfolding (more precisely, by unfolding-definition-folding in this order as the title in [4] rhymes). On the other hand the path is perfectly reasonable at first sight.

Thus, unfortunately the situation is not so clear cut: to summarize • Not every eliminable local variables represents an intermediate compu-

1Or ‘declarative’ programming, as you can easily come up with an equivalent linear program by yourself

tation: the path example can be solved by unfolding: The treatment is particularly simple; you just need to unfold the edge predicate until it wires the asserted graph into path. Of course you come up with a program whose size is the double of the number of edges. Then computing the complement of the program is a (tedious) routine.

Example 2

                      path(a,Y)   :-  path(b,Y)
                      path(b,Y)   :-  path(c,Y)

                      path(a,b).
                      path(b,c).

◇

• not every unnecessary computation is represented by a local variable

Note also that the UDF method requires some ingenuity and it is only semimechanical, though a lot of research has been dedicated to the automatic synthesis of eureka predicates, see for example [2]. Moreover, as we exemplified earlier, it may suffer of the usual combinatorial explosion problems typically associated to partial deduction.

Moral: program transformation is not an exhaustive way of getting rid of localities, or in other term, not every local variable can be eliminated in a clean and mechanical. In this case we may want to live with extensional quantification. Since this entails a significant change in the operational semantics of uniform proofs and an additional source of non-determinism, a fair attempt to eliminate localities may be worthwhile (and does not to have necessarily to be made visible to the user)

1.1 Lifting localities

Given the well-known input-output nature of logical variables, an obvious remark is that in certain cases local variables do not need to be local, but maybe brought to the surface, i.e. made to appear in the head of the clause^{2}.

There are a couple of immediate case where the process seems harmless, in the specific sense that the two programs are equivalent w.r.t. an opportune semantics, say the set of computed answer substitutions, restricted to the set of original variables. The real trick is showing equivalence to (finite) failure. My gutsy feeling is positive for the below cases.

1. Hierarchical programs: the absence of recursion make the lifting of localities trivial: for example Example 3

2Compare with the idea of ‘allowed’ program; the question may be whether every program can be rewritten as allowed

 average(Xs,L,S,A)  :-  length(Xs,L), sumlist(Xs,S), A is S/A.

◇

The set of answer substitutions of the lifted program restricted to Xs, A is clearly equivalent to the source’s one.

2. Recursive predicates where lifting does not change the arity: this means that the lifted variables get buried inside some already existing data structure whose arity is then extended; in fact for this notion to be well-defined, we require the exclusion of the creation of new data structures like say X + Y where Y is local.

Example 4 For example, we may change the declaration of application, with the understanding that T 2 is an output variable.

app :  exp -> exp -> tp -> exp.

of (app E1 E2 T2) T1             :-  of E1 T1 => T2 ,of E2 T2.

◇

The general case is more problematic; although the lifted variable is intended to be only output and hence should not affect the computation, it is not clear how to treat recursion. Example 5

      path3(X,Y,Z)  :-  edge(X,Y).
      path3(X,Y,Z)  :-  edge(X,Z), path3(Z,Y,??).

◇

Putting something like Z at ?? is arbitrarious (though seems to preserve the sucess set) and does not mantain finite failure.

References

[1] Tamaki H. & T. Sato. Unfold/Fold Transformations of Logic Program. In/ S.-A. Tarnlund (ed.)Proc. Second Int. Conf. on Logic Programming, pp. 127–139, 1984

[2] Pettorossi A., Proietti M. Synthesis of eureka definitions…

[3] Pettorossi A., Proietti M.: Transformation of logic programs: foundations and techniques. Journal of Logic Programming. 19–20 (1994) 261–321

[4] Pettorossi A., Proietti M. unfolding-definition-folding…