We present a formalization of proof-nets (and more generally, proof- structures) for the multiplicative-exponential fragment of linear logic, with a novel treatment of boxes: instead of integrating boxes into to the graphical structure (e.g., by adding explicit auxiliary doors, plus a mapping from boxed nodes to the main door, and ad hoc conditions on the nesting of boxes), we fix a graph morphism from the underlying graph of the proof-structure to the tree of boxes given by the nesting order. This approach allows to apply tools and notions from the theory of algebraic graph transformations, and obtain very synthetic presentations of sophisticated operations: for instance, each element of the Taylor expansion of a proof-structure is obtained by a pull- back along a morphism representing a thick subtree of the tree of boxes. A treatment of cut elimination in this framework currently under development.

Guerrieri, G., Manara, G., Pellissier, L., TORTORA DE FALCO, L., Vaux Auclair, L. (2021). MELL proof-nets in the category of graphs. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021).

MELL proof-nets in the category of graphs

Tortora De Falco Lorenzo;
2021

Abstract

We present a formalization of proof-nets (and more generally, proof- structures) for the multiplicative-exponential fragment of linear logic, with a novel treatment of boxes: instead of integrating boxes into to the graphical structure (e.g., by adding explicit auxiliary doors, plus a mapping from boxed nodes to the main door, and ad hoc conditions on the nesting of boxes), we fix a graph morphism from the underlying graph of the proof-structure to the tree of boxes given by the nesting order. This approach allows to apply tools and notions from the theory of algebraic graph transformations, and obtain very synthetic presentations of sophisticated operations: for instance, each element of the Taylor expansion of a proof-structure is obtained by a pull- back along a morphism representing a thick subtree of the tree of boxes. A treatment of cut elimination in this framework currently under development.
Guerrieri, G., Manara, G., Pellissier, L., TORTORA DE FALCO, L., Vaux Auclair, L. (2021). MELL proof-nets in the category of graphs. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021).
File in questo prodotto:
File Dimensione Formato  
2021-6-27-TLLA-2021.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Versione Editoriale (PDF)
Licenza: DRM non definito
Dimensione 330.84 kB
Formato Adobe PDF
330.84 kB Adobe PDF Visualizza/Apri

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: http://hdl.handle.net/11590/404879
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact