Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'vidc82cb9apk5s49qpd79d8ce0' in /var/www/church/includes/database.mysql.inc on line 121
Jump from parallel to sequential proofs: Exponentials | Gruppo di Logica e Geometria della Cognizione

Jump from parallel to sequential proofs: Exponentials

2011

Paolo Di Giamberardino

Mathematical Structures in Computer Science, special issue on `DIFFERENTIAL LINEAR LOGIC, NETS, AND OTHER QUANTITATIVE AND PARALLEL APPROACHES TO PROOF-THEORY''

Abstract

In previous works, by importing ideas from game semantics (notably
Faggian-Maurel-Curien's \emph{ludics nets}), we defined a new class of
multiplicative/additive polarized proof nets, called \emph{J-proof nets}. The
distinctive feature of J-proof nets with respect to other proof net
syntaxes, is the possibility of representing proof nets which are
partially sequentialized, by using \emph{jumps} (that is, untyped extra edges) as
sequentiality constraints. Starting from this result, in the present work we
extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: more precisely, we
replace the familiar linear logic notion of exponential box with a less restricting one (called \emph{cone})
defined by means of jumps. As a consequence, we get a syntax for
polarized nets where, instead of a structure of boxes nested one into the other,
we have one of cones which can be \emph{partially overlapping}. Moreover, we define cut-elimination for exponential J-proof nets, proving, by a variant of Gandy's method, that even in case of ``superposed'' cones, reduction enjoys confluence and strong
normalization.

BibTeX


Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = 'vidc82cb9apk5s49qpd79d8ce0' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/418', 'http://logica.uniroma3.it/pubblicazioni/tutti', '193.204.165.103', 1754566510) in /var/www/church/includes/database.mysql.inc on line 121

Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: INSERT INTO sessions (sid, uid, cache, hostname, session, timestamp) VALUES ('vidc82cb9apk5s49qpd79d8ce0', 0, 0, '193.204.165.103', '', 1754566510) in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/418', 'http://logica.uniroma3.it/pubblicazioni/tutti', '193.204.165.103', 1754566510) in /var/www/church/includes/database.mysql.inc on line 121