Speaker:  Michele PAGANI


Quando:  21/09/2007  08:00


Dove:  Aula 13  Facoltà Lettere e Filosofia  Università Roma Tre  Via Ostiense 234 Roma


Abstract
We prove a strict correspondence between cutelimination, acyclicity and denotational semantics in the framework of differential interaction nets with promotion (DIN for short). DIN is an extension of the multiplicative exponential linear logic (MELL) introducing differential operators for the exponentials. We define the orthogonal TeX Embedding failed! of a net TeX Embedding failed! with conclusion TeX Embedding failed! as the set of all nets TeX Embedding failed! with a conclusion TeX Embedding failed! s.t. the cut between TeX Embedding failed! and TeX Embedding failed! is weak normalizable. Then, we introduce in DIN visible acyclicity, a geometric condition which in usual MELL characterizes those proofstructures which correspond to cliques in coherence spaces. Moreover, we consider finiteness spaces, a generalization of coherence spaces which are at the base of the differential extension of MELL. Let TeX Embedding failed! be a cutfree net with conclusion TeX Embedding failed!, our results prove that the following conditions are equivalent: 1. TeX Embedding failed! contains all visible acyclic nets with a conclusion TeX Embedding failed! These equivalences provide a generalization of the ones in the main theorems of the theory of linear logic proofnets, namely: Bechét's theorem (TeX Embedding failed!), weak normalization theorem (TeX Embedding failed!), semantic soundness theorem (TeX Embedding failed!) and Retoré's theorem (TeX Embedding failed!). Above all, it discloses a deep unity in DIN between normalization, visible acyclicity and finiteness spaces, which was present (even if never actually remarked) only in the multiplicative fragment of linear logic. 