论共享与线性性之间的交互
编程语言
2012-10-09 v2 计算机科学中的逻辑
摘要
在逻辑程序分析中，用于检测共享和线性性信息的抽象域被广泛使用。为此类域设计抽象合一算法已被证明相当困难。目前可用的算法虽然正确但并非最优，即它们无法充分利用抽象域所传达的信息。本文定义了一个新的（无限）域 ShLin-w，可将其视为一个通用框架，其他域可通过抽象从中轻松导出。ShLin-w 使共享与线性性之间的交互显式化。我们提供了 ShLin-w 上最优抽象合一算子的构造性刻画，并将其提升（lift）到 ShLin-w 的两个著名抽象：即经典的 Sharing X Lin 抽象域，以及由 Andy King 提出的更精确的 ShLin-2 抽象域。在单绑定替换的情况下，我们获得了这些域的最优抽象合一算法。本文将发表于《逻辑编程理论与实践》(TPLP)。
引用
@article{arxiv.0710.0528,
title = {On the interaction between sharing and linearity},
author = {Gianluca Amato and Francesca Scozzari},
journal= {arXiv preprint arXiv:0710.0528},
year = {2012}
}