Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Taming Modal Impredicativity: Superlazy Reduction

Ugo Dal Lago18 Contact Information, Luca Roversi19 Contact Information and Luca Vercelli20 Contact Information

(18)  Dipartimento di Informatica, Università di Bologna,  
(19)  Dipartimento di Informatica, Università di Torino,  
(20)  Dipartimento di Matematica, Università di Torino,  
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.

Keywords  Linear logic - implicit computational complexity - proof theory


Contact Information Ugo Dal Lago

URL: http://www.cs.unibo.it/~dallago/

Contact Information Luca Roversi

URL: http://www.di.unito.it/~rover/

Contact Information Luca Vercelli

URL: http://www.di.unito.it/~vercelli/
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.112 • Server: mpweb01
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)