Recent work establishes a direct link between the complexity of a linear logic proof in terms of the exchange rule and the topological complexity of its corresponding proof net, expressed as the minimal rank of the surfaces on which the proof net can be drawn without crossing edges. That surface is essentially computed by sequentialising the proof net into a sequent calculus which is derived from that of linear logic by attaching an appropriate structure to the sequents. We show here that this topological calculus can be given a better-behaved logical status, when viewed in the variety-presentation framework introduced by the first author. This change of viewpoint gives rise to permutative logic, which enjoys cut elimination and focussing properties and comes equipped with new modalities for the management of the exchange rule. Moreover, both cyclic and linear logic are shown to be embedded into permutative logic. It provides the natural logical framework in which to study and constrain the topological complexity of proofs, and hence the use of the exchange rule.
KeywordsLinear Logic Structural Rule Sequent Calculus Minimal Rank Categorial Grammar
Unable to display preview. Download preview PDF.
- 1.Abrusci, V.M.: Non-commutative logic and categorial grammar: ideas and questions. In: Abrusci, V.M., Casadio, C. (eds.) Dynamic Perspectives in Logic and Linguistics, Cooperativa Libraria Universitaria Editrice Bologna (1999)Google Scholar
- 3.Andreoli, J.-M.: An axiomatic approach to structural rules for locative linear logic. In: Linear logic in computer science. London Mathematical Society Lecture Notes Series, vol. 316, Cambridge University Press, Cambridge (2004)Google Scholar
- 4.Andreoli, J.-M., Pareschi, R.: Linear objects: logical processes with built-in inheritance. New Generation Computing 9 (1991)Google Scholar
- 11.Lecomte, A., Retoré, C.: Pomset logic as an alternative categorial grammar. In: Oehrle, M. (ed.) Formal Grammar, Barcelona (1995)Google Scholar
- 13.Melliès, P.-A.: A topological correctness criterion for multiplicative noncommutative logic. In: Linear logic in computer science. London Mathematical Society Lecture Notes Series, vol. 316, Cambridge University Press, Cambridge (2004)Google Scholar
- 17.Retoré, C.: Pomset logic - A non-commutative extension of commutative linear logic. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, Springer, Heidelberg (1997)Google Scholar
- 19.Yetter, D.N.: Quantales and (non-commutative) linear logic. Journal of Symbolic Logic 55(1) (1990)Google Scholar