From proof nets to interaction nets
Yves Lafont · Cambridge University Press eBooks · 1995
Introduction If we consider the interpretation of proofs as programs, say in intuitionistic logic, the question of equality between proofs becomes crucial: The syntax introduces meaningless distinctions whereas the (denotational) semantics makes excessive identifications. This question does not have a simple answer in general, but it leads to the notion of proof-net, which is one of the main novelties of linear logic. This has been already explained in [Gir87] and [GLT89]. The notion of interaction net introduced in [Laf90] comes from an attempt to implement the reduction of these proof-nets. It happens to be a simple model of parallel computation, and so it can be presented independently of linear logic, as in [Laf94]. However, we think that it is also useful to relate the exact origin of interaction nets, especially for readers with some knowledge in linear logic. We take this opportunity to give a survey of the theory of proof-nets, including a new proof of the sequentialization theorem. Multiplicatives First we consider the kernel of linear logic, with only two connectives: ⊗ ( times or tensor product ) and its dual ℘ ( par or tensor sum ). The first one can be seen as a conjunction and the second one as a disjunction. Each atom has a positive form p and a negative one p ⊥ (the linear negation of p ).