The Bang Calculus Revisited | SpringerLink
Skip to main content
Springer Nature Link
Log in

The Bang Calculus Revisited

  • Conference paper
  • First Online:
Functional and Logic Programming (FLOPS 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12073))

Included in the following conference series:

Abstract

Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The paradigm was recently modelled by means of the Bang Calculus, a term language connecting CBPV and Linear Logic.

This paper presents a revisited version of the Bang Calculus, called \(\lambda !\), enjoying some important properties missing in the original system. Indeed, the new calculus integrates commutative conversions to unblock value redexes while being confluent at the same time. A second contribution is related to non-idempotent types. We provide a quantitative type system for our \(\lambda !\)-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form plus the size of this normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from \(\lambda \)-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the type system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a tight one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent exact measures for them.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Indeed, there exist clash-free terms in normal form that are \(\sigma \)-reducible to normal terms with clashes, e.g.  \(R = \mathop {\text {der}}{({(\lambda {y}{.}{\lambda {x}{.}{z}})}\,{({\mathop {\text {der}}{(y)}}\,{y})})} \equiv _{\sigma } \mathop {\text {der}}{(\lambda {x}{.}{{(\lambda {y}{.}{z})}\,{({\mathop {\text {der}}{(y)}}\,{y})})}}\).

  2. 2.

    In particular, the term R is not in normal form in our framework, and it reduces to a clash term in normal form which is filtered by the type system.

References

  1. Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds. In: PACMPL, 2 (ICFP), pp. 94:1–94:30 (2018)

    Google Scholar 

  2. Accattoli, B., Guerrieri, G.: Open call-by-value. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 206–226. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_12

    Chapter  Google Scholar 

  3. Accattoli, B., Guerrieri, G.: Types of fireballs. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 45–66. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02768-1_3

    Chapter  Google Scholar 

  4. Accattoli, B., Guerrieri, G., Leberle, M.: Types by need. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 410–439. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_15

    Chapter  Google Scholar 

  5. 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). https://doi.org/10.1007/978-3-642-15205-4_30

    Chapter  Google Scholar 

  6. Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4–16. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29822-6_4

    Chapter  Google Scholar 

  7. Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics, vol. 103, revised edition. Amsterdam, North Holland (1984)

    Google Scholar 

  8. De Benedetti, E., Rocca, S.R.D.: A type assignment for \(\lambda \)-calculus complete both for FPTIME and strong normalization. Inf. Comput. 248, 195–214 (2016)

    Article  MathSciNet  Google Scholar 

  9. Bernadet, A., Lengrand, S.: Non-idempotent intersection types and strong normalisation. Log. Methods Comput. Sci. 9(4), 1–46 (2013)

    Article  MathSciNet  Google Scholar 

  10. Bezem, M., Klop, J.W., van Oostrom, V.: Term Rewriting Systems (TeReSe). Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  11. Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Log. 109(3), 205–241 (2001)

    Article  MathSciNet  Google Scholar 

  12. Bucciarelli, A., Kesner, D., Ríos, A., Viso, A.: The bang calculus revisited. Extended report (2020). https://arxiv.org/abs/2002.04011

  13. Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL 25(4), 431–464 (2017)

    Article  MathSciNet  Google Scholar 

  14. Carraro, A., Guerrieri, G.: A semantical and operational account of call-by-value solvability. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 103–118. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54830-7_7

    Chapter  MATH  Google Scholar 

  15. Chouquet, J., Tasson, C.: Taylor expansion for Call-By-Push-Value. In: International Conference on Computer Science Logic (CSL), Barcelona, Spain. LIPIcs, vol. 152, pp. 16:1–16:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2020)

    Google Scholar 

  16. Coppo, M., Dezani-Ciancaglini, M.: A new type assignment for \(\lambda \)-terms. Arch. Math. Log. 19(1), 139–156 (1978)

    Article  MathSciNet  Google Scholar 

  17. Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \(\lambda \)-calculus. Notre Dame J. Form. Log. 21(4), 685–693 (1980)

    Article  MathSciNet  Google Scholar 

  18. de Carvalho, D.: Sémantiques de la logique linéaire et temps de calcul. Ph.D. thesis, Université Aix-Marseille II (2007)

    Google Scholar 

  19. de Carvalho, D.: The relational model is injective for multiplicative exponential linear logic. In: International Conference on Computer Science Logic (CSL), Marseille, France. LIPIcs, vol. 62, pages 41:1–41:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  20. de Carvalho, D.: Execution time of \(\lambda \)-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci. 28(7), 1169–1203 (2018)

    Article  MathSciNet  Google Scholar 

  21. de Carvalho, D., dede Falco, L.T.: A semantic account of strong normalization in linear logic. Inf. Comput. 248, 104–129 (2016)

    Article  MathSciNet  Google Scholar 

  22. de Carvalho, D., Pagani, M., de Falco, L.T.: A semantic measure of the execution time in linear logic. Theor. Comput. Sci. 412(20), 1884–1902 (2011)

    Article  MathSciNet  Google Scholar 

  23. Danos, V.: La Logique Linéaire appliquée à l’étude de divers processus de normalisation (principalement du lambda-calcul). PhD thesis, Université Paris 7 (1990)

    Google Scholar 

  24. Ehrhard, T.: Collapsing non-idempotent intersection types. In: International Conference on Computer Science Logic (CSL), Fontainebleau, France. LIPIcs, vol. 16, pp. 259–273. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)

    Google Scholar 

  25. Ehrhard, T.: Call-by-push-value from a linear logic point of view. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 202–228. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_9

    Chapter  Google Scholar 

  26. Ehrhard, T., Guerrieri, G.: The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In: International Symposium on Principles and Practice of Declarative Programming (PPDP), Edinburgh, United Kingdom, pp. 174–187. ACM (2016)

    Google Scholar 

  27. Ehrhard, T., Regnier, L.: Uniformity and the Taylor expansion of ordinary lambda-terms. TCS 403(2–3), 347–372 (2008)

    Article  MathSciNet  Google Scholar 

  28. Gardner, P.: Discovering needed reductions using type theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 555–574. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-57887-0_115

    Chapter  Google Scholar 

  29. Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)

    Article  MathSciNet  Google Scholar 

  30. Girard, J.-Y.: Normal functors, power series and \(\lambda \)-calculus. Ann. Pure Appl. Log. 37(2), 129–177 (1988)

    Article  MathSciNet  Google Scholar 

  31. Guerrieri, G.: Towards a semantic measure of the execution time in call-by-value lambda-calculus. In: Joint International Workshops on Developments in Computational Models and Intersection Types and Related Systems (DCM/ITRS), Oxford, UK, EPTCS 283, pp. 57–72 (2018)

    Google Scholar 

  32. Guerrieri, G., Manzonetto, G.: The bang calculus and the two Girard’s translations. In: Joint International Workshops on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA), Oxford, UK, EPTCS, pp. 15–30 (2019)

    Google Scholar 

  33. Guerrieri, G., Pellissier, L., de Falco, L.T.: Computing connected proof(-structure)s from their taylor expansion. In: International Conference on Formal Structures for Computation and Deduction (FSCD), Porto, Portugal. LIPIcs, vol. 52, pp. 20:1–20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  34. 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). https://doi.org/10.1007/978-3-662-49630-5_25

    Chapter  MATH  Google Scholar 

  35. 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). https://doi.org/10.1007/978-3-662-44602-7_23

    Chapter  Google Scholar 

  36. Kesner, D., Vial, P.: Types as resources for classical natural deduction. In: International Conference on Formal Structures for Computation and Deduction (FSCD), Oxford, UK. LIPIcs, vol. 84, pp. 24:1–24:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  37. Levy, P.B.: Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Springer, Dordrecht (2004). https://doi.org/10.1007/978-94-007-0954-6

    Book  MATH  Google Scholar 

  38. Levy, P.B.: Call-by-push-value: decomposing call-by-value and call-by-name. High. Order Symb. Comput. 19(4), 377–414 (2006)

    Article  Google Scholar 

  39. Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci. 228(1–2), 175–210 (1999)

    Article  MathSciNet  Google Scholar 

  40. Pagani, M., della Rocca, S.R.: Solvability in resource lambda-calculus. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 358–373. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12032-9_25

    Chapter  Google Scholar 

  41. Regnier, L.: Une équivalence sur les lambda-termes. TCS 126(2), 281–292 (1994)

    Article  Google Scholar 

  42. Santo, J.E., Pinto, L., Uustalu, T.: Modal embeddings and calling paradigms. In: International Conference on Formal Structures for Computation and Deduction (FSCD), Dortmund, Germany. LIPIcs, vol. 131, pp. 18:1–18:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019)

    Google Scholar 

