Several proposals for computing freeness information for logic program
s have been put forward in the recent literature. The availability of
such information has proven useful in a variety of applications, inclu
ding parallelization of Prolog programs, optimizations in Prolog compi
lers, as well as for improving the precision of other analyses. While
these proposals have illustrated the importance of such analyses, they
lack formal justification. Moreover, several have been found incorrec
t. This paper introduces a novel domain of abstract equation, systems
describing possible sharing and definite freeness of terms in a system
of equations. A simple and intuitive abstract unification algorithm i
s presented, providing the core of a correct and precise sharing and f
reeness analysis for logic programs. Our contribution is not only a co
rrect algorithm, but perhaps primarily, the application of a systemati
c approach in which it is derived by mimicking each step in a suitable
concrete unification algorithm. Consequently, the abstract algorithm
is intuitive-as it resembles the concrete algorithm. It is amenable to
formal justification-as the proof of correctness is reduced to showin
g that each step in the concrete algorithm is mimicked by a correspond
ing step in the abstract algorithm. Finally, it is precis as each step
mimics only those situations which can arise in the concrete algorith
m.