proof-net
proof-net
proof-net o rete dimostrativa o rete di prova, in logica lineare è un grafo che rappresenta una dimostrazione, termine con cui si intende una deduzione formale nel calcolo dei → sequenti della logica lineare. Come ogni grafo, un proof-net presenta un insieme di nodi connessi fra loro da un insieme di archi. Gli archi di un proof-net sono etichettati da formule della logica lineare; i nodi sono detti legami e rappresentano le regole del calcolo dei sequenti lineare. Ogni legame ha un certo numero di archi entranti, detti premesse del legame, e degli archi uscenti detti conclusioni. Esempi di legami sono:
• legame assioma: corrisponde alla regola dell’assioma (o regola dell’identità) nel calcolo dei sequenti lineare. Il legame assioma è indicato con (ax), non ha premesse e ha due conclusioni, etichettate rispettivamente da una formula A e dalla sua negazione A⊥;
• legame tensore: corrisponde alla regola di introduzione della congiunzione moltiplicativa (detta times e indicata con il simbolo ⊗; → logica lineare). Il legame tensore ha due premesse etichettate dalle formule A e B e una conclusione etichettata dalla formula A ⊗ B;
• legame par: corrisponde alla regola di introduzione della disgiunzione moltiplicativa (detta par e indicata anche con il simbolo ℘; → logica lineare). Il legame par ha due premesse etichettate dalle formule A e B e una conclusione etichettata dalla formula A ℘ B;
• legame cut: corrisponde alla regola del → taglio del calcolo dei sequenti. Il legame cut ha due premesse etichettate rispettivamente da una formula A e dalla sua negazione A⊥ e nessuna conclusione.
Per definire formalmente un proof-net si parte da una particolare classe di grafi detti strutture di prova. Una struttura di prova è un grafo orientato G i cui nodi (legami) e i cui archi (premesse e conclusioni) soddisfano le seguenti condizioni: a) ogni arco di G è conclusione di un unico legame; b) ogni arco di G è premessa di al più un legame. Un arco di G che non è premessa di alcun legame è detto conclusione del grafo G. Fra tutte le strutture di prova, solo alcune rappresentano dimostrazioni della logica lineare e quindi possono essere considerate dei proof-net. Un proof-net è una struttura di prova G tale che il grafo non orientato che si ottiene da G eliminando una delle due premesse in ogni legame par (detto grafo di correttezza) è aciclico e connesso. A ogni dimostrazione π di una formula A della logica lineare è possibile associare un proof-net Gπ con un arco conclusione etichettato dalla formula A. Viceversa per ogni proof-net R esiste una dimostrazione tale che il proof-net associato a essa (Gπ) coincide con R. Dato un proof-net G, possono esistere più dimostrazioni che abbiano come grafo associato il proof-net G.
In logica lineare vale il teorema di eliminazione del taglio secondo cui ogni dimostrazione di una formula A può essere trasformata in un’altra dimostrazione di A in cui non si fa uso della regola di taglio. La trasformazione di una dimostrazione d in un’altra d′ corrisponde alla trasformazione del proof-net Gd, associato a d, nel proof-net Gd′. Ciò consente di rappresentare un processo di calcolo (l’eliminazione del taglio da una dimostrazione) attraverso la deformazione di un grafo (il proof-net).