کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423395 685215 2008 21 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Soft Linear Logic and Polynomial Complexity Classes
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Soft Linear Logic and Polynomial Complexity Classes
چکیده انگلیسی

We describe some results inspired to Lafont's Soft Linear Logic (SLL) which is a subsystem of second-order linear logic with restricted rules for exponentials, correct and complete for polynomial time computations. SLL is the basis for the design of type assignment systems for lambda-calculus, characterizing the complexity classes PTIME, PSPACE and NPTIME. PTIME is characterized by a type assignments system where types are a proper subset of SLL formulae. The characterization consists in the fact that a well typed term can be reduced to normal form by a number of beta-reductions polynomial in its lenght, and moreover all polynomial time functions can be computed by well typed terms. PSPACE is characterized by a type assignment system obtained from the previous one, by extending the set of types by a type for booleans, and the lambda-calculus by two boolean constants and a conditional constructor. The system assigns types to terms in such a way that the evaluation of programs (closed terms of type boolean) can be performed carefully in polynomial space. Moreover all polynomial space decision problems can be computed by terms typable in this system. In order to characterize NPTIME we extend the lambda-calculus by a nondeterministic choice operator, and the system by a rule for dealing with this new term constructor.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 205, 6 April 2008, Pages 67-87