Lightweight semiformal time complexity analysis for purely functional data structures

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.

REFERENCES

• 1: Ralph Benzinger, Automated higher-order complexity analysis, Theoretical Computer Science, v.318 n.1-2, p.79-103, June 2004 [doi>10.1016/j.tcs.2003.10.022]
• 2: Bror Bjerner , S. Holmström, A composition approach to time analysis of first order lazy functional programs, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.157-165, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99382]
• 3: Bror Bjerner. Time Complexity of Programs in Type Theory. PhD thesis, Department of Computer Science, University of Göteborg, 1989.
• 4: 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.
• 5: 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.
• 6: Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1(2):1--28, 2005.
• 7: 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.
• 8: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 9: 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.
• 10: Peter Dybjer. Inductive families. Formal Aspects of Computing, 6(4):440--465, 1994.
• 11: Ralf Hinze , Ross Paterson, Finger trees: a simple general-purpose data structure, Journal of Functional Programming, v.16 n.2, p.197-217, March 2006 [doi>10.1017/S0956796805005769]
• 12: Martin Hofmann and Steffen Jost. Type-based amortised heap-space analysis. In ESOP 2006, volume 3924 of LNCS, pages 22--37, 2006.
• 13: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 14: Haim Kaplan , Chris Okasaki , Robert E. Tarjan, Simple Confluently Persistent Catenable Lists, SIAM Journal on Computing, v.30 n.3, p.965-977, 2000 [doi>10.1137/S0097539798339430]
• 15: Haim Kaplan , Robert E. Tarjan, Purely functional, real-time deques with catenation, Journal of the ACM (JACM), v.46 n.5, p.577-603, Sept. 1999 [doi>10.1145/324133.324139]
• 16: John Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.144-154, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158618]
• 17: Daan Leijen , Erik Meijer, Domain specific embedded compilers, Proceedings of the 2nd conference on Domain-specific languages, p.109-122, October 03-06, 1999, Austin, Texas, United States
• 18: Andrew Moran , David Sands, Improvement in a lazy context: an operational theory for call-by-need, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292547]
• 19: Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University, 2007.
• 20: Chris Okasaki, Purely functional data structures, Cambridge University Press, New York, NY, 1998
• 21: C. Paulin-Mohring, Extracting &ohgr;'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.89-104, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75285]
• 22: Simon Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.
• 23: Á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.
• 24: David Sands. A naïve time analysis and its theory of cost equivalence. Journal of Logic and Computation, 5(4):495--541, 1995.
• 25: The Agda Team. The Agda Wiki. Available at http://www.cs.chalmers.se/~ulfn/Agda/, 2007.
• 26: P. Wadler, Strictness analysis aids time analysis, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-132, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73571]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.m Miscellaneous

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

  E. Data
  E.1 DATA STRUCTURES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Performance, Theory, Verification

Keywords:
amortised time complexity, dependent types, lazy evaluation, purely functional data structures