Skip to main content
SpringerLink
Log in

A Strong Distillery

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9458))

Included in the following conference series:

Abstract

Abstract machines for the strong evaluation of \(\lambda \)-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.

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 EPUB and 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

Notes

  1. 1.

    Modulo the presence of markers of the form and in the environment, which are needed for bookkeeping purposes and were omitted here.

References

  1. Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  2. Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: RTA, pp. 6–21 (2012)

    Google Scholar 

  3. Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP, pp. 363–376 (2014)

    Google Scholar 

  4. Accattoli, B., Barenbaum, P., Mazza, D.: A strong distillery. CoRR abs/1509.00996 (2015). http://arxiv.org/abs/1509.00996

  5. Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: POPL, pp. 659–670 (2014)

    Google Scholar 

  6. Accattoli, B., Dal Lago, U.: Beta Reduction is Invariant, Indeed. In: CSL-LICS, p. 8 (2014)

    Google Scholar 

  7. Accattoli, B., Sacerdoti Coen, C.: On the value of variables. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds.) WoLLIC. LNCS, vol. 8652, pp. 36–50. Springer, Heidelberg (2014)

    Google Scholar 

  8. Accattoli, B., Sacerdoti Coen, C.: On the relative usefulness of fireballs. In: LICS, pp. 141–155 (2015)

    Google Scholar 

  9. Ariola, Z.M., Bohannon, A., Sabry, A.: Sequent calculi and abstract machines. ACM Trans. Program. Lang. Syst. 31(4) (2009). Article No. 13

    Google Scholar 

  10. Biernacka, M., Danvy, O.: A concrete framework for environment machines. ACM Trans. Comput. Log. 9(1) (2007). Article No. 6

    Google Scholar 

  11. Boutiller, P.: De nouveaus outils pour manipuler les inductif en Coq. Ph.D. thesis, Université Paris Diderot - Paris 7 (2014)

    Google Scholar 

  12. de Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. CoRR abs/0905.4251 (2009)

    Google Scholar 

  13. Crégut, P.: An abstract machine for lambda-terms normalization. In: LISP and Functional Programming, pp. 333–340 (1990)

    Google Scholar 

  14. Crégut, P.: Strongly reducing variants of the Krivine abstract machine. High.-Order Symbolic Comput. 20(3), 209–230 (2007)

    Article  MATH  Google Scholar 

  15. Curien, P.: An abstract framework for environment machines. Theor. Comput. Sci. 82(2), 389–402 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  16. Danos, V., Regnier, L.: Head linear reduction (2004). (unpublished)

    Google Scholar 

  17. Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Technical Report RS-04-26, BRICS (2004)

    Google Scholar 

  18. Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP, pp. 97–108 (2013)

    Google Scholar 

  19. Dénès, M.: Étude formelle d’algorithmes efficaces en algèbre linéaire. Ph.D. thesis, Université de Nice - Sophia Antipolis (2013)

    Google Scholar 

  20. Ehrhard, T., Regnier, L.: Böhm trees, Krivine’s machine and the taylor expansion of lambda-terms. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 186–197. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Fernández, M., Siafakas, N.: New developments in environment machines. Electr. Notes Theor. Comput. Sci. 237, 57–73 (2009)

    Article  Google Scholar 

  22. García-Pérez, Á., Nogueira, P., Moreno-Navarro, J.J.: Deriving the full-reducing krivine machine from the small-step operational semantics of normal order. In: PPDP, pp. 85–96 (2013)

    Google Scholar 

  23. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP, pp. 235–246 (2002)

    Google Scholar 

  24. Hardin, T., Maranget, L.: Functional runtime systems within the lambda-sigma calculus. J. Funct. Program. 8(2), 131–176 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  25. Lang, F.: Explaining the lazy Krivine machine using explicit substitution and addresses. High.-Order Symbolic Comput. 20(3), 257–270 (2007)

    Article  MATH  Google Scholar 

  26. Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theor. Comput. Sci. 135(1), 111–137 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  27. Milner, R.: Local bigraphs and confluence: two conjectures. Electr. Notes Theor. Comput. Sci. 175(3), 65–73 (2007)

    Article  MathSciNet  Google Scholar 

  28. Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  29. Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 60–82. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Smith, C.: Abstract machines for higher-order term sharing, Presented at IFL 2014

    Google Scholar 

Download references

Acknowledgments

This work was partially supported by projects Logoi ANR-2010-BLAN-0213-02, Coquas ANR-12-JS02-006-01, Elica ANR-14-CE25-0005, the Saint-Exupéry program funded by the French embassy and the Ministry of Education in Argentina, and the French–Argentinian laboratory in Computer Science INFINIS.

Author information

Authors and Affiliations

  1. LIX, Inria-École Polytechnique, Palaiseau, France

    Beniamino Accattoli

  2. CONICET, University of Buenos Aires, Buenos Aires, Argentina

    Pablo Barenbaum

  3. LIPN, CNRS-Université Paris 13, Sorbonne Paris Cité, Villetaneuse, France

    Damiano Mazza

Authors
  1. Beniamino Accattoli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pablo Barenbaum
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Damiano Mazza
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Damiano Mazza .

Editor information

Editors and Affiliations

  1. Univ. of Science and Technology of China, Hefei, Anhui, China

    Xinyu Feng

  2. Pohang Univ. of Science and Technology, Nam-Gu, Pohang, Korea (Republic of)

    Sungwoo Park

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Accattoli, B., Barenbaum, P., Mazza, D. (2015). A Strong Distillery. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26529-2_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-26528-5

  • Online ISBN: 978-3-319-26529-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation