nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

The Negligible and Yet Subtle Cost of Pattern Matching

verfasst von : Beniamino Accattoli, Bruno Barras

Erschienen in: Programming Languages and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The model behind functional programming languages is the closed \(\lambda \) -calculus, that is, the fragment of the \(\lambda \)-calculus where evaluation is weak (i.e. out of abstractions) and terms are closed. It is well-known that the number of \(\beta \) (i.e. evaluation) steps is a reasonable cost model in this setting, for all natural evaluation strategies (call-by-name/value/need). In this paper we try to close the gap between the closed \(\lambda \)-calculus and actual languages, by considering an extension of the \(\lambda \)-calculus with pattern matching. It is straightforward to prove that \(\beta \) plus matching steps provide a reasonable cost model. What we do then is finer: we show that \(\beta \) steps only, without matching steps, provide a reasonable cost model also in this extended setting—morally, pattern matching comes for free, complexity-wise. The result is proven for all evaluation strategies (name/value/need), and, while the proof itself is simple, the problem is shown to be subtle. In particular we show that qualitatively equivalent definitions of call-by-need may behave very differently.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Partiality and Container Monads

Nächstes Kapitel A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls

The kernel of Coq is the subset of the codebase which ensures that only valid proofs are accepted. Hence the use of an abstract machine, which has a better ratio efficiency/complexity than the use of a compiler or a naive interpreter.

We do not prove the equivalence between the two formulations of CbNeed studied in the paper, but the difference is essentially that in one case \(\mathtt{c}(\varvec{t})\) is reduced to

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-71237-6_21/460753_1_En_21_IEq378_HTML.gif

(via \(\rightarrow _{\mathtt{cstr}}\)) while in the other case it is left unchanged—the two calculi compute the same result, up to substitutions, just with very different complexities.

Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991)MathSciNetCrossRefMATH

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

Accattoli, B.: COCA HOLA (2016). https://sites.google.com/site/beniaminoaccattoli/coca-hola

Accattoli, B.: The complexity of abstract machines. In: WPTE@FSCD 2016, pp. 1–15 (2016)

Accattoli, B.: The useful MAM, a reasonable implementation of the strong \(\lambda \)-calculus. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 1–21. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-52921-8_1

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

Accattoli, B., Barras, B.: Environments and the complexity of abstract machines (2017). Accepted to PPDP 2017

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

Accattoli, B., Coen, C.S.: On the relative usefulness of fireballs. In: LICS 2015, pp. 141–155. IEEE Computer Society (2015)

10.

Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Logical Methods Comput. Sci. 12(1), 1–46 (2016)MathSciNetCrossRefMATH

11.

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 CrossRef

12.

Accattoli, B., Guerrieri, G.: Implementing open call-by-value. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 1–19. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68972-2_1 CrossRef

13.

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 CrossRef

14.

Accattoli, B., Sacerdoti Coen, C.: On the value of variables. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds.) WoLLIC 2014. LNCS, vol. 8652, pp. 36–50. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44145-9_3

15.

Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)MathSciNetCrossRefMATH

16.

Barras, B.: Auto-validation d’un système de preuves avec familles inductives. Ph.D. thesis, Université Paris 7 (1999)

17.

Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: FPCA 1995, pp. 226–237. ACM (1995)

18.

Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 137–153. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_9

19.

Cirstea, H., Kirchner, C.: The rewriting calculus - part I. Logic J. IGPL 9(3), 339–375 (2001)MathSciNetCrossRefMATH

20.

Coq Development Team: The coq proof-assistant reference manual, version 8.6 (2016). http://coq.inria.fr

21.

Dal Lago, U., Martini, S.: Derivational complexity is an invariant cost model. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 100–113. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15331-0_7 CrossRef

22.

Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 163–174. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_14 CrossRef

23.

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

24.

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

25.

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

26.

Jay, C.B., Kesner, D.: First-class patterns. J. Funct. Program. 19(2), 191–225 (2009)MathSciNetCrossRefMATH

27.

Jeannin, J., Kozen, D.: Computing with capsules. J. Automata Lang. Comb. 17(2–4), 185–204 (2012)MathSciNetMATH

28.

Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238–252. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74915-8_20 CrossRef

29.

Klop, J.W., van Oostrom, V., de Vrijer, R.C.: Lambda calculus with patterns. Theor. Comput. Sci. 398(1–3), 16–31 (2008)MathSciNetCrossRefMATH

30.

Launchbury, J.: A natural semantics for lazy evaluation. In: POPL 1993, pp. 144–154. ACM Press (1993)

31.

Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275–317 (1998)MathSciNetCrossRefMATH

32.

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

33.

Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)MATH

34.

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). https://doi.org/10.1007/3-540-36377-7_4 CrossRef

35.

Sergey, I., Vytiniotis, D., Peyton Jones, S.L.: Modular, higher-order cardinality analysis in theory and practice. In: POPL 2014, pp. 335–348 (2014)

36.

Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231–264 (1997)MathSciNetCrossRefMATH

37.

Wadsworth, C.P.: Semantics and pragmatics of the lambda-calculus. Ph.D. thesis, Oxford (1971). Chapter 4

38.

Walker, D.: Substructural type systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 3–43. The MIT Press (2004)

39.

Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)MathSciNetCrossRefMATH

Titel: The Negligible and Yet Subtle Cost of Pattern Matching
verfasst von: Beniamino Accattoli
Bruno Barras
Verlag: Springer International Publishing
Buch: Programming Languages and Systems
Print ISBN: 978-3-319-71236-9

Electronic ISBN: 978-3-319-71237-6

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-71237-6_21

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner