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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Modulo the presence of markers of the form and in the environment, which are needed for bookkeeping purposes and were omitted here.
References
Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)
Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: RTA, pp. 6–21 (2012)
Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP, pp. 363–376 (2014)
Accattoli, B., Barenbaum, P., Mazza, D.: A strong distillery. CoRR abs/1509.00996 (2015). http://arxiv.org/abs/1509.00996
Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: POPL, pp. 659–670 (2014)
Accattoli, B., Dal Lago, U.: Beta Reduction is Invariant, Indeed. In: CSL-LICS, p. 8 (2014)
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)
Accattoli, B., Sacerdoti Coen, C.: On the relative usefulness of fireballs. In: LICS, pp. 141–155 (2015)
Ariola, Z.M., Bohannon, A., Sabry, A.: Sequent calculi and abstract machines. ACM Trans. Program. Lang. Syst. 31(4) (2009). Article No. 13
Biernacka, M., Danvy, O.: A concrete framework for environment machines. ACM Trans. Comput. Log. 9(1) (2007). Article No. 6
Boutiller, P.: De nouveaus outils pour manipuler les inductif en Coq. Ph.D. thesis, Université Paris Diderot - Paris 7 (2014)
de Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. CoRR abs/0905.4251 (2009)
Crégut, P.: An abstract machine for lambda-terms normalization. In: LISP and Functional Programming, pp. 333–340 (1990)
Crégut, P.: Strongly reducing variants of the Krivine abstract machine. High.-Order Symbolic Comput. 20(3), 209–230 (2007)
Curien, P.: An abstract framework for environment machines. Theor. Comput. Sci. 82(2), 389–402 (1991)
Danos, V., Regnier, L.: Head linear reduction (2004). (unpublished)
Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Technical Report RS-04-26, BRICS (2004)
Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP, pp. 97–108 (2013)
Dénès, M.: Étude formelle d’algorithmes efficaces en algèbre linéaire. Ph.D. thesis, Université de Nice - Sophia Antipolis (2013)
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)
Fernández, M., Siafakas, N.: New developments in environment machines. Electr. Notes Theor. Comput. Sci. 237, 57–73 (2009)
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)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP, pp. 235–246 (2002)
Hardin, T., Maranget, L.: Functional runtime systems within the lambda-sigma calculus. J. Funct. Program. 8(2), 131–176 (1998)
Lang, F.: Explaining the lazy Krivine machine using explicit substitution and addresses. High.-Order Symbolic Comput. 20(3), 257–270 (2007)
Mascari, G., Pedicini, M.: Head linear reduction and pure proof net extraction. Theor. Comput. Sci. 135(1), 111–137 (1994)
Milner, R.: Local bigraphs and confluence: two conjectures. Electr. Notes Theor. Comput. Sci. 175(3), 65–73 (2007)
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)
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)
Smith, C.: Abstract machines for higher-order term sharing, Presented at IFL 2014
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)