Taming Modal Impredicativity: Superlazy Reduction

TL;DR

This paper introduces superlazy reduction, a novel reduction strategy for pure proof nets in linear logic that controls modal impredicativity, ensuring finite, predictable, and primitive recursive time complexity for cut-elimination.

Contribution

It defines superlazy reduction to manage modal impredicativity, making cut-elimination cost predictable and enabling the computation of any primitive recursive function within pure proof nets.

Findings

Superlazy reduction ensures finite, primitive recursive time for proof net reduction.

It controls modal impredicativity during cut-elimination.

Any primitive recursive function can be represented and computed using pure proof nets with superlazy reduction.

Abstract

Pure, or type-free, Linear Logic proof nets are Turing complete once cut-elimination is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing the complexity of cut-elimination to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, the conclusion of a residual of a box b interacts with a node that belongs to the proof net inside another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a proof net finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a pure proof net via superlazy reduction.