An algebraic approach to sharing analysis of logic programs

This paper describes an algebraic approach to the sharing analysis of logic programs based on an abstract domain of set logic programs. Set logic prog rams are logic programs in which the terms are sets of variables and unific ation is based on an associative, commutative, and idempotent equality theo ry. All of the basic operations required for sharing analyses, as well as t heir formal justification, are based on simple algebraic properties of set substitutions and set-based atoms. An ordering on set-based syntactic objec ts, similar to "less general" on concrete syntactic objects, is shown to re flect the notion of "less sharing" information. The (abstract) unification of a pair of set-based terms corresponds to finding their most general ACI1 unifier with respect to this ordering. The unification of a set of equatio ns between set-based terms is defined exactly as in the concrete case, by s olving the equations one by one and repeatedly applying their solutions to the remaining equations. We demonstrate that all of the operations in a sha ring analysis have natural definitions which are both correct and optimal. (C) 2000 Elsevier Science Inc. All rights reserved.