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 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.
Taming Modal Impredicativity: Superlazy Reduction / U. Dal Lago; L. Roversi; L. Vercelli. - STAMPA. - 5407:(2009), pp. 137-151. (Intervento presentato al convegno International Symposium on Logical foundations of Computer Science tenutosi a Deerfield Beach, FL, USA nel January 3-6, 2009).
Taming Modal Impredicativity: Superlazy Reduction
DAL LAGO, UGO;
2009
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 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.