Download references

Acknowledgments

We are grateful to Giulio Guerrieri and Giulio Manzonetto for fruitful discussions. This work has been partially supported by LIA INFINIS/IRP SINFIN, the ECOS-Sud program PA17C01, and the ANR COCA HOLA.

Author information

Authors and Affiliations

  1. Université de Paris, CNRS, IRIF, Paris, France

    Antonio Bucciarelli & Delia Kesner

  2. Institut Universitaire de France, Paris, France

    Delia Kesner

  3. Universidad de Buenos Aires, Buenos Aires, Argentina

    Alejandro Ríos & Andrés Viso

  4. Universidad Nacional de Quilmes, Bernal, Argentina

    Andrés Viso

Authors
  1. Antonio Bucciarelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Delia Kesner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alejandro Ríos
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrés Viso
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrés Viso .

Editor information

Editors and Affiliations

  1. Tohoku University, Sendai, Japan

    Keisuke Nakano

  2. Uppsala University, Uppsala, Sweden

    Konstantinos Sagonas

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bucciarelli, A., Kesner, D., Ríos, A., Viso, A. (2020). The Bang Calculus Revisited. In: Nakano, K., Sagonas, K. (eds) Functional and Logic Programming. FLOPS 2020. Lecture Notes in Computer Science(), vol 12073. Springer, Cham. https://doi.org/10.1007/978-3-030-59025-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-59025-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-59024-6

  • Online ISBN: 978-3-030-59025-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation