Freeness, sharing, linearity and correctness | all at once

emaih mauriceOcs.kuleuven.ac.be Abst ract. The availability of freeness and sharing information for logic pro-grams has proven useful in a wide variety of applications. However, deriving correct freeness and sharing information turns out to be a complex task. In a recent paper, Codish et al. introduce a domain of abstract equation systems and illustrate the systematic derivation of an abstract unification algorithm for sharing and freeness. This paper follows the same approach, and using a more detailed abstraction, develops a more powerful transition system. The resulting algorithm is more prone to efficient implementation asit computes a single abstract solved form which exhibits sharing, freeness, groundness and linearity information. 1 In t roduct ion The aim of possible sharing analysis of a logic program P is to identify independent variables in a clause of P. A set of variables is said to be independeng if no compu-tat ion binds them to terms which contain a common variable. Groundness, l inearit