  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 Sharing 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 Sharing to be well-defined
and that published statements of the soundness of Sharing assume the
occurs-check. This paper provides a generalization of the abstraction function
for Sharing 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.
