Abstract
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.
Research partly supported by Italy-France CNR-CNRS cooperation project 16251.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Abrusci, V.M., Ruet, P.: Non-commutative logic I: the multiplicative fragment. Annals of Pure and Applied Logic 101(1), 29–64 (2000)
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)
Andreoli, J.-M., Pareschi, R.: Linear objects: logical processes with built-in inheritance. New Generation Computing 9 (1991)
Bellin, G., Fleury, A.: Planar and braided proof-nets for multiplicative linear logic with mix. Archive for Mathematical Logic 37(5-6), 309–325 (1998)
Gaubert, C.: Two-dimensional proof-structures and the exchange rule. Mathematical Structures in Computer Science 14(1), 73–96 (2004)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)
Habert, L., Notin, J.-M., Galmiche, D.: Link: a proof environment based on proof nets. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 330–334. Springer, Heidelberg (2002)
Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 119, 447–468 (1996)
Lambek, J.: The mathematics of sentence structure. American Mathematical Monthly 65(3), 154–170 (1958)
Lecomte, A., Retoré, C.: Pomset logic as an alternative categorial grammar. In: Oehrle, M. (ed.) Formal Grammar, Barcelona (1995)
Massey, W.S.: A basic course in algebraic topology. Springer, Heidelberg (1991)
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)
Métayer, F.: Implicit exchange in multiplicative proofnets. Mathematical Structures in Computer Science 11(2), 261–272 (2001)
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals Pure Appl. Logic 51, 125–157 (1991)
Polakow, J., Pfenning, F.: Natural deduction for intuitionistic non-commutative linear logic. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 295–309. Springer, Heidelberg (1999)
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)
Ruet, P., Fages, F.: Concurrent constraint programming and non-commutative logic. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 406–423. Springer, Heidelberg (1998)
Yetter, D.N.: Quantales and (non-commutative) linear logic. Journal of Symbolic Logic 55(1) (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andreoli, JM., Pulcini, G., Ruet, P. (2005). Permutative Logic. In: Ong, L. (eds) Computer Science Logic. CSL 2005. Lecture Notes in Computer Science, vol 3634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11538363_14
Download citation
DOI: https://doi.org/10.1007/11538363_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28231-0
Online ISBN: 978-3-540-31897-2
eBook Packages: Computer ScienceComputer Science (R0)