research-article

Lightweight semiformal time complexity analysis for purely functional data structures

Author:

Nils Anders DanielssonAuthors Info & Claims

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 133 - 144

https://doi.org/10.1145/1328438.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

Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Xia LIsrael LKramarz MColtharp NClaessen KWeirich SLi Y(2024)Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy ProgramsProceedings of the ACM on Programming Languages10.1145/36746268:ICFP(30-63)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674626
Pham LSaad FHoffmann J(2024)Robust Resource Bounds with Static Analysis and Bayesian InferenceProceedings of the ACM on Programming Languages10.1145/36563808:PLDI(76-101)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656380
Show More Cited By

Recommendations

Lightweight semiformal time complexity analysis for purely functional data structures
POPL '08

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 Conferences

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

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

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL08

Sponsor:

POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 7 - 12, 2008

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

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 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Xia LIsrael LKramarz MColtharp NClaessen KWeirich SLi Y(2024)Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy ProgramsProceedings of the ACM on Programming Languages10.1145/36746268:ICFP(30-63)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674626
Pham LSaad FHoffmann J(2024)Robust Resource Bounds with Static Analysis and Bayesian InferenceProceedings of the ACM on Programming Languages10.1145/36563808:PLDI(76-101)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656380
Atkey R(2024)Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages10.1145/36329188:POPL(2288-2317)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632918
Pottier FGuéneau AJourdan JMével G(2024)Thunks and Debits in Separation Logic with Time CreditsProceedings of the ACM on Programming Languages10.1145/36328928:POPL(1482-1508)Online publication date: 5-Jan-2024
https://doi.org/10.1145/3632892
Niu YSterling JGrodin HHarper R(2022)A cost-aware logical frameworkProceedings of the ACM on Programming Languages10.1145/34986706:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498670
DANNER NLICATA D(2022)Denotational semantics as a foundation for cost recurrence extraction for functional languagesJournal of Functional Programming10.1017/S095679682200003X32Online publication date: 5-Jul-2022
https://doi.org/10.1017/S095679682200003X
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: 19-Aug-2021
https://dl.acm.org/doi/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: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473585
Kahn DHoffmann J(2021)Automatic amortized resource analysis with the Quantum physicist’s methodProceedings of the ACM on Programming Languages10.1145/34735815:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473581
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 Table of Contents