Exact bounds for acyclic higher-order recursion schemes

被引：0
|
作者：
Afshari, Bahareh [1 ,2 ]
Wehr, Dominik [2 ]
机构：
[1] Univ Amsterdam, Inst Logic Language & Computat, Amsterdam, Netherlands
[2] Univ Gothenburg, Dept Philosophy Linguist & Theory Sci, Gothenburg, Sweden
来源：
INFORMATION AND COMPUTATION | 2023年 / 290卷
基金：
瑞典研究理事会;
关键词：
Higher-order recursion schemes; Simply typed A; -calculus; Language bounds;
D O I：
10.1016/j.ic.2022.104982
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Beckmann [1] derives bounds on the length of reduction chains of classes of simply typed A.-calculus terms which are exact up-to a constant factor in their highest exponent. Afshari et al. [2] obtain similar bounds on acyclic higher-order recursion schemes (HORS) by embedding them in the simply typed A.-calculus and applying Beckmann's result. In this article, we apply Beckmann's proof strategy directly to acyclic HORS, proving exactness of the bounds on reduction chain length and obtaining exact bounds on the size of languages generated by acyclic HORS. (c) 2022 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
引用
收藏
页数：15
相关论文
共 50 条
  • [1] Semantics of Higher-Order Recursion Schemes
    Adamek, Jiri
    Milius, Stefan
    Velebil, Jiri
    ALGEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2009, 5728 : 49 - +
  • [2] Linearity in Higher-Order Recursion Schemes
    Clairambault, Pierre
    Grellois, Charles
    Murawski, Andrzej S.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [3] SEMANTICS OF HIGHER-ORDER RECURSION SCHEMES
    Adamek, Jiri
    Milius, Stefan
    Velebil, Jiri
    LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (01)
  • [4] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs
    Kobayashi, Naoki
    ACM SIGPLAN NOTICES, 2009, 44 (01) : 416 - 428
  • [5] On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
    Kobayashi, Naoki
    Lozes, Etienne
    Bruse, Florian
    ACM SIGPLAN NOTICES, 2017, 52 (01) : 246 - 259
  • [6] Types and Recursion Schemes for Higher-Order Program Verification
    Kobayashi, Naoki
    PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2009, 5904 : 2 - 3
  • [7] The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
    Clemente, Lorenzo
    Parys, Pawel
    Salvati, Sylvain
    Walukiewicz, Igor
    PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), 2016, : 96 - 105
  • [8] IO vs OI in Higher-Order Recursion Schemes
    Haddad, Axel
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (77): : 23 - 30
  • [9] Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
    Broadbent, Christopher H.
    Carayol, Arnaud
    Ong, C-H Luke
    Serre, Olivier
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2021, 22 (02)
  • [10] On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
    Broadbent, Christopher
    Ong, Luke
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2009, 5504 : 107 - 121
12345