Soft Linear Logic: A Language for Polynomial Time Computation

Title: Soft Linear Logic: A Language for Polynomial Time Computation

Abstract: Soft linear logic (SLL) is a subsystem of linear logic that can characterize the PTIME complexity class. This study introduces soft lambda-calculus, a typable calculus in the intuitionistic and affine variant of SLL. The main result is that the untyped terms of this calculus can be reduced in polynomial time. The type system of SLL is extended with recursive types, allowing for non-standard types representing lists. The example of insertion sort algorithm is used to examine the expressivity of SLL.

Main Research Question: Can Soft Linear Logic be used as a programming language for polynomial time computation?

Methodology: The study uses the soft lambda-calculus, a typable calculus in the intuitionistic and affine variant of SLL. The main methodology involves proving that the untyped terms of this calculus can be reduced in polynomial time. This is achieved by extending the type system of SLL with recursive types and using these datatypes to represent lists.

Results: The main result of the study is that the untyped terms of the soft lambda-calculus can be reduced in polynomial time. The expressivity of SLL is examined using the example of the insertion sort algorithm.

Implications: The results of this study suggest that Soft Linear Logic can be used as a programming language for polynomial time computation. This opens up new possibilities for studying program properties using Implicit Computational Complexity. The ability to represent standard algorithms like insertion sort in SLL indicates that it has sufficient programming capabilities.

Link to Article: https://arxiv.org/abs/0312015v1 Authors: arXiv ID: 0312015v1