Light types for polynomial time computation in lambda-calculus

We present a polymorphic type system for lambda calculus ensuring that welltyped 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. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL. Key words: linear logic, light linear logic, lambda calculus, type system, implicit computational complexity, polynomial time complexity.

• Type: Journal
• Year: 2004
• Where: CORR
• Authors: Patrick Baillot, Kazushige Terui
• Keywords: CORR 2004, Education, Light Affine Logic, Polynomial Time, Type System