首页    期刊浏览 2024年11月25日 星期一
登录注册

文章基本信息

  • 标题:Complexity Hierarchies and Higher-Order Cons-Free Rewriting
  • 本地全文:下载
  • 作者:Cynthia Kop ; Jakob Grue Simonsen
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2016
  • 卷号:52
  • 页码:23:1-23:18
  • DOI:10.4230/LIPIcs.FSCD.2016.23
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data structures. It is well-known that cons-free programming languages can be used to characterize computational complexity classes, and that cons-free first-order term rewriting can be used to characterize the set of polynomial-time decidable sets. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the order of the types used in the systems. We prove that, for every k >= 1, left-linear cons-free systems with type order k characterize E^kTIME if arbitrary 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 possible rule overlaps with no assumptions about reduction strategy, (ii) results for such term rewriting systems have previously only been obtained for k = 1, and with additional syntactic restrictions on top of cons-freeness and left-linearity. Our results are apparently among the first implicit characterizations of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior results that having full non-determinism (via overlaps of 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 such as admitting product types or non-left-linear rules.
  • 关键词:higher-order term rewriting; implicit complexity; cons-freeness; ETIME hierarchy
国家哲学社会科学文献中心版权所有