# Proof Nets and the Linear Substitution Calculus

• Beniamino Accattoli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

## Abstract

Since the very beginning of the theory of linear logic it is known how to represent the $$\lambda$$-calculus as linear logic proof nets. The two systems however have different granularities, in particular proof nets have an explicit notion of sharing—the exponentials—and a micro-step operational semantics, while the $$\lambda$$-calculus has no sharing and a small-step operational semantics. Here we show that the linear substitution calculus, a simple refinement of the $$\lambda$$-calculus with sharing, is isomorphic to proof nets at the operational level.

Nonetheless, two different terms with sharing can still have the same proof nets representation—a further result is the characterisation of the equality induced by proof nets over terms with sharing. Finally, such a detailed analysis of the relationship between terms and proof nets, suggests a new, abstract notion of proof net, based on rewriting considerations and not necessarily of a graphical nature.

## Notes

### Acknowledgments

To the reviewers, for useful comments. This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01).

## References

1. 1.
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991).
2. 2.
Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari, A. (ed.) Proceedings of 28th International Conference on Rewriting Techniques and Applications, RTA 2012, May–June 2012, Nagoya, Leibniz International Proceedings in Informatics, vol. 15, pp. 6–21. Dagstuhl Publishing, Saarbrücken, Wadern (2012).
3. 3.
Accattoli, B.: Evaluating functions as processes. In: Echahed, R., Plump, D. (eds.) Proceedings of 7th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2013, March 2013, Rome, Electronic Proceedings in Theoretical Computer Science, vol. 110, pp. 41–55. Open Publishing Association, Sydney (2013).
4. 4.
Accattoli, B.: Linear logic and strong normalization. In: van Raamsdonk, F. (ed.) Proceedings of 29th International Conference on Rewriting Techniques and Applications, RTA 2013, June 2013, Eindhoven, Leibniz International Proceedings in Informatics, vol. 21, pp. 39–54. Dagstuhl Publishing, Saarbrücken, Wadern (2013).
5. 5.
Accattoli, B.: Proof nets and the call-by-value $$\lambda$$-calculus. Theor. Comput. Sci. 606, 2–24 (2015).
6. 6.
Accattoli, B.: Proof nets and the linear substitution calculus. arXiv preprint 1808.03395 (2018). https://arxiv.org/abs/1808.03395
7. 7.
Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Proceedings of 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, Gothenburg, September 2014, pp. 363–376. ACM Press, New York (2014).
8. 8.
Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Proceedings of 41st ACM SIGPLAG-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, January 2014, pp. 659–670. ACM Press, New York (2014).
9. 9.
Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta-reduction is invariant, indeed. Log. Methods Comput. Sci. 12(1), Article 4 (2016).
10. 10.
Accattoli, B., Guerrini, S.: Jumping boxes. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 55–70. Springer, Heidelberg (2009).
11. 11.
Accattoli, B., Kesner, D.: The structural $$\lambda$$-calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381–395. Springer, Heidelberg (2010).
12. 12.
Accattoli, B., Kesner, D.: Preservation of strong normalisation modulo permutations for the structural $$\lambda$$-calculus. Log. Methods Comput. Sci. 8(1), Article 28 (2012).
13. 13.
Asperti, A., Laneve, C.: Comparing $$\lambda$$-calculus translations in sharing graphs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 1–15. Springer, Heidelberg (1995).
14. 14.
Barenbaum, P., Bonelli, E.: Optimality and the linear substitution calculus. In: Miller, D. (ed.) Proceedings of of 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Oxford, September 2017. Leibniz International Proceedings in Informatics, vol. 84, Article 9. Dagstuhl Publishing, Saarbrücken/Wadern (2017).
15. 15.
Danos, V., Regnier, L.: Proof-nets and the Hilbert space. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol. 222, pp. 307–328. Cambridge University Press (1995).
16. 16.
Danos, V.: La Logique Linéaire appliqué à l’étude de divers processus de normalisation (principalement du $$\lambda$$-calcul). Ph.D. thesis, Université Paris 7 (1990)Google Scholar
17. 17.
Danos, V., Regnier, L.: Reversible, irreversible and optimal $$\lambda$$-machines. Theor. Comput. Sci. 227(1–2), 79–97 (1999).
18. 18.
19. 19.
Di Cosmo, R., Kesner, D.: Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract). In: Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science, LICS 1997, Warsaw, June–July 1997, pp. 35–46. IEEE CS Press, Washington, D.C. (1997).
20. 20.
Di Cosmo, R., Kesner, D., Polonowski, E.: Proof nets and explicit substitutions. Math. Struct. Comput. Sci. 13(3), 409–450 (2003).
21. 21.
Ehrhard, T., Regnier, L.: Differential interaction nets. Electron. Notes Theor. Comput. Sci. 123, 35–74 (2005).
22. 22.
Fernández, M., Siafakas, N.: Labelled calculi of resources. J. Log. Comput. 24(3), 591–613 (2014).
23. 23.
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987).
24. 24.
Guerrini, S.: Proof nets and the $$\lambda$$-calculus. In: Ehrhard, T., Girard, J.-Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science. London Mathematical Society Lecture Note Series, vol. 316, pp. 65–118. Cambridge University Press (2004).
25. 25.
Gundersen, T., Heijltjes, W., Parigot, M.: Atomic $$\lambda$$ calculus: a typed $$\lambda$$-calculus with explicit sharing. In: Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, June 2015, pp. 311–320. IEEE CS Press, Washington, D.C. (2013).
26. 26.
Kesner, D.: Reasoning about call-by-need by means of types. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 424–441. Springer, Heidelberg (2016).
27. 27.
Kesner, D., Conchúirl, S.Ó.: Milner’s $$\lambda$$ calculus with partial substitutions. Technical report, Université Paris 7 (2008). https://www.irif.fr/~kesner/papers/shortpartial.pdf
28. 28.
Kesner, D., Lengrand, S.: Extending the explicit substitution paradigm. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 407–422. Springer, Heidelberg (2005).
29. 29.
Kesner, D., Renaud, F.: The prismoid of resources. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 464–476. Springer, Heidelberg (2009).
30. 30.
Kesner, D., Ventura, D.: Quantitative types for the linear substitution calculus. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 296–310. Springer, Heidelberg (2014).
31. 31.
Laurent, O.: Étude de la polarisation en logique. Ph.D. thesis, University Aix-Marseille II (2002)Google Scholar
32. 32.
Laurent, O.: Polarized proof-nets and $$\lambda \mu$$-calculus. Theor. Comput. Sci. 290(1), 161–188 (2003).
33. 33.
Lévy, J.-J.: Réductions correctes et optimales dans le $$\lambda$$-calcul. Ph.D. thesis, University Paris VII (1978)Google Scholar
34. 34.
Mackie, I.: Encoding strategies in the $$\Lambda$$ calculus with interaction nets. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol. 4015, pp. 19–36. Springer, Heidelberg (2006).
35. 35.
Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theor. Comput. Sci. 135(1), 111–137 (1994).
36. 36.
Mellies, P.-A.: Typed $$\lambda$$-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328–334. Springer, Heidelberg (1995).
37. 37.
Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119–141 (1992).
38. 38.
Milner, R.: Bigraphical reactive systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 16–35. Springer, Heidelberg (2001).
39. 39.
Milner, R.: Local bigraphs and confluence: two conjectures (extended abstract). Electron. Notes Theor. Comput. Sci. 175(3), 65–73 (2007).
40. 40.
Muroya, K., Ghica, D.R.: The dynamic geometry of interaction machine: a call-by-need graph rewriter. In: Goranko, V., Dam, M. (eds.) Proceeding of 26th EACSL Annual Conference, CSL 2017, Stockholm, August 2017. Leibniz International Proceedings in Informatics, vol. 82, Article 32. Dagstuhl Publishing, Saarbrücken/Wadern (2017).
41. 41.
Regnier, L.: $$\lambda$$-calcul et réseaux. Ph.D. thesis, University Paris VII (1992)Google Scholar
42. 42.
Regnier, L.: Une équivalence sur les $$\lambda$$-termes. Theor. Comput. Sci. 126(2), 281–292 (1994).
43. 43.
Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)Google Scholar
44. 44.
Tranquilli, P.: Nets between determinism and nondeterminism. Ph.D. thesis, Universitá degli Studi Roma Tre/University Paris Diderot (2009)Google Scholar
45. 45.
Tranquilli, P.: Intuitionistic differential nets and $$\lambda$$-calculus. Theor. Comput. Sci. 412(20), 1979–1997 (2011).
46. 46.
Vaux, L.: $$\lambda$$-calcul différentiel et logique classique: interactions calculatoires. Ph.D. thesis, University Aix-Marseille II (2007)Google Scholar
47. 47.
Wadsworth, C.P.: Semantics and pragmatics of the $$\lambda$$-calculus. Ph.D. thesis, University of Oxford (1971)Google Scholar