集共享的合理性、恒等性和交换性
Soundness, Idempotence and Commutativity of Set-Sharing
摘要：
重要的是，实际的数据流分析器必须有可靠的理论结果支持。抽象解释提供了一个健全的数学框架和必要的通用属性的一个抽象领域是明确的和健全的具体语义。在逻辑程序设计中，抽象域共享是共享分析的标准选择，无论是在实际工作中还是在进一步的理论研究中。尽管如此，我们发现，没有令人满意的证明的关键属性的交换性和恒等式是必不可少的共享是明确的，并发表声明的合理性共享假设发生检查。本文提供了一个概括的抽象功能共享，可以应用于任何语言，或没有发生检查。证明了使用该抽象函数的抽象统一的可靠性、恒等性和交换性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
