Proof Nets and the Linear Substitution Calculus

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


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.



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


  1. 1.
    Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991). Scholar
  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). Scholar
  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). Scholar
  6. 6.
    Accattoli, B.: Proof nets and the linear substitution calculus. arXiv preprint 1808.03395 (2018).
  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). Scholar
  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). Scholar
  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). Scholar
  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). Scholar
  18. 18.
    Danos, V., Regnier, L.: Head linear reduction. Technical report (2004)Google Scholar
  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). Scholar
  21. 21.
    Ehrhard, T., Regnier, L.: Differential interaction nets. Electron. Notes Theor. Comput. Sci. 123, 35–74 (2005). Scholar
  22. 22.
    Fernández, M., Siafakas, N.: Labelled calculi of resources. J. Log. Comput. 24(3), 591–613 (2014). Scholar
  23. 23.
    Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987). Scholar
  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). Scholar
  27. 27.
    Kesner, D., Conchúirl, S.Ó.: Milner’s \(\lambda \) calculus with partial substitutions. Technical report, Université Paris 7 (2008).
  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). Scholar
  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). Scholar
  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). Scholar
  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). Scholar
  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). Scholar
  35. 35.
    Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theor. Comput. Sci. 135(1), 111–137 (1994). Scholar
  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). Scholar
  37. 37.
    Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119–141 (1992). Scholar
  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). Scholar
  39. 39.
    Milner, R.: Local bigraphs and confluence: two conjectures (extended abstract). Electron. Notes Theor. Comput. Sci. 175(3), 65–73 (2007). Scholar
  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). Scholar
  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). Scholar
  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

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Inria Saclay and LIX, École PolytechniquePalaiseauFrance

Personalised recommendations