Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion

  • Giulio Manzonetto
  • Michele Pagani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


We study the resource calculus, an extension of the λ-calculus allowing to model resource consumption. We achieve an internal separation result, in analogy with Böhm’s theorem of λ-calculus. We define an equivalence relation on the terms, which we prove to be the maximal non-trivial congruence on normalizable terms respecting β-reduction. It is significant that this equivalence extends the usual η-equivalence and is related to Ehrhard’s Taylor expansion – a translation mapping terms into series of finite resources.


differential linear logic resource lambda-calculus separation property Böhm-out technique 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Böhm, C.: Alcune proprietà delle forme β-η-normali nel λ-K-calcolo. Pubbl. INAC 696 (1968)Google Scholar
  2. 2.
    Barendregt, H.: The lambda-calculus, its syntax and semantics, 2nd edn. Stud. Logic Found. Math., vol. 103. North-Holland, Amsterdam (1984)zbMATHGoogle Scholar
  3. 3.
    Böhm, C., Dezani-Ciancaglini, M., Peretti, P., Ronchi Della Rocca, S.: A discrimination algorithm inside λβ-calculus. Theor. Comp. Sci. 8(3), 271–291 (1979)CrossRefzbMATHGoogle Scholar
  4. 4.
    Hyland, J.M.E.: A syntactic characterization of the equality in some models of the lambda calculus. J. London Math. Soc. 2(12), 361–370 (1976)CrossRefzbMATHGoogle Scholar
  5. 5.
    Girard, J.Y.: Linear logic. Th. Comp. Sc. 50, 1–102 (1987)CrossRefzbMATHGoogle Scholar
  6. 6.
    Carraro, A., Ehrhard, T., Salibra, A.: Exponentials with infinite multiplicities. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 170–184. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Pagani, M., Ronchi Della Rocca, S.: Linearity, non-determinism and solvability. Fundamenta Informaticae 103(1-4), 173–202 (2010)zbMATHGoogle Scholar
  8. 8.
    Boudol, G.: The lambda-calculus with multiplicities. INRIA Report 2025 (1993)Google Scholar
  9. 9.
    Boudol, G., Laneve, C.: The discriminating power of multiplicities in the lambda-calculus. Inf. Comput. 126(1), 83–102 (1996)CrossRefzbMATHGoogle Scholar
  10. 10.
    Boudol, G., Curien, P.L., Lavatelli, C.: A semantics for lambda calculi with resources. MSCS 9(4), 437–482 (1999)zbMATHGoogle Scholar
  11. 11.
    Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theor. Comput. Sci. 309(1), 1–41 (2003)CrossRefzbMATHGoogle Scholar
  12. 12.
    Tranquilli, P.: Intuitionistic differential nets and lambda-calculus. Theor. Comput. Sci. (2008) (to appear)Google Scholar
  13. 13.
    Bucciarelli, A., Carraro, A., Ehrhard, T., Manzonetto, G.: Full abstraction for resource calculus with tests (submitted),
  14. 14.
    Ehrhard, T., Regnier, L.: Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. 403(2-3), 347–372 (2008)CrossRefzbMATHGoogle Scholar
  15. 15.
    Pagani, M., Tranquilli, P.: Parallel reduction in resource lambda-calculus. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 226–242. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Manzonetto, G.: What is a categorical model of the differential and the resource λ-calculi? (submitted),
  17. 17.
    Terese.: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Giulio Manzonetto
    • 1
  • Michele Pagani
    • 2
  1. 1.Intelligent SystemsRadboud UniversityThe Netherlands
  2. 2.Laboratoire LIPN, CNRS UMR7030Université Paris 13France

Personalised recommendations