最内层重写的可达性分析

我们考虑给定描述函数式程序输入的文法、推断描述其输出文法的问题。该问题的解有助于检测函数式程序的错误或者证明其安全性质，并且已有若干重写工具用于解决此问题。然而，已知的文法推断技术无法考虑程序的求值策略。这在求值策略起作用时会产生非常不精确的结果。在本工作中，我们调整树自动机补全算法，以精确近似由最内层策略下重写可达的项集合。我们形式化地证明了所提出的技术关于最内层重写是可靠且精确的。我们展示了这些结果可以推广到最左最内层与最右最内层的情况。针对一般最内层情况的算法已在 Timbuk 可达性工具中实现。实验表明，对于使用按值调用求值策略的函数式程序，它显著提高了静态分析的精度。