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 Böhm’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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Böhm, C.: Alcune proprietà delle forme βη-normali nel λ-K-calcolo. Pubblicazioni dell’IAC 696, 1–19 (1968)
Friedman, H.: Equality between functionals. In: Proceedings of LC 72-73. Lecture Notes in Math., vol. 453, pp. 22–37 (1975)
Statman, R.: Completeness, invariance and λ-definability. J. Symbolic Logic, 17–26 (1983)
Joly, T.: Codages, séparabilité et représentation de fonctions en λ-calcul simplement typé et dans d’autres systèmes de types. Ph.D. Thesis, Université de Paris 7 (2000)
Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50, 1–102 (1987)
Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theoret. Comput. Sci. 135, 111–137 (1994)
Girard, J.Y.: Locus solum. Math. Struct. Comput. Sci. 11, 301–506 (2001)
de Falco, L.T.: Obsessional experiments for linear logic proof-nets. Math. Struct. Comput. Sci. 13, 799–855 (2003)
Ehrhard, T., Regnier, L.: Differential interaction nets. Theoret. Comput. Sci. 364, 166–195 (2006)
Lafont, Y.: Interaction nets. In: POPL 1990, pp. 95–108 (1990)
Ehrhard, T.: Finiteness spaces. Math. Struct. Comput. Sci. 15, 615–646 (2005)
Mazza, D.: Interaction Nets: Semantics and Concurrent Extensions. Ph.D. Thesis, Universitée de la Méditerranée/Universitá degli Studi Roma Tre (2006)
Regnier, L.: Lambda-calcul et réseaux. Ph.D. Thesis, Université de Paris 7 (1992)
De Carvalho, D.: Sémantique de la logique linéaire et temps de calcul. Ph.D. Thesis, Université d’Aix-Marseille 2 (2007)
Danos, V., Regnier, L.: Proof nets and the Hilbert space. In: Advances in Linear Logic, pp. 307–328. Cambridge University Press, Cambridge (1995)
David, R., Py, W.: λμ-calculus and Böhm’s theorem. J. Symbolic Logic 66, 407–413 (2001)
Vaux, L.: The differential λμ-calculus. Theoret. Comput. Sci. 379, 166–209 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mazza, D., Pagani, M. (2007). The Separation Theorem for Differential Interaction Nets. In: Dershowitz, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2007. Lecture Notes in Computer Science(), vol 4790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75560-9_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-75560-9_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75558-6
Online ISBN: 978-3-540-75560-9
eBook Packages: Computer ScienceComputer Science (R0)