zbMATH — the first resource for mathematics

Modules in non-commutative logic. (English) Zbl 0931.03068
Girard, Jean-Yves (ed.), Typed lambda calculi and applications. 4th international conference, TLCA ’99. L’Aquila, Italy, April 7–9, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1581, 14-24 (1999).
The question we want to investigate was expressed by J.-Y. Girard [Rend. Semin. Mat., Torino Fasc. Spec. 1987, 11-33 (1987; Zbl 0667.03046)] as follows:
“Assume that I am given a program \(P\) [a proof-net \(\Pi]\), and that I cut it in two parts arbitrarily. I create two \(\dots\) modules, linked together by their border. Can I express that my two modules are complementary [orthogonal], in other terms that I can branch them by identification over their common border? One would like to define the type of the modules as their branching instructions; these branching instructions should be such that they authorized the restoring of the original \(P\) [the proof-net \(\Pi]\).”
Girard [loc. cit.] gave the solution for the multiplicative fragment of linear logic (MLL); another deep investigation of this question for MLL has been given by V. Danos and L. Regnier [Arch. Math. Log. 28, No. 3, 181-203 (1989; Zbl 0689.03013)]. Here we present the first steps towards a solution of this question for the multiplicative fragment of non-commutative logic (MNL), which is a refinement of MLL and an extension of both MLL and the cyclic multiplicative linear logic. MNL was introduced by the author and P. Ruet [Non-commutative logic. I: The multiplicative fragment (Preprint, Univ. Roma Tre and McGill Univ.) (1998)].
The lines of Girard’s investigations [loc. cit.] are the basis for our investigations, since they can be improved and adapted also for MNL.
For the entire collection see [Zbl 0911.00022].
03F07 Structure of proofs
03F52 Proof-theoretic aspects of linear logic and other substructural logics
03B70 Logic in computer science
PDF BibTeX Cite