Skip to main content
SpringerLink
Log in

Modularity of proof-nets

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

Abstract.

When we cut a multiplicative proof-net of linear logic in two parts we get two modules with a certain border. We call pretype of a module the set of partitions over its border induced by Danos-Regnier switchings. The type of a module is then defined as the double orthogonal of its pretype. This is an optimal notion describing the behaviour of a module: two modules behave in the same way precisely if they have the same type.

In this paper we define a procedure which allows to characterize (and calculate) the type of a module only exploiting its intrinsic geometrical properties and without any explicit mention to the notion of orthogonality. This procedure is simply based on elementary graph rewriting steps, corresponding to the associativity, commutativity and weak-distributivity of the multiplicative connectives of linear logic.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abramsky, S., Jagadeesan, R.: Games and Full Completeness for Multiplicative Linear Logic. J. Symbolic Logic 59 (2), 543–574 (1994)

    Google Scholar 

  2. Abrusci, V.M., Ruet, P.: Non commutative logic I: the multiplicative fragment. Annals of Pure and Applied Logic 101, 29–64 (2000)

    Google Scholar 

  3. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2, 1992

  4. Andreoli, J.-M.: Focussing and proof construction. Annals of Pure and Applied Logic 107, 131–163 (2001)

    Google Scholar 

  5. Cockett, J.R.B., Seely, R.A.G.: Weakly Distributive Categories. Journal of Pure and Applied Algebra, 114, 133–173 (1997)

    Google Scholar 

  6. Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28, 181–203 (1989)

    MathSciNet  MATH  Google Scholar 

  7. Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)

    Article  MATH  Google Scholar 

  8. Girard, J.-Y.: Multiplicatives. Rendiconti del Seminario Matematico dell’Università e Policlinico di Torino, special issue on Logic and Computer Science, pp. 11–33, 1987

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Rome “La Sapienza”,  

    Roberto Maieli

  2. Department of Philosophy, University “Roma Tre”,  

    Quintijn Puite

Authors
  1. Roberto Maieli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Quintijn Puite
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roberto Maieli.

Additional information

This work was carried out at the University “Roma Tre”, in the framework of the European TMR Research Programme “Linear Logic in Computer Science”. The authors are grateful to Paul Ruet and to the anonymous referee for their useful comments and remarks on a previous version of this paper.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Maieli, R., Puite, Q. Modularity of proof-nets. Arch. Math. Logic 44, 167–193 (2005). https://doi.org/10.1007/s00153-004-0242-2

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-004-0242-2

Keywords

Search

Navigation