Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'lau85vqm3ul323pka62f4neai4' 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 = 'lau85vqm3ul323pka62f4neai4' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node/418', '', '216.73.216.58', 1751586016) in /var/www/church/includes/database.mysql.inc on line 121