Context Semantics, Linear Logic and Computational Complexity

TL;DR

This paper applies context semantics to analyze proof normalization in linear logic, introducing a weight measure that bounds normalization time and steps, and proving soundness for various linear logic subsystems.

Contribution

It introduces a novel weight measure based on context semantics that bounds proof normalization complexity in linear logic subsystems.

Findings

Weight measure bounds normalization time and steps.

Proves strong soundness theorems for elementary, soft, and light linear logic.

Provides a quantitative framework for analyzing proof normalization complexity.

Abstract

We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the number of steps to normal form (for certain reduction strategies). Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic and light linear logic.