Soundness, idempotence and commutativity of set-sharing

It is important that practical data-flow analyzers are backed by reliably proven theoretical Abstract interpretation provides a sound mathematical framework and necessary properties for an abstract domain to be well-defined and sound with respect to rete 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 zation 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 ract unification using this abstraction function are proven.

• Type: Journal
• Year: 2002
• Where: TPLP
• Authors: Patricia M. Hill, Roberto Bagnara, Enea Zaffanella
• Keywords: Abstract Domain, Sharing, Theoretical Abstract Interpretation, TPLP 2002