A bilateral-free notion of modules for Non commutative logic

manuscritA module is a piece of a proof structure. An adequate notion of type describes its behaviour, e.g. as a set of relations on the border, not making any reference to the original formulas or links of the module. Two modules connected along their border constitute a proof net precisely if their types are ``orthogonal''. For MLL the longtrip criterion of [Girard87] leads to a definition of type as (the biorthogonal of) the set of permutations on the border induced by the switchings. The correctness criterion for MNL, being based on bilateral longtrips ([AbRu00]), leads to a notion of type for MNL modules as a set of tuples of partial permutations and some relations on the border taking care of bilaterality and inclusion of the conclusions ([Abrusci99]). We will show that the bilaterality condition for MNL can be replaced by the requirement that the underlying commutative structure be a net. In other words it suffices to take into account commutative switchings as well: sequential-3-free switchings which may contain next-left-switches. This yields a definition of type as a pair of sets of decorated partial permutations on the border. The separation into pairs prevents composition of partial permutations being induced by two ``non-compatible'' switchings. The decoration is needed because for MNL it no longer holds that the longtrip meets all formulas, notably the border formulas and the conclusions. Finally, we generalize the composition of modules into an operation which yields modules again. This corresponds to a theory of types (without any reference to proof structures). Then all subsets of conclusions can be regarded as border formulas, while we compose two types only on the intersection of the not necessarily coinciding border