Automating sized-type inference for complexity analysis

Abstract

This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.

References

1. A. Abel and B. Pientka. 2016. Well-founded Recursion with Copatterns and Sized types. JFP 26 (2016), e2.
2. E. Albert, P. Arenas, S. Genaim, and G. Puebla. 2008. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In Proc. of 15 th SAS. Springer, Heidelberg, DE, 221–237.
3. E. Albert, S. Genaim, and A. N. Masud. 2013. On the Inference of Resource Usage Upper and Lower Bounds. TOCL 14, 3 (2013), 22(1–35).
4. D. Aspinall, L. Beringer, M. Hofmann, H-W. Loidl, and A. Momigliano. 2007. A Program Logic for Resources. TCS 389, 3 (2007), 411–445.
5. M. Avanzini and U. Dal Lago. 2017. Automating Sized Type Inference for Complexity Analysis (Technical Report). CoRR cs/CC/1706.09169 (2017), 1 – 38. Available at http://www.arxiv.org/abs/1706.09169 .
6. M. Avanzini, U. Dal Lago, and G. Moser. 2015. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Proc. of 20 th ICFP. ACM, New York, NY, 152–164.
7. M. Avanzini and G. Moser. 2010. Closing the Gap Between Runtime Complexity and Polytime Computability. In Proc. of 21 st RTA (LIPIcs), Vol. 6. Dagstuhl, Saarbrücken, DE, 33–48.
8. M. Avanzini, G. Moser, and M. Schaper. 2016. TcT: Tyrolean Complexity Tool. In Proc. of 2 nd TACAS (LNCS). Springer, Heidelberg, DE, 407–423.
9. G. Barthe, B. Grégoire, and C. Riba. 2008. Type-Based Termination with Sized Products. In Proc. of 17 th CSL (LNCS), Vol. 5213. Springer, Heidelberg, DE, 493–507.
10. F. Blanqui. 2005. Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. In Proc. of 14 th CSL (LNCS), Vol. 3634. Springer, Heidelberg, DE, 135–150.
11. K. Crary and S. Weirich. 2000. Resource Bound Certification. In Proc. of 27 th POPL. ACM, New York, NY, 184–198.
12. U. Dal Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. LMCS 8, 4 (2011), 1–44.
13. U. Dal Lago and S. Martini. 2009. On Constructor Rewrite Systems and the Lambda-Calculus. In Proc. of 36 th ICALP (LNCS), Vol. 5556. Springer, Heidelberg, DE, 163–174.
14. U. Dal Lago and Barbara Petit. 2013. The Geometry of Types. In Proc. of 40 th POPL. ACM, New York, NY, 167–178.
15. U. Dal Lago and B. Petit. 2014. Linear Dependent Types in a Call-by-value Scenario. SCP 84 (2014), 77–100.
16. N. A. Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proc. of 35 th POPL. ACM, New York, NY, 133–144.
17. N. Danner, D. R. Licata, and Ramyaa. 2015. Denotational Cost Semantics for Functional Languages with Inductive Types. In Proc. of 20 th ICFP. ACM, New York, NY, 140–151.
18. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl. 2007. SAT Solving for Termination Analysis with Polynomial Interpretations. In Proc. of 10 th SAT (LNCS), Vol. 4501. Springer, Heidelberg, DE, 340–354.
19. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl. 2008. Maximal Termination. In Proc. of 19 th RTA, Vol. 5117. Springer, Heidelberg, DE, 110–125.
20. S. Gimenez and G. Moser. 2016. The Complexity of Interaction. In Proc. of 43 rd POPL. ACM, New York, NY, 243–255.
21. J. Hoffmann, K. Aehlig, and M. Hofmann. 2011. Multivariate Amortized Resource Analysis. In Proc. of 38 th POPL. ACM, New York, NY, 357–370.
22. J. Hoffmann, K. Aehlig, and M. Hofmann. 2012. Resource Aware ML. In Proc. of 24 th CAV (LNCS), Vol. 7358. Springer, Heidelberg, DE, 781–786.
23. J. Hoffmann, A. Das, and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Proc. of 44 th POPL. ACM, New York, NY, 359–373.
24. J. Hoffmann and Z. Shao. 2015a. Automatic Static Cost Analysis for Parallel Programs. In Proc. of 24 th ESOP (LNCS), Vol. 9032. Springer, Heidelberg, DE, 132–157.
25. J. Hoffmann and Z. Shao. 2015b. Type-based Amortized Resource Analysis with Integers and Arrays. JFP 25 (2015), e17.
26. J. Hughes, L. Pareto, and A. Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Proc. of 23 rd POPL (POPL ’96). ACM, New York, NY, 410–423.
27. S. Jost, K. Hammond, H.-W. Loidl, and M.Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higherorder Programs. In Proc. of 37 th POPL. ACM, New York, NY, 223–236.
28. L. Mendonça de Moura and N. Bjørner. 2008. Z3: An Efficient SMT Solver. In Proc. of 14 th TACAS (LNCS), Vol. 4963. Springer, Heidelberg, DE, 337–340.
29. A. Mycroft. 1984. Polymorphic Type Schemes and Recursive Definitions. Springer, Heidelberg, DE, 217–228.
30. C. Okasaki. 1999. Purely Functional Data Structures. Cambridge University Press, Oxford, UK.
31. R. Péchoux. 2013. Synthesis of Sup-interpretations: A Survey. TCS 467 (2013), 30–52.
32. S. L. Peyton Jones, D. Vytiniotis, S. Weirich, and M. Shields. 2007. Practical Type Inference for Arbitrary-rank Types. JFP 17, 1 (2007), 1–82.
33. A. Podelski and A. Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In Proc. 5 th VMCAI. ACM, New York, NY, 239–251.
34. O. Shkaravska, M. C. J. D. van Eekelen, and R. van Kesteren. 2009. Polynomial Size Analysis of First-Order Shapely Functions. LMCS 5, 2 (2009), 1–35.
35. M. Sinn, F. Zuleger, and H. Veith. 2014. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Proc. of 26 th CAV (LNCS), Vol. 8559. Springer, Heidelberg, DE, 745–761.
36. P. Vasconcelos. 2008. Space Cost Analysis Using Sized Types. Ph.D. Dissertation. School of Computer Science, University of St Andrews.
37. R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenstrom. 2008. The Worst Case Execution Time Problem - Overview of Methods and Survey of Tools. TECS 7, 3 (2008), 1–53.
38. H. Zankl and A. Middeldorp. 2010. Satisfiability of Non-linear (Ir)rational Arithmetic. In Proc. of 16 th LPAR (LNCS), Vol. 6355. Springer, Heidelberg, DE, 481–500.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Functional languages

• Theory of computation

  • Logic

    • Automated reasoning

    • Equational logic and rewriting

  • Semantics and reasoning

    • Program reasoning

      • Program analysis