Ricostruire una rete di prova dal suo sviluppo di Taylor (lavoro in comune con Christine Tasson).

La logica lineare (LL) è basata sull'analogia tra la linearità in algebra (i.e. commutazione con somme e prodotti con scalari) e la linearità in informatica (i.e. utilizzo dei dati di entrata esattamente una volta). Portando avanti tale analogia, Ehrhard e Regnier hanno introdotto la logica lineare differenziale (DiLL) -- un'estensione di LL con operatori differenziali. In questo contesto la promozione (l'analogo in logica dell'esponenziale) può essere approssimata da una somma di reti differenziali per mezzo di una nozione di sviluppo di Taylor.

Presenteremo un algoritmo per definire l'inverso dello sviluppo di Taylor. Più precisamente, definiremo un sistema di riscrittura (merging reduction) in grado di ricostruire da una somma finita S di reti differenziali, una rete di prova R con promozione se e solo se S è contenuta nell'espansione di Taylor di R. L'algoritmo è non-deterministico, valido e completo. Termineremo mostrando la stretta relazione tra una proprietà di confluenza della merging reduction e il problema dell'iniettività della semantica relazionale per la logica lineare.

http://www.pps.jussieu.fr/%7Emichele/taylorLL.pdf