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].

“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].