Termination Analysis of Higher-Order Functional Programs

Termination Analysis of Higher-Order Functional Programs
复制标题

高阶函数程序的终止分析

DOI：
--
复制
发表时间：
2005
期刊：
Asian Symposium on Programming Languages and Systems
影响因子：
--
通讯作者：
N. Jones
N. Jones
中科院分区：
--
文献类型：
--
作者：
D. Sereni;N. Jones

文献摘要

被引文献

相似文献

尺寸变化终止（SCT）自动识别一阶函数程序的终止。SCT原则：如果每一个无限控制流序列将导致一个有根据的数据值的无限下降，则程序终止（POPL 2001）。 最近的工作（RTA 2004）使用类似的方法开发了纯无类型λ演算的终止分析，但需要完全不同的大小概念来比较高阶值。这也是一个强有力的分析，甚至证明了包含不动点组合子Y的某些λ-表达式的终止性。然而，分析的语言很小，甚至不包含常数。 这些技术是统一的，并大大扩展，以产生一个终止分析器，用于高阶，按值调用程序，如ML的纯函数核心或类似的函数语言。我们的分析器已被证明是正确的，并实现了OCaml的一个重要子集。
Size-change termination (SCT) automatically identifies termination of first-order functional programs. The SCT principle: a program terminates if every infinite control flow sequence would cause an infinite descent in a well-founded data value (POPL 2001). More recent work (RTA 2004) developed a termination analysis of the pure untyped λ-calculus using a similar approach, but an entirely different notion of size was needed to compare higher-order values. Again this is a powerful analysis, even proving termination of certain λ-expressions containing the fixpoint combinator Y. However the language analysed is tiny, not even containing constants. These techniques are unified and extended significantly, to yield a termination analyser for higher-order, call-by-value programs as in ML’s purely functional core or similar functional languages. Our analyser has been proven correct, and implemented for a substantial subset of OCaml.