Author:

Abstract:

For a given program and query pattern (formulated as a precondition on permitted queries) the authors present an algorithm which constructs an AND/OR tree with the query as root, where each call is labeled with a precondition and a postcondition. Conditions which are sufficient for the algorithm to terminate and conditions which are sufficient for the pre- and postconditions to be correct are given, to guarantee that when executing a query, each executed call corresponds to a call in the finite AND/OR tree and satisfies the precondition on entry and the postcondition on exit. Three applications of the abstract interpretation theorem are given, allowing type, mode, and aliasing information to be inferred for all clauses in the program. It is suggested that these three applications can be combined into an optimizing compiler for pure Prolog. It is shown to be important that the aliasing information allow overwriting the data structures, thereby yielding a memory usage which is identical to the memory usage of a similar program in a conventional imperative language.