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.

U. Dal Lago, L. Roversi, L. Vercelli (2009). Taming Modal Impredicativity: Superlazy Reduction. BERLIN : Springer.

### Taming Modal Impredicativity: 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 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.
##### Scheda breve Scheda completa Scheda completa (DC)
2009
Lecture Notes in Computer Science
137
151
U. Dal Lago, L. Roversi, L. Vercelli (2009). Taming Modal Impredicativity: Superlazy Reduction. BERLIN : Springer.
U. Dal Lago; L. Roversi; L. Vercelli
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11585/86884`
##### Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

• ND
• 2
• 2