The Correctness of Set-Sharing

It is important that practical data flow analysers are backed bly 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 conmantics. 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 safeness property assumed the occur-check. This paper provides a sation of the abstraction function for Sharing that can be applied to any language, with or without the occur-check. The results for safeempotence and commutativity for abstract unification using this ion function are given.

• Type: Conference
• Year: 1998
• Where: AGP
• Authors: Patricia M. Hill, Roberto Bagnara, Enea Zaffanella
• Keywords: Abstract Domain, Abstract Domain Sharing, AGP 1998, Artificial Intelligence, Sharing