Jump from parallel to sequential proofs: exponentials

摘要

In previous works, by importing ideas from game semantics (notably Faggian–Maurel–Curien’s ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called 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 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 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 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.