research-article

Lightweight semiformal time complexity analysis for purely functional data structures

Author:

Nils Anders DanielssonAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 1

Pages 133 - 144

https://doi.org/10.1145/1328897.1328457

Published: 07 January 2008 Publication History

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, 318:79--103, 2004.

Digital Library

[2]

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.

Digital Library

[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.

Digital Library

[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 and Stephanie Weirich. Resource bound certification. In POPL '00, pages 184--198, 2000.

Digital Library

[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.

Digital Library

[11]

Ralf Hinze and Ross Paterson. Finger trees: A simple general-purpose data structure. Journal of Functional Programming, 16(2):197--217, 2006.

Digital Library

[12]

Martin Hofmann and Steffen Jost. Type-based amortised heap-space analysis. In ESOP 2006, volume 3924 of LNCS, pages 22--37, 2006.

Digital Library

[13]

John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In POPL '96, pages 410--423, 1996.

Digital Library

[14]

Haim Kaplan, Chris Okasaki, and Robert E. Tarjan. Simple confluently persistent catenable lists. SIAM Journal on Computing, 30(3):965--977, 2000.

Digital Library

[15]

Haim Kaplan and Robert E. Tarjan. Purely functional, real-time deques with catenation. Journal of the ACM, 46(5):577--603, 1999.

Digital Library

[16]

John Launchbury. A natural semantics for lazy evaluation. In POPL '93, pages 144--154, 1993.

Digital Library

[17]

Daan Leijen and Erik Meijer. Domain specific embedded compilers. In 2nd USENIX Conference on Domain--Specific Languages (DSL '99), pages 109--122, 1999.

Digital Library

[18]

Andrew Moran and David Sands. Improvement in a lazy context: an operational theory for call-by-need. In POPL '99, pages 43--56, 1999.

Digital Library

[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, 1998.

Digital Library

[21]

Christine Paulin-Mohring. Extracting F_ω's programs from proofs in the calculus of constructions. In POPL '89, pages 89--104, 1989.

Digital Library

[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.

Digital Library

[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]

Philip Wadler. Strictness analysis aids time analysis. In POPL '88, pages 119--132, 1988.

Digital Library

Cited By

Grosen JKahn DHoffmann J(2023)Automatic Amortized Resource Analysis with Regular Recursive Types2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175720(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175720
Avanzini MBarthe GDal Lago U(2021)On continuation-passing transformations and expected cost analysisProceedings of the ACM on Programming Languages10.1145/34735925:ICFP(1-30)Online publication date: 22-Aug-2021
https://doi.org/10.1145/3473592
Li YXia LWeirich S(2021)Reasoning about the garden of forking pathsProceedings of the ACM on Programming Languages10.1145/34735855:ICFP(1-28)Online publication date: 22-Aug-2021
https://doi.org/10.1145/3473585
Show More Cited By

Recommendations

Lightweight semiformal time complexity analysis for purely functional data structures
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
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 programming

This 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 43, Issue 1

POPL '08

January 2008

420 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1328897

Issue’s Table of Contents

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2008
448 pages
ISBN:9781595936899
DOI:10.1145/1328438
General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Published in SIGPLAN Volume 43, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

82
Total Citations
View Citations
635
Total Downloads

Downloads (Last 12 months)36
Downloads (Last 6 weeks)2

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Grosen JKahn DHoffmann J(2023)Automatic Amortized Resource Analysis with Regular Recursive Types2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175720(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175720
Avanzini MBarthe GDal Lago U(2021)On continuation-passing transformations and expected cost analysisProceedings of the ACM on Programming Languages10.1145/34735925:ICFP(1-30)Online publication date: 22-Aug-2021
https://doi.org/10.1145/3473592
Li YXia LWeirich S(2021)Reasoning about the garden of forking pathsProceedings of the ACM on Programming Languages10.1145/34735855:ICFP(1-28)Online publication date: 22-Aug-2021
https://doi.org/10.1145/3473585
Orchard DLiepelt VEades III H(2019)Quantitative program reasoning with graded modal typesProceedings of the ACM on Programming Languages10.1145/33417143:ICFP(1-30)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341714
Baillot PBarthe GDal Lago U(2019)Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic ProofsJournal of Automated Reasoning10.1007/s10817-019-09530-2Online publication date: 31-Jul-2019
https://doi.org/10.1007/s10817-019-09530-2
Handley MHutton G(2019)Improving HaskellZivilgesellschaft und Wohlfahrtsstaat im Wandel10.1007/978-3-030-18506-0_6(114-135)Online publication date: 24-Apr-2019
https://doi.org/10.1007/978-3-030-18506-0_6
Yanok INystrom NEisenberg RVazou N(2018)Implementing resource-aware safe assembly for kernel probes as a dependently-typed DSLProceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3240719.3241792(25-37)Online publication date: 27-Sep-2018
https://dl.acm.org/doi/10.1145/3240719.3241792
Orchard DYoshida N(2016)Effects as sessions, sessions as effectsACM SIGPLAN Notices10.1145/2914770.283763451:1(568-581)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837634
Yanok INystrom N(2016)TapirACM SIGOPS Operating Systems Review10.1145/2883591.288360249:2(51-56)Online publication date: 20-Jan-2016
https://dl.acm.org/doi/10.1145/2883591.2883602
Orchard DYoshida NBodik RMajumdar R(2016)Effects as sessions, sessions as effectsProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837634(568-581)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837634
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents