一句话：论文证明左线性 cons-free 高阶项重写系统按类型阶 K 刻画 E^K TIME，并分析非确定性与语法限制的影响。
本文研究 cons-free 高阶项重写系统的隐式计算复杂度：cons-free 要求规则右端构造子项是左端子项，不能构造新数据结构；此前结果多限于一阶或类型阶 K=1。作者定义按类型阶 K 分层的左线性 cons-free 高阶项重写系统，在不限定归约策略（允许非正交与重叠规则）下分析其可计算函数类。主要结论是，对每个 K≥1，这类系统恰好刻画 E^K TIME；相比先前工作，每升一阶得到更大的类（E^K TIME 而非 EXP^{K-1}TIME），并首次给出 E 层级 E^1TIME ⊊ E^2TIME ⊊ … 的隐式刻画之一。论文还表明完全非确定性不能直接刻画 NE，且非确定性使所刻画类对乘积类型或非左线性规则等微小语法改动高度敏感。
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of the left-hand sides; the computational intuition is that rules cannot build new data structures. In programming language research, cons-free languages have been used to characterize hierarchies of computational complexity classes; in term rewriting, cons-free first-order TRSs have been used to characterize the class PTIME. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the type order of the systems. We prove that, for every K $\geq$ 1, left-linear cons-free systems with type order K characterize E$^K$TIME if unrestricted evaluation is used (i.e., the system does not have a fixed reduction strategy). The main difference with prior work in implicit complexity is that (i) our results hold for non-orthogonal term rewriting systems with no assumptions on reduction strategy, (ii) we consequently obtain much larger classes for each type order (E$^K$TIME versus EXP$^{K-1}$TIME), and (iii) results for cons-free term rewriting systems have previously only been obtained for K = 1, and with additional syntactic restrictions besides cons-freeness and left-linearity. Our results are among the first implicit characterizations of the hierarchy E = E$^1$TIME $\subsetneq$ E$^2$TIME $\subsetneq$ ... Our work confirms prior results that having full non-determinism (via overlapping rules) does not directly allow for characterization of non-deterministic complexity classes like NE. We also show that non-determinism makes the classes characterized highly sensitive to minor syntactic changes like admitting product types or non-left-linear rules.Comment: extended version of a paper submitted to FSCD 2016. arXiv admin note: substantial text overlap with arXiv:1604.08936
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KopS17,
title = {Complexity Hierarchies and Higher-order Cons-free Term Rewriting},
author = {Cynthia Kop and Jakob Grue Simonsen},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:8)2017}
}