Linear Logic by Levels and Bounded Time Complexity

TL;DR

This paper introduces a generalized stratification method in linear logic proof nets using levels, extending Girard's systems while preserving complexity bounds, and proposes a more efficient type assignment system for lambda calculus.

Contribution

It presents a novel level-based stratification approach in linear logic proof nets that generalizes Girard's systems and simplifies the handling of the paragraph modality.

Findings

Extended Girard's systems with levels that preserve complexity bounds

Eliminated the need for boxes in the paragraph modality handling

Proposed a more efficient lambda-calculus type assignment system

Abstract

We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indexes, which allows us to extend Girard's systems while keeping the same complexity properties. In particular, it turns out that Girard's systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones.