Conjunctive partial deduction: foundations, control, algorithms, and experiments

Partial deduction in the Lloyd-Shepherdson framework cannot achieve certain optimisations which are possible by unfold/fold transformations. We introd uce conjunctive partial deduction, an extension of partial deduction accomm odating such optimisations, e.g., tupling and deforestation, We first prese nt a framework for conjunctive partial deduction, extending the Lloyd-Sheph erdson framework by considering conjunctions of atoms (instead of individua l atoms) for specialisation and renaming. Correctness results are given for the framework with respect to computed answer semantics, least Herbrand mo del semantics, and finite failure semantics, Maintaining the well-known dis tinction between local and global control, we describe a basic algorithm fo r conjunctive partial deduction, and refine it into a concrete algorithm fo r which we prove termination, The problem of finding suitable renamings whi ch remove redundant arguments turns out to be important, so we give an inde pendent technique for this. A fully automatic implementation has been under taken, which always terminates, Differences between the abstract semantics and Prolog's left-to-right execution motivate deviations from the abstract technique in the actual implementation, which we discuss. The implementatio n has been tested on an extensive set of benchmarks which demonstrate that conjunctive partial deduction indeed pays off, surpassing conventional part ial deduction on a range of small to medium-size programs, while remaining manageable in an automatic and terminating system. (C) 1999 Elsevier Scienc e Inc. All rights reserved.