Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. We prove that DIN enjoy an internal separation property:given two different normal nets, there exists a dual net separating them, in analogy with Bohm’s theorem for the ?-calculus. Our result implies in particular the faithfulness of every non-trivial denotational model of DIN (such as Ehrhard’s finiteness spaces). We also observe that internal separation does not hold for linear logic proof-nets: our work points out that this failure is due to the fundamental asymmetry of linear logic exponential modalities, which are instead completely symmetric in DIN.

Pagani, M., Mazza, D. (2007). The separation property for differential interaction nets. In Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference (pp.393-407). Yerevan : Nachum Dershowitz, Andrei Voronkov.

The separation property for differential interaction nets

2007-01-01

Abstract

Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. We prove that DIN enjoy an internal separation property:given two different normal nets, there exists a dual net separating them, in analogy with Bohm’s theorem for the ?-calculus. Our result implies in particular the faithfulness of every non-trivial denotational model of DIN (such as Ehrhard’s finiteness spaces). We also observe that internal separation does not hold for linear logic proof-nets: our work points out that this failure is due to the fundamental asymmetry of linear logic exponential modalities, which are instead completely symmetric in DIN.
2007
978-3-540-75558-6
Pagani, M., Mazza, D. (2007). The separation property for differential interaction nets. In Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference (pp.393-407). Yerevan : Nachum Dershowitz, Andrei Voronkov.
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/271170
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact