Light types for polynomial time computation in Lambda-calculus

被引:38
作者
Baillot, P [1 ]
Terui, K [1 ]
机构
[1] Univ Paris 13, CNRS, Lab Informat Paris Nord, F-93430 Villetaneuse, France
来源
19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 2004年
关键词
D O I
10.1109/LICS.2004.1319621
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We propose a new type system for lambda-calculus ensuring that well-typed programs can be executed in polynomial time: Dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality.t corresponds to a fragment of Light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms: subject reduction is satisfied and a well-typed term admits a polynomial bound on the reduction by any strategy. Finally we establish that as LAL, DLAL allows to represent all poly time functions.
引用
收藏
页码:266 / 275
页数:10
相关论文
共 27 条
[1]  
ASPERTI A, 2002, ACM T COMPUT LOG, V3, P1
[2]  
Asperti A., 1998, P LICS 98
[3]  
BAILLOT P, 2003, 0203 LIPN U PARIS 13
[4]  
BAILLOT P, 2002, P IFIP TCS 02 MONTR
[5]  
BAILLOT P, 2004, CSLO0402059
[6]  
BAILLOT P, 2004, IN PRESS THEORETICAL
[7]  
BARBER A, 1997, DUAL INTUITIONISTIC
[8]   Higher type recursion, ramification and polynomial time [J].
Bellantoni, SJ ;
Niggl, KH ;
Schwichtenberg, H .
ANNALS OF PURE AND APPLIED LOGIC, 2000, 104 (1-3) :17-30
[9]  
Bellantoni Stephen, 1992, COMPUT COMPLEX, V2, P97, DOI [10.1007/bf01201998., DOI 10.1007/BF01201998, 10.1007/BF01201998]
[10]  
BENTON N, 1993, LNCS, V664