Polynomial time in untyped elementary linear logic

被引：1

作者：

Laurent, Olivier ^{[1
]}

机构：

[1] Univ Lyon, UCBL, CNRS, Ensl,LIP, F-69342 Lyon 07, France

来源：

THEORETICAL COMPUTER SCIENCE | 2020年 / 813卷

关键词：

Implicit computational complexity; Polynomial time computation; Elementary linear logic; Proof nets; Strong normalization; SEMANTICS;

D O I：

10.1016/j.tcs.2019.10.002

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We show how to represent polynomial time computation in an untyped version of proof-nets for elementary linear logic. This follows previous work by P. Baillot but which was developed in a typed and affine setting. We describe how these two properties can be adapted. (C) 2019 Elsevier B.V. All rights reserved.

引用

页码：117 / 142

页数：26

共 21 条

[1] [Anonymous], 2003, CAMBRIDGE TRACTS THE, V55
[2] [Anonymous], 1989, Cambridge Tracts in Theoretical Computer Science
[3] Asperti A., 2002, ACM Transactions on Computational Logic, V3, P137, DOI 10.1145/504077.504081
[4] Light affine logic
Asperti, A
[J]. THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 300 - 308
[5] Stratified coherence spaces: a denotational semantics for light linear logic
Baillot, P
[J]. THEORETICAL COMPUTER SCIENCE, 2004, 318 (1-2) : 29 - 55
[6] On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy
Baillot, Patrick
[J]. INFORMATION AND COMPUTATION, 2015, 241 : 3 - 31
[7] On light logics, uniform encodings and polynomial time
Dal Lago, Ugo
Baillot, Patrick
[J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (04) : 713 - 733
[8] Context Semantics, Linear Logic, and Computational Complexity
Dal Lago, Ugo
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 10 (04)
[9] Linear logic and elementary time
Danos, V
Joinet, JB
[J]. INFORMATION AND COMPUTATION, 2003, 183 (01) : 123 - 137
[10] DANOS V, 1990, THESIS

← 1 2 3 →