Characterizing polynomial and exponential complexity classes in elementary lambda-calculus

被引：2
|
作者：
Baillot, Patrick [1 ]
De Benedetti, Erika [2 ]
Della Rocca, Simona Ronchi [2 ]
机构：
[1] Univ Lyon, Univ Claude Bernard Lyon 1, CNRS, ENS Lyon,LIP UMR5668, F-69342 Lyon 07, France
[2] Univ Torino, Dipartimento Informat, Turin, Italy
来源：
INFORMATION AND COMPUTATION | 2018年 / 261卷
关键词：
Implicit computational complexity; Linear logic; Lambda-calculus; LINEAR LOGIC;
D O I：
10.1016/j.ic.2018.05.005
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper an implicit characterization of the complexity classes k-EXPand k-FEXP, for k >= 0, is given, by a type assignment system for a stratified lambda-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k-EXP is characterized by a hierarchy of types. (C) 2018 Elsevier Inc. All rights reserved.
引用
收藏
页码：55 / 77
页数：23
相关论文
共 50 条
  • [1] An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus
    Mazza, Damiano
    2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 471 - 480
  • [2] The differential lambda-calculus
    Ehrhard, T
    Regnier, L
    THEORETICAL COMPUTER SCIENCE, 2003, 309 (1-3) : 1 - 41
  • [3] On the Elementary Affine Lambda-calculus with and Without Type Fixpoints
    Nguyen, Le Thanh Dung
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (298): : 15 - 29
  • [4] A linear linear lambda-calculus
    Diaz-Caro, Alejandro
    Dowek, Gilles
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2024, : 1103 - 1137
  • [5] Intuitionistic differential nets and lambda-calculus
    Tranquilli, Paolo
    THEORETICAL COMPUTER SCIENCE, 2011, 412 (20) : 1979 - 1997
  • [6] Focused Linear Logic and the lambda-calculus
    Brock-Nannestad, Taus
    Guenot, Nicolas
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2015, 319 : 103 - 119
  • [7] Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation
    Brunel, Alois
    Mazza, Damiano
    Pagani, Michele
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [8] ON CONSTRUCTOR REWRITE SYSTEMS AND THE LAMBDA-CALCULUS
    Dal Lago, Ugo
    Martini, Simone
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (03)
  • [9] Lambda-calculus with director strings
    Fernández, M
    Mackie, I
    Sinot, FR
    APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING, 2005, 15 (06) : 393 - 437
  • [10] Spinal Atomic Lambda-Calculus
    Sherratt, David
    Heijltjes, Willem
    Gundersen, Tom
    Parigot, Michel
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2020, 2020, 12077 : 582 - 601
12345