{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:29:29Z","timestamp":1759638569926},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2002,3,25]],"date-time":"2002-03-25T00:00:00Z","timestamp":1017014400000},"content-version":"unspecified","delay-in-days":24,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2002,3]]},"abstract":"<jats:p>It is important that practical data-flow analyzers are backed by reliably proven theoretical \nresults. Abstract interpretation provides a sound mathematical framework and necessary \ngeneric properties for an abstract domain to be well-defined and sound with respect to the \nconcrete semantics. In logic programming, the abstract domain <jats:italic>Sharing<\/jats:italic> is a standard choice \nfor sharing analysis for both practical work and further theoretical study. In spite of this, \nwe found that there were no satisfactory proofs for the key properties of commutativity and \nidempotence that are essential for <jats:italic>Sharing<\/jats:italic> to be well-defined and that published statements \nof the soundness of <jats:italic>Sharing<\/jats:italic> assume the occurs-check. This paper provides a generalization of \nthe abstraction function for <jats:italic>Sharing<\/jats:italic> that can be applied to any language, with or without the \noccurs-check. Results for soundness, idempotence and commutativity for abstract unification \nusing this abstraction function are proven.<\/jats:p>","DOI":"10.1017\/s1471068401001338","type":"journal-article","created":{"date-parts":[[2006,6,2]],"date-time":"2006-06-02T05:36:33Z","timestamp":1149226593000},"page":"155-201","source":"Crossref","is-referenced-by-count":6,"title":["Soundness, idempotence and commutativity of set-sharing"],"prefix":"10.1017","volume":"2","author":[{"given":"PATRICIA M.","family":"HILL","sequence":"first","affiliation":[]},{"given":"ROBERTO","family":"BAGNARA","sequence":"additional","affiliation":[]},{"given":"ENEA","family":"ZAFFANELLA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2002,3,25]]},"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068401001338","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T15:43:44Z","timestamp":1554047024000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068401001338\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S1471068401001338"],"URL":"https:\/\/doi.org\/10.1017\/s1471068401001338","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}