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