基于ACI统一的多态类型逻辑程序分析
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification
摘要：
（部分）根据性分析是抽象解释的一个重要应用。有几个建议通过利用类型信息来提高这种分析的精度，包括我们自己与Hill和King的工作，我们已经展示了如何使用程序类型声明中的信息来以精确但固有有限的方式来确定术语的实例化程度。这种方法适用于像Goedel或HAL那样的多态类型程序。在这里，我们重铸这个方法以下的Codish，泻湖和斯塔基的作品。为了形式化我们想要识别的项的哪些属性，我们使用标签函数，这些函数是沿着某些路径从项中提取子项的函数。一个抽象项收集一个项的所有标签函数的结果。对于分析，程序执行的抽象条款，而不是具体的，通常的统一是取代统一模的平等理论，其中包括著名的ACI理论。因此，我们概括了Codish，Lagoon和Stuckey w.r.t.所考虑的类型系统，并相互关联的作品。
英文摘要：
Analysis of (partial) groundness is an important application of abstract interpretation. There are several proposals for improving the precision of such an analysis by exploiting type information, icluding our own work with Hill and King, where we had shown how the information present in the type declarations of a program can be used to characterise the degree of instantiation of a term in a precise and yet inherently finite way. This approach worked for polymorphically typed programs as in Goedel or HAL. Here, we recast this approach following works by Codish, Lagoon and Stuckey. To formalise which properties of terms we want to characterise, we use labelling functions, which are functions that extract subterms from a term along certain paths. An abstract term collects the results of all labelling functions of a term. For the analysis, programs are executed on abstract terms instead of the concrete ones, and usual unification is replaced by unification modulo an equality theory which includes the well-known ACI-theory. Thus we generalise the works by Codish, Lagoon and Stuckey w.r.t. the type systems considered and relate the works among each other.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
