一句话：将解释方法扩展到纯高阶函数式语言，并用高阶多项式刻画任意阶 Basic Feasible Functions。
一阶项重写系统常借助解释方法及其多项式限制来控制终止性与复杂度，但这类方法难以直接用于纯高阶函数式语言。本文发展了一套适合该语言复杂度分析的高阶函数解释理论：将解释域设为完备格，并把程序解释表示为最小不动点，从而为高阶计算提供语义基础。作为应用，作者用高阶多项式对解释进行界限制，刻画任意阶的 Basic Feasible Functions。该工作把解释方法从一阶项重写推广到高阶函数式场景，并给出相应复杂度类的精确对应。
Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional language. We develop a theory of higher order functions that is well-suited for the complexity analysis of this programming language. The interpretation domain is a complete lattice and, consequently, we express program interpretation in terms of a least fixpoint. As an application, by bounding interpretations by higher order polynomials, we characterize Basic Feasible Functions at any order.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1801-08350,
title = {Theory of higher order interpretations and application to Basic Feasible Functions},
author = {Emmanuel Hainry and Romain Péchoux},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:14)2020}
}