The essential interaction between classical and intuitionistic features in the system of linear logic is best described in the language of category theory. Given a symmetric monoidal closed category C with products, the category C x C^op can be given the structure of a *-autonomous category by a special case of the Chu construction. The main result of the paper is to show that the intuitionistic translations induced by Girard trips on a proof net determine the functor from the free *-autonomous category on a set of atoms {P, P',...} to C x C^op, where C is the free monoidal closed category with products and coproducts on the set of atoms {P_O, P_I, P'_O, P'_I, ...} (a pair P_O, P_I in C for each atom P of A).
Chu's construction: a proof-theoretic approach
BELLIN, Gianluigi
2003-01-01
Abstract
The essential interaction between classical and intuitionistic features in the system of linear logic is best described in the language of category theory. Given a symmetric monoidal closed category C with products, the category C x C^op can be given the structure of a *-autonomous category by a special case of the Chu construction. The main result of the paper is to show that the intuitionistic translations induced by Girard trips on a proof net determine the functor from the free *-autonomous category on a set of atoms {P, P',...} to C x C^op, where C is the free monoidal closed category with products and coproducts on the set of atoms {P_O, P_I, P'_O, P'_I, ...} (a pair P_O, P_I in C for each atom P of A).File | Dimensione | Formato | |
---|---|---|---|
chu's_construction.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
1.23 MB
Formato
Adobe PDF
|
1.23 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.