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 [J].

Afshari, Bahareh ;

Hetzl, Stefan ;

Leigh, Graham E. .

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 [J].

Beckmann, A .

JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (03) :1277-1285

[5] NON-IDEMPOTENT INTERSECTION TYPES AND STRONG NORMALISATION [J].

Bernadet, Alexis ;

Graham-Lengrand, Stephane .

LOGICAL METHODS IN COMPUTER SCIENCE, 2013, 9 (04)

[6] BOUNDING LINEAR HEAD REDUCTION AND VISIBLE INTERACTION THROUGH SKELETONS [J].

Clairambault, Pierre .

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 [J].

de Carvalho, D. ;

Pagani, M. ;

de Falco, L. Tortora .

THEORETICAL COMPUTER SCIENCE, 2011, 412 (20) :1884-1902

[10] Model Checking Higher-Order Programs [J].

Kobayashi, Naoki .

JOURNAL OF THE ACM, 2013, 60 (03)

← 1 2 →