Taming Modal Impredicativity: Superlazy Reduction

8 years 2 months ago
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
Ugo Dal Lago, Luca Roversi, Luca Vercelli
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Ugo Dal Lago, Luca Roversi, Luca Vercelli
Comments (0)