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
关键词
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] CLASSES OF NUMERATION MODELS OF LAMBDA-CALCULUS
    KANDA, A
    ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1986, 32 (04): : 315 - 322
  • [2] Light types for polynomial time computation in Lambda-calculus
    Baillot, P
    Terui, K
    19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 266 - 275
  • [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] Soft lambda-calculus: A language for polynomial time computation
    Baillot, P
    Mogbil, V
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2004, 2987 : 27 - 41
  • [5] 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
  • [6] Atomic lambda-calculus: a typed lambda-calculus with explicit sharing
    Gundersen, Tom
    Heijltjes, Willem
    Parigot, Michel
    2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2013, : 311 - 320
  • [7] ALGEBRA AND THE LAMBDA-CALCULUS
    JAFFER, A
    DR DOBBS JOURNAL, 1993, 18 (09): : 36 - &
  • [8] SET-THEORETICAL AND OTHER ELEMENTARY MODELS OF THE LAMBDA-CALCULUS
    PLOTKIN, GD
    THEORETICAL COMPUTER SCIENCE, 1993, 121 (1-2) : 351 - 409
  • [9] The differential lambda-calculus
    Ehrhard, T
    Regnier, L
    THEORETICAL COMPUTER SCIENCE, 2003, 309 (1-3) : 1 - 41
  • [10] Lambda-calculus with constructors
    Arbiser, Ariel
    Miquel, Alexandre
    Rios, Alejandro
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 181 - 196