Nils Anders Danielsson
ABSTRACT
Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.
- Ralph Benzinger. Automated higher-order complexity analysis. Theoretical Computer Science, 318:79--103, 2004. Google Scholar
Digital Library
- Bror Bjerner and Sören Holmström. A compositional approach to time analysis of first order lazy functional programs. In FPCA '89, pages 157--165, 1989. Google ScholarDigital Library
- Bror Bjerner. Time Complexity of Programs in Type Theory. PhD thesis, Department of Computer Science, University of Göteborg, 1989.Google Scholar
- Edwin Brady and Kevin Hammond. A dependently typed framework for static analysis of program execution costs. In IFL 2005, volume 4015 of LNCS, pages 74--90, 2006. Google ScholarDigital Library
- Edwin Brady, Conor McBride, and James McKinna. Inductive families need not store their indices. In TYPES 2003: Types for Proofs and Programs, volume 3085 of LNCS, pages 115--129, 2004.Google ScholarCross Ref
- Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1(2):1--28, 2005.Google ScholarCross Ref
- Robert L. Constable and Karl Crary. Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, chapter Computational Complexity and Induction for Partial Computable Functions in Type Theory. A K Peters Ltd, 2002.Google Scholar
- Karl Crary and Stephanie Weirich. Resource bound certification. In POPL '00, pages 184--198, 2000. Google ScholarDigital Library
- Nils Anders Danielsson. A formalisation of the correctness result from "Lightweight semiformal time complexity analysis for purely functional data structures". Technical Report 2007:16, Department of Computer Science and Engineering, Chalmers University of Technology, 2007.Google Scholar
- Peter Dybjer. Inductive families. Formal Aspects of Computing, 6(4):440--465, 1994.Google ScholarDigital Library
- Ralf Hinze and Ross Paterson. Finger trees: A simple general-purpose data structure. Journal of Functional Programming, 16(2):197--217, 2006. Google ScholarDigital Library
- Martin Hofmann and Steffen Jost. Type-based amortised heap-space analysis. In ESOP 2006, volume 3924 of LNCS, pages 22--37, 2006. Google ScholarDigital Library
- John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In POPL '96, pages 410--423, 1996. Google ScholarDigital Library
- Haim Kaplan, Chris Okasaki, and Robert E. Tarjan. Simple confluently persistent catenable lists. SIAM Journal on Computing, 30(3):965--977, 2000. Google ScholarDigital Library
- Haim Kaplan and Robert E. Tarjan. Purely functional, real-time deques with catenation. Journal of the ACM, 46(5):577--603, 1999. Google ScholarDigital Library
- John Launchbury. A natural semantics for lazy evaluation. In POPL '93, pages 144--154, 1993. Google ScholarDigital Library
- Daan Leijen and Erik Meijer. Domain specific embedded compilers. In 2nd USENIX Conference on Domain--Specific Languages (DSL '99), pages 109--122, 1999. Google ScholarDigital Library
- Andrew Moran and David Sands. Improvement in a lazy context: an operational theory for call-by-need. In POPL '99, pages 43--56, 1999. Google ScholarDigital Library
- Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University, 2007.Google Scholar
- Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google ScholarDigital Library
- Christine Paulin-Mohring. Extracting Fω's programs from proofs in the calculus of constructions. In POPL '89, pages 89--104, 1989. Google ScholarDigital Library
- Simon Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.Google Scholar
- Álvaro J. Rebón Portillo, Kevin Hammond, Hans-Wolfgang Loidl, and Pedro Vasconcelos. Cost analysis using automatic size and time inference. In IFL 2002, volume 2670 of LNCS, pages 232--247, 2003. Google ScholarDigital Library
- David Sands. A naïve time analysis and its theory of cost equivalence. Journal of Logic and Computation, 5(4):495--541, 1995.Google ScholarCross Ref
- The Agda Team. The Agda Wiki. Available at http://www.cs.chalmers.se/~ulfn/Agda/, 2007.Google Scholar
- Philip Wadler. Strictness analysis aids time analysis. In POPL '88, pages 119--132, 1988. Google ScholarDigital Library
Index Terms
- Lightweight semiformal time complexity analysis for purely functional data structures
Recommendations
Lightweight semiformal time complexity analysis for purely functional data structures
POPL '08Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis ...
Purely functional, real-time deques with catenation
We describe an efficient, purely functional implementation of deques with catenation. In addition to being an intriguing problem in its own right, finding a purely functional implementation of catenable deques is required to add certain sophisticated ...
Automatic amortised analysis of dynamic memory allocation for lazy functional programs
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingThis paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and ...
Comments