DocumentCode :
3223358
Title :
Light affine lambda calculus and polytime strong normalization
Author :
Terui, Kazushige
Author_Institution :
Dept. of Philos., Keio Univ., Tokyo, Japan
fYear :
2001
fDate :
2001
Firstpage :
209
Lastpage :
220
Abstract :
Light linear logic (LLL) and its variant, intuitionistic light affine logic (ILAL), are logics of polytime computation. All polynomial-time functions are representable by proofs of these logics (via the proofs-as-programs correspondence), and, conversely, that there is a specific reduction (cut-elimination) strategy which normalizes a given proof in polynomial time (the latter may well be called the polytime “weak” normalization theorem). In this paper, we introduce an untyped term calculus, called the light affine lambda calculus (λLA), generalizing the essential ideas of light logics into an untyped framework. It is a simple modification of the λ-calculus, and has ILAL as a type assignment system. Then, in this generalized setting, we prove the polytime “strong” normalization theorem: any reduction strategy normalizes a given λLA term (of fixed depth) in a polynomial number of reduction steps, and indeed in polynomial time
Keywords :
computational complexity; lambda calculus; λLA-calculus; cut-elimination strategy; intuitionistic light affine logic; light affine lambda calculus; light linear logic; polynomial-time functions; polytime computation; polytime strong normalization; proofs-as-programs correspondence; reduction strategy; type assignment system; untyped term calculus; Calculus; Functional programming; Logic programming; Polynomials;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
Conference_Location :
Boston, MA
ISSN :
1043-6871
Print_ISBN :
0-7695-1281-X
Type :
conf
DOI :
10.1109/LICS.2001.932498
Filename :
932498
Link To Document :
بازگشت