Dual Light Affine Logic (DLAL) for Polynomial Time Computation

Title: Dual Light Affine Logic (DLAL) for Polynomial Time Computation

Research Question: Can we develop a type system for lambda-calculus that ensures polynomial time computation while maintaining the benefits of linear and intuitionistic logic?

Methodology: We propose Dual Light Affine Logic (DLAL), a new type system for lambda-calculus. DLAL combines linear and intuitionistic logic with a single modality, resulting in a simpler type language with the same properties as Light Affine Logic (LAL).

Results: We show that DLAL ensures subject reduction and that a well-typed term admits a polynomial bound on the reduction by any strategy. Furthermore, we demonstrate that DLAL can represent all polynomial time functions.

Implications: DLAL offers several advantages over LAL. First, its language of types is "smaller," making it easier to work with. Second, DLAL ensures a complexity bound on the lambda-term itself, allowing for separation of the program part and the complexity specification. Lastly, we believe that type inference in DLAL could become easier, though this question remains to be explored.

Significance: Dual Light Affine Logic (DLAL) provides a new approach to type inference for lambda-calculus, offering a simpler system with the same benefits as LAL. This could lead to more efficient and reliable programming, particularly in the context of functional languages and implicit computational complexity.

Link to Article: https://arxiv.org/abs/0402059v2 Authors: arXiv ID: 0402059v2