Description:
<jats:p>It is important that practical data-flow analyzers are backed by reliably proven theoretical
results. Abstract interpretation provides a sound mathematical framework and necessary
generic properties for an abstract domain to be well-defined and sound with respect to the
concrete semantics. In logic programming, the abstract domain <jats:italic>Sharing</jats:italic> is a standard choice
for sharing analysis for both practical work and further theoretical study. In spite of this,
we found that there were no satisfactory proofs for the key properties of commutativity and
idempotence that are essential for <jats:italic>Sharing</jats:italic> to be well-defined and that published statements
of the soundness of <jats:italic>Sharing</jats:italic> assume the occurs-check. This paper provides a generalization of
the abstraction function for <jats:italic>Sharing</jats:italic> that can be applied to any language, with or without the
occurs-check. Results for soundness, idempotence and commutativity for abstract unification
using this abstraction function are proven.</jats:p>