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

共 14 条

[1] Herbrand's theorem as higher order recursion
Afshari, Bahareh
Hetzl, Stefan
Leigh, Graham E.
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2020, 171 (06)
[2] Beckmann A, 2000, MATH LOGIC QUART, V46, P517, DOI 10.1002/1521-3870(200010)46:4<517::AID-MALQ517>3.0.CO
[3] 2-A
[4] Exact bounds for lengths of reductions in typed λ-calculus
Beckmann, A
[J]. JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (03) : 1277 - 1285
[5] NON-IDEMPOTENT INTERSECTION TYPES AND STRONG NORMALISATION
Bernadet, Alexis
Graham-Lengrand, Stephane
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2013, 9 (04)
[6] BOUNDING LINEAR HEAD REDUCTION AND VISIBLE INTERACTION THROUGH SKELETONS
Clairambault, Pierre
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (02)
[7] Clairambault P, 2011, LECT NOTES COMPUT SC, V6604, P335, DOI 10.1007/978-3-642-19805-2_23
[8] Dal Lago U, 2008, LECT NOTES COMPUT SC, V5213, P230, DOI 10.1007/978-3-540-87531-4_18
[9] A semantic measure of the execution time in linear logic
de Carvalho, D.
Pagani, M.
de Falco, L. Tortora
[J]. THEORETICAL COMPUTER SCIENCE, 2011, 412 (20) : 1884 - 1902
[10] Model Checking Higher-Order Programs
Kobayashi, Naoki
[J]. JOURNAL OF THE ACM, 2013, 60 (03)

← 1 2 →