一句话：将树自动机补全算法扩展到 innermost 重写策略，以精确近似可达项集合，并在 Timbuk 中实现验证。
本文研究在给定输入语法时推断函数式程序输出语法的问题，即重写系统可达项集合的静态近似。已有语法推断方法忽略求值策略，在策略影响结果时精度不足。作者将 Tree Automata Completion 算法适配到 innermost 重写策略，用树自动机补全过程近似最内层重写可达的项集合，并证明该技术相对于 innermost 重写是可靠且精确的；结果还可扩展到最左和最右 innermost 情形。算法已在 Timbuk 可达性工具中实现，实验表明其显著提升了采用 call-by-value 求值策略的函数式程序静态分析的精度。
We consider the problem of inferring a grammar describing the output of a functional program given a grammar describing its input. Solutions to this problem are helpful for detecting bugs or proving safety properties of functional programs, and several rewriting tools exist for solving this problem. However, known grammar inference techniques are not able to take evaluation strategies of the program into account. This yields very imprecise results when the evaluation strategy matters. In this work, we adapt the Tree Automata Completion algorithm to approximate accurately the set of terms reachable by rewriting under the innermost strategy. We formally prove that the proposed technique is sound and precise w.r.t. innermost rewriting. We show that those results can be extended to the leftmost and rightmost innermost case. The algorithms for the general innermost case have been implemented in the Timbuk reachability tool. Experiments show that it noticeably improves the accuracy of static analysis for functional programs using the call-by-value evaluation strategy.