Document Open Access Logo

A Quantitative Understanding of Pattern Matching

Authors Sandra Alves, Delia Kesner, Daniel Ventura

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.3.pdf
  • Filesize: 0.7 MB
  • 36 pages

Document Identifiers

Author Details

Sandra Alves
  • DCC-FCUP & CRACS, University of Porto, Portugal
Delia Kesner
  • Université de Paris, CNRS, IRIF, France
  • Institut Universitaire de France, France
Daniel Ventura
  • INF, Universidade Federal de Goiás, Goiânia, Brazil

Funding

This work was partially done within the framework of ANR COCA HOLA (16-CE40-004-01). It was partially funded by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project UIDB/50014/2020 and by the Brazilian Research Council (CNPq) grant Universal 430667/2016-7.

Acknowledgements

We are grateful to Antonio Bucciarelli and Simona Ronchi Della Rocca for fruitful discussions.

Cite AsGet BibTex

Sandra Alves, Delia Kesner, and Daniel Ventura. A Quantitative Understanding of Pattern Matching. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 3:1-3:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TYPES.2019.3

Abstract

This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E, for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [Antonio Bucciarelli et al., 2015], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [Antonio Bucciarelli et al., 2015], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [Antonio Bucciarelli et al., 2015], which turn out to be an essential quantitative tool because they remove the confusion between "being a pair" and "being duplicable". Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
Keywords
  • Intersection Types
  • Pattern Matching
  • Exact Bounds

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Beniamino Accattoli and Bruno Barras. The negligible and yet subtle cost of pattern matching. In APLAS, volume 10695 of LNCS, pages 426-447. Springer, 2017. Google Scholar
  2. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1-94:30, 2018. Google Scholar
  3. Beniamino Accattoli and Giulio Guerrieri. Types of fireballs. In APLAS, volume 11275 of LNCS, pages 45-66. Springer, 2018. Google Scholar
  4. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In ESOP, volume 11423 of LNCS, pages 410-439. Springer, 2019. Google Scholar
  5. Beniamino Accattoli and Delia Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:28)2012.
  6. Sandra Alves, Besik Dundua, Mário Florido, and Temur Kutsia. Pattern-based calculi with finitary matching. Logic Journal of the IGPL, 26(2):203-243, 2018. Google Scholar
  7. Martin Avanzini and Ugo Dal Lago. Automating sized-type inference for complexity analysis. PACMPL, 1(ICFP):43:1-43:29, 2017. Google Scholar
  8. Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. PACMPL, 1(ICFP):20:1-20:29, 2017. Google Scholar
  9. Pablo Barenbaum, Eduardo Bonelli, and Kareem Mohamed. Pattern matching and fixed points: Resource types and strong call-by-need: Extended abstract. In PPDP, pages 6:1-6:12. ACM Press, 2018. Google Scholar
  10. Hendrik Pieter Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North-Holland, Amsterdam, revised edition, 1984. Google Scholar
  11. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. Google Scholar
  12. Alexis Bernadet. Types intersections non-idempotents pour raffiner la normalisation forte avec des informations quantitatives. PhD thesis, École Polytechnique, 2014. Google Scholar
  13. Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. Google Scholar
  14. Frédéric Blanqui. Size-based termination of higher-order rewriting. Journal of Functional Programming, 28:e11, 2018. Google Scholar
  15. Eduardo Bonelli, Delia Kesner, Carlos Lombardi, and Alejandro Ríos. Normalisation for dynamic pattern calculi. In RTA, volume 15 of LIPIcs, pages 117-132. Schloss Dagstuhl, 2012. Google Scholar
  16. Gérard Boudol, Pierre-Louis Curien, and Carolina Lavatelli. A semantics for lambda calculi with resources. Mathematical Structures in Computer Science, 9(4):437-482, 1999. Google Scholar
  17. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, 109(3):205-241, 2001. Google Scholar
  18. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. A relational semantics for parallelism and non-determinism in a functional setting. Annals of Pure and Applied Logic, 163(7):918-934, 2012. Google Scholar
  19. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for pair pattern calculi. In TLCA, volume 38 of LIPIcs, pages 123-137, 2015. Google Scholar
  20. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. Google Scholar
  21. Horatiu Cirstea and Claude Kirchner. The rewriting calculus - Part I. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427-463, 2001. Google Scholar
  22. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. Phd thesis, Université Aix-Marseille II, 2007. Google Scholar
  23. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. Google Scholar
  24. Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Information and Computation, 248:104-129, 2016. Google Scholar
  25. Thomas Ehrhard. Collapsing non-idempotent intersection types. In CSL, volume 16 of LIPIcs, pages 259-273. Schloss Dagstuhl, 2012. Google Scholar
  26. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In PPDP, pages 174-187. ACM Press, 2016. Google Scholar
  27. Philippa Gardner. Discovering needed reductions using type theory. In TACS, volume 789 of LNCS, pages 555-574. Springer, 1994. Google Scholar
  28. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  29. Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two girard’s translations. In Linearity-TLLA, volume 292 of EPTCS, pages 15-30, 2018. Google Scholar
  30. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Resource aware ML. In CAV, volume 7358 of LNCS, pages 781-786. Springer, 2012. Google Scholar
  31. Jan Hoffmann, Ankush Das, and Shu-Chun Weng. Towards automatic resource bound analysis for ocaml. In POPL, pages 359-373. ACM Press, 2017. Google Scholar
  32. Barry Jay and Delia Kesner. First-class patterns. Journal of Functional Programming, 19(2):191-225, 2009. Google Scholar
  33. Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. Static determination of quantitative resource usage for higher-order programs. In POPL, pages 223-236. ACM Press, 2010. Google Scholar
  34. Steffen Jost, Pedro B. Vasconcelos, Mário Florido, and Kevin Hammond. Type-based cost analysis for lazy functional languages. Journal of Automated Reasoning, 59(1):87-120, 2017. Google Scholar
  35. Wolfram Kahl. Basic pattern matching calculi: a fresh view on matching failure. In FLOPS, volume 2998 of LNCS, pages 276-290. Springer, 2004. Google Scholar
  36. Delia Kesner. Reasoning about call-by-need by means of types. In FoSSaCS, volume 9634 of LNCS, pages 424-441. Springer, 2016. Google Scholar
  37. Delia Kesner, Carlos Lombardi, and Alejandro Ríos. Standardisation for constructor based pattern calculi. In HOR, volume 49, page 58–72, 2011. Google Scholar
  38. Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In IFIP TCS, volume 8705 of LNCS, pages 296-310. Springer, 2014. Google Scholar
  39. Delia Kesner and Daniel Ventura. A resource aware computational interpretation for Herbelin’s syntax. In ICTAC, volume 9399 of LNCS, pages 388-403. Springer, 2015. Google Scholar
  40. Delia Kesner and Pierre Vial. Types as resources for classical natural deduction. In FSCD, volume 84 of LIPIcs, pages 24:1-24:17. Schloss Dagstuhl, 2017. Google Scholar
  41. Delia Kesner and Pierre Vial. Extracting exact bounds from typing in a classical framework. 25th International Conference on Types for Proofs and Programs, 2019. Google Scholar
  42. Delia Kesner and Pierre Vial. Consuming and persistent types for classical logic. In LICS. IEEE Computer Society, 2020. Google Scholar
  43. Assaf Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411-436, 2000. Google Scholar
  44. Jean Louis Krivine. Lambda-Calculus, Types and Models. Masson, Paris, and Ellis Horwood, Hemel Hempstead, 1993. Google Scholar
  45. Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. Logical Methods in Computer Science, 8(4), 2011. Google Scholar
  46. Ugo Dal Lago and Barbara Petit. Linear dependent types in a call-by-value scenario. Science of Computer Programming, 84:77-100, 2014. Google Scholar
  47. C.-H. Luke Ong. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In LICS, pages 1-12. IEEE Computer Society, 2017. Google Scholar
  48. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science, 27(5):626-650, 2017. Google Scholar
  49. Álvaro J. Rebón Portillo, Kevin Hammond, Hans-Wolfgang Loidl, and Pedro B. Vasconcelos. Cost analysis using automatic size and time inference. In IFL, volume 2670 of LNCS, pages 232-248. Springer, 2002. Google Scholar
  50. RaML. Resource Aware ML. URL: http://raml.co.
  51. Franz Siglmüller. Type-based resource analysis on haskell. In DICE-FOPARA, volume 298 of EPTCS, pages 47-60, 2019. Google Scholar
  52. Hugo R. Simões, Kevin Hammond, Mário Florido, and Pedro B. Vasconcelos. Using intersection types for cost-analysis of higher-order polymorphic functional programs. In TYPES, volume 4502 of LNCS, pages 221-236. Springer, 2006. Google Scholar
  53. Hugo R. Simões, Pedro B. Vasconcelos, Mário Florido, Steffen Jost, and Kevin Hammond. Automatic amortised analysis of dynamic memory allocation for lazy functional programs. In ICFP, pages 165-176. ACM Press, 2012. Google Scholar
  54. Pedro B. Vasconcelos and Kevin Hammond. Inferring cost equations for recursive, polymorphic and higher-order functional programs. In IFL, volume 3145 of LNCS, pages 86-101. Springer, 2003. Google Scholar
  55. Philip Wadler. The essence of functional programming. In POPL, pages 1-14. ACM Press, 1992. Google Scholar
  56. Joe B. Wells. The essence of principal typings. In ICALP, volume 2380 of LNCS, pages 913-925. Springer, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact