Skip to main content
SpringerLink
Log in

Standardization and Böhm Trees for Λμ-Calculus

  • Conference paper
Functional and Logic Programming (FLOPS 2010)

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

Included in the following conference series:

Abstract

Λμ-calculus is an extension of Parigot’s λμ-calculus which (i) satisfies Separation theorem: it is Böhm-complete, (ii) corresponds to CBN delimited control and (iii) is provided with a stream interpretation.

In the present paper, we study solvability and investigate Böhm trees for Λμ-calculus. Moreover, we make clear the connections between Λμ-calculus and infinitary λ-calculi. After establishing a standardization theorem for Λμ-calculus, we characterize solvability. Then, we study infinite Λμ-Böhm trees, which are Böhm-like trees for Λμ-calculus; this allows to strengthen the separation results that we established previously for Λμ-calculus and to shed a new light on the failure of separation in Parigot’s original λμ-calculus.

Our construction clarifies Λμ-calculus both as an infinitary calculus and as a core language for dealing with streams as primitive objects.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ariola, Z., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 871–885. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  2. Baba, K., Hirokawa, S., etsu Fujita, K.: Parallel reduction in type free lambda/mu-calculus. Electronic Notes in Theoretical Computer Science 42 (2001)

    Google Scholar 

  3. Berarducci, A.: Infinite lambda-calculus and non-sensible models. In: Ursini, A., Aglianò, P. (eds.) Logic and Algebra (Pontignano 1994). Lecture Notes in Pure and Applied Mathematics Series, vol. 180, pp. 339–378. Marcel Dekker Inc., New York (1996)

    Google Scholar 

  4. Berarducci, A., Dezani, M.: Infinite lambda-calculus and types. TCS 212(1-2), 29–75 (1999)

    Article  MATH  Google Scholar 

  5. Böhm, C.: Alcune proprietà delle forme βη-normali nel λK-calcolo. Publicazioni dell’Istituto per le Applicazioni del Calcolo, 696 (1968)

    Google Scholar 

  6. Curien, P.-L., Herbelin, H.: Computing with abstract Böhm trees. In: Third Fuji International Symposium on Functional and Logic Programming, Kyoto. World Scientific, Singapore (1998)

    Google Scholar 

  7. Danvy, O., Filinski, A.: Abstracting control. In: LISP and Functional Programming, pp. 151–160 (1990)

    Google Scholar 

  8. David, R., Py, W.: λμ-calculus and Böhm’s theorem. Journal of Symbolic Logic (2001)

    Google Scholar 

  9. Dezani, M., Severi, P., de Vries, F.-J.: Infinitary lambda calculus and discrimination of Berarducci trees. TCS 2(298), 275–302 (2003)

    Article  Google Scholar 

  10. Felleisen, M., Friedman, D.P., Kohlbecker, E.E., Duba, B.F.: A syntactic theory of sequential control. TCS 52, 205–237 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  11. Filinski, A.: Representing monads. In: Conf. Record 21st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 1994, Portland, OR, USA, January 17-21, pp. 446–457. Association for Computing Machinery (1994)

    Google Scholar 

  12. Girard, J.-Y.: Locus solum. Mathematical Structures in Computer Science 11, 301–506 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  13. Griffin, T.: A formulae-as-types notion of control. In: Principles of Programming Languages. IEEE Computer Society Press, Los Alamitos (1990)

    Google Scholar 

  14. Herbelin, H., Ghilezan, S.: An approach to call-by-name delimited continuations. In: Principles of Programming Languages, ACM Sigplan (January 2008)

    Google Scholar 

  15. Howard, W.A.: The formulae-as-type notion of construction. In: Seldin, J.P., Hindley, R. (eds.) To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 479–490. Academic Press, New York (1980)

    Google Scholar 

  16. Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.-J.: Infinitary lambda calculi and böhm models. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 257–270. Springer, Heidelberg (1995)

    Google Scholar 

  17. Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.-J.: Infinitary lambda calculus. TCS 175(1), 93–125 (1997)

    Article  MATH  Google Scholar 

  18. Kiselyov, O.: Call-by-name linguistic side effects. In: ESSLLI 2008 Workshop on Symmetric calculi and Ludics for the semantic interpretation (2008)

    Google Scholar 

  19. Klop, J.W.: Combinatory Reduction Systems. Ph.D. thesis, State University of Utrecht (1980)

    Google Scholar 

  20. Krivine, J.-L.: Lambda-calculus, Types and Models. Ellis Horwood (1993)

    Google Scholar 

  21. Lassen, S.: Head normal form bisimulation for pairs and the λμ-calculus. In: Logic In Computer Science. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  22. Loew, T.: Locally Boolean Domains and Universal Models for Infinitary Sequential Languages. PhD thesis, Darmstadt University (2006)

    Google Scholar 

  23. Maurel, F.: Un cadre quantitatif pour la Ludique. PhD thesis, Université Paris VII (2004)

    Google Scholar 

  24. Pagani, M., Saurin, A.: Stream associative nets and Λμ-calculus. Technical Report 6431, INRIA (January 2008)

    Google Scholar 

  25. Parigot, M.: Free deduction: An analysis of “computations” in classical logic. In: Voronkov, A. (ed.) RCLP 1990 and RCLP 1991. LNCS, vol. 592, pp. 361–380. Springer, Heidelberg (1992)

    Google Scholar 

  26. Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  27. Parigot, M.: Strong normalization for second order classical natural deduction. In: Vardi, M. (ed.) Eighth Annual Symposium on Logic in Computer Science, pp. 39–46. IEEE, Los Alamitos (1993)

    Chapter  Google Scholar 

  28. Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. Journal of Symbolic Logic 62(4), 1461–1479 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  29. Py, W.: Confluence en λμ-calcul. PhD thesis, Université de Savoie (1998)

    Google Scholar 

  30. Saurin, A.: Separation with streams in the Λμ-calculus. In: Logic In Computer Science, Chicago, pp. 356–365. IEEE Computer Society Press, Los Alamitos (2005)

    Google Scholar 

  31. Saurin, A.: On the relations between the syntactic theories of λμ-calculi. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 154–168. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  32. Saurin, A.: Une étude logique du contrôle, appliquée à la programmation fonctionnelle et logique. PhD thesis, École Polytechnique (September 2008)

    Google Scholar 

  33. Saurin, A.: Typing streams in the Λμ-calculus. ACM Transactions on Computational Logic (2009) (to appear)

    Google Scholar 

  34. Saurin, A.: A hierarchy for delimited continuations in call-by-name. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 374–388. Springer, Heidelberg (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. PPS & INRIA π r2,  

    Alexis Saurin

Authors
  1. Alexis Saurin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Google, 20 West Kinzie Street, 60610, Chicago, IL, USA

    Matthias Blume

  2. Department of Computer and Mathematical Sciences, Tohoku University, 6-3-9 Aoba, Aramaki, Aoba-ku, Sendai-shi, 980-8579, Miyagi, Japan

    Naoki Kobayashi

  3. DSIC, MiST, Technical University of Valencia, Camino de Vera, S/N, 46022, Valencia, Spain

    Germán Vidal

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Saurin, A. (2010). Standardization and Böhm Trees for Λμ-Calculus. In: Blume, M., Kobayashi, N., Vidal, G. (eds) Functional and Logic Programming. FLOPS 2010. Lecture Notes in Computer Science, vol 6009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12251-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-12251-4_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-12250-7

  • Online ISBN: 978-3-642-12251-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation