Taming Modal Impredicativity: Superlazy Reduction

Pure, or type-free, Linear Logic proof nets are Turing complete once cut-elimination is5 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 con-10 trol modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of the reduction 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.15 Contents

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Ugo Dal Lago, Luca Roversi, Luca Vercelli
• Keywords: CORR 2008, Education, Modal Impredicativity, Proof Net, Superlazy Reduction