Optimal reduction

Introduction

Linear Logic LL was introduced by Girard in 1986 [Gir87] as a refinement of classical and intuitionistic logic, in particular characterized by the introduction of new connectives (exponentials) which give a logical status to the operations of erasing and copying (corresponding to the structural rules of classical and intuitionistic sequent calculi). In other words, with Linear Logic, logical formulae really become physical resources, with a lot of almost immediate applications to Computer Science, spanning from the representation of operational aspects of programming languages and their evaluation strategies, to a dynamic definition of the notion of computational complexity, from linearity analysis and refined type synthesis for sequential languages, to the semantics of sequential and concurrent programming languages. Since its birth, Linear Logic has taken increasing importance in the field of logic in computer science ; it carried a set of completely original concepts (phase semantics, proof nets, coherent spaces,
geometry of interaction), rediscovered and put to use previous tools (*-autonomous categories, game semantics), and deeply renewed the field. So, Linear Logic is not only an elegant and powerful technical theory but, first of all, a source of methodological guidelines. We learned from the definition of LL that some logical connectives, which were considered atomic, are composite. In fact the essential property of LL is the decomposition of the intuitionistic implication in
. A linear implication represents a transformation process, that, taken as input one object belonging to ,
gives as output one object belonging to B. The modality ! denotes a different process, which gives explicit evidence to intensional
properties of the object to be transformed. These properties describe the potentiality of the object to be either duplicated or deleted during the transformation. So LL supports primitive operators for duplication and erasure,...