Between interaction and semantics: visible acyclic nets

Michele PAGANI
21/09/2007 - 08:00
Aula 13 - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma

We prove a strict correspondence between cut-elimination, 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 proof-structures 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 cut-free 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!
2. TeX Embedding failed! is visible acyclic
3. TeX Embedding failed! is a finitary relation in the finiteness space associated with TeX Embedding failed!

These equivalences provide a generalization of the ones in the main theorems of the theory of linear logic proof-nets, 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.