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.

Maieli, R., Quintijn, P. (2005). Modularity of proof nets: generating the type of a module. ARCHIVE FOR MATHEMATICAL LOGIC, 44(2), 167-193 [10.1007/s00153-004-0242-2].

### Modularity of proof nets: generating the type of a module

#### 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.
##### Scheda breve Scheda completa Scheda completa (DC)
2005
Maieli, R., Quintijn, P. (2005). Modularity of proof nets: generating the type of a module. ARCHIVE FOR MATHEMATICAL LOGIC, 44(2), 167-193 [10.1007/s00153-004-0242-2].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11590/149357`
• ND
• 4
• 3