More Web Proxy on the site http://driver.im/

research-article

Analysing the complexity of functional programs: higher-order meets first-order

Authors:

Martin Avanzini,

Georg MoserAuthors Info & Claims

ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

Pages 152 - 164

https://doi.org/10.1145/2784731.2784753

Published: 29 August 2015 Publication History

Abstract

We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalised versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Further, we describe suitable strategies for the application of the studied transformations and provide ample experimental data for assessing the viability of our method.

References

[1]

B. Accattoli and U. Dal Lago. Beta Reduction is Invariant, Indeed. In Proc. of 23rd CSL, pages 8:1–8:10. ACM, 2014.

Digital Library

[2]

B. Accattoli and C. Sacerdoti Coen. On the Usefulness of Constructors. In Proc. of 30th LICS. IEEE, 2015. To appear.

[3]

E. Albert, S. Genaim, and A. N. Masud. On the Inference of Resource Usage Upper and Lower Bounds. TOCL, 14(3):22(1–35), 2013.

Digital Library

[4]

T. Arts and J. Giesl. Termination of Term Rewriting using Dependency Pairs. TCS, 236(1–2):133–178, 2000.

Digital Library

[5]

D. Aspinall, L. Beringer, M. Hofmann, H.-W. Loidl, and A. Momigliano. A Program Logic for Resources. TCS, 389(3):411–445, 2007.

Digital Library

[6]

M. Avanzini and G. Moser. Closing the Gap Between Runtime Complexity and Polytime Computability. In Proc. of 21st RTA, volume 6 of LIPIcs, pages 33–48, 2010.

[7]

M. Avanzini and G. Moser. Polynomial Path Orders. LMCS, 9(4), 2013.

[8]

M. Avanzini and G. Moser. Tyrolean Complexity Tool: Features and Usage. In Proc. of 24th RTA, volume 21 of LIPIcs, pages 71–80, 2013.

[9]

M. Avanzini and G. Moser. A Combination Framework for Complexity. IC, 2015. To appear.

[10]

M. Avanzini, U. Dal Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version). CoRR, cs/CC/1506.05043, 2015. Available at http://www.arxiv. org/abs/1506.05043.

Digital Library

[11]

F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. ISBN 978-0-521-77920-3.

[12]

P. Baillot and U. Dal Lago. Higher-Order Interpretations and Program Complexity. In Proc. of 26th CSL, volume 16 of LIPIcs, pages 62–76, 2012.

[13]

P. Baillot and K. Terui. Light types for Polynomial Time Computation in Lambda Calculus. IC, 207(1):41–62, 2009.

Digital Library

[14]

R. Benzinger. Automated Higher-order Complexity Analysis. TCS, 318(1-2):79–103, 2004.

Digital Library

[15]

R. Bird. Introduction to Functional Programming using Haskell, Second Edition. Prentice Hall, 1998. ISBN 978-0-134-84346-9.

Digital Library

[16]

G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with Polynomial Interpretation Termination Proof. JFP, 11(1):33–53, 2001.

Digital Library

[17]

G. Bonfante, J.-Y. Marion, and R. Péchoux. Quasi-interpretation Synthesis by Decomposition and an Application to Higher-order Programs. In Proc. of 4th ICTAC, volume 4711 of LNCS, pages 410– 424, 2007.

Digital Library

[18]

U. Dal Lago and M. Gaboardi. Linear Dependent Types and Relative Completeness. LMCS, 8(4), 2012.

[19]

U. Dal Lago and S. Martini. On Constructor Rewrite Systems and the Lambda Calculus. LMCS, 8(3):1–27, 2012.

[20]

U. Dal Lago and B. Petit. The Geometry of Types. In Proc. of 40th POPL, pages 167–178. ACM, 2013.

Digital Library

[21]

N. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proc. of 35th POPL, pages 133–144. ACM, 2008.

Digital Library

[22]

O. Danvy and L. R. Nielsen. Defunctionalization at Work. In Proc. of 3rd PPDP, pages 162–174. ACM, 2001.

Digital Library

[23]

G. Feuillade, T. Genet, and V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. JAR, 33(3-4):341–383, 2004.

Digital Library

[24]

J. Giesl, R. Thiemann, and P. Schneider-Kamp. Proving and Disproving Termination of Higher-Order Functions. In Proc. of 5th FROCOS, volume 3717 of LNCS, pages 216–231, 2005.

Digital Library

[25]

J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated Termination Proofs for Haskell by Term Rewriting. TOPLAS, 33(2):7:1–7:39, 2011.

Digital Library

[26]

J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Proving Termination of Programs Automatically with AProVE. In Proc. of 7th IJCAR, volume 8562 of LNCS, pages 184–191, 2014.

[27]

G. Gomez and Y. Liu. Automatic Time-bound Analysis for a Higherorder Language. In Proc. of 9th PEPM, pages 75–86. ACM, 2002.

Digital Library

[28]

B. Gramlich. Abstract Relations between Restricted Termination and Confluence Properties of Rewrite Systems. FI, 24:3–23, 1995.

Digital Library

[29]

R. Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2012. ISBN 978-1-107-02957-6.

Digital Library

[30]

N. Hirokawa and G. Moser. Automated Complexity Analysis Based on the Dependency Pair Method. In Proc. of 4th IJCAR, volume 5195 of LNAI, pages 364–380, 2008.

Digital Library

[31]

N. Hirokawa and G. Moser. Complexity, Graphs, and the Dependency Pair Method. In Proc. of 15th LPAR, volume 5330 of LNCS, pages 652–666, 2008.

Digital Library

[32]

N. Hirokawa, A. Middeldorp, and H. Zankl. Uncurrying for Termination and Complexity. JAR, 50(3):279–315, 2013.

Digital Library

[33]

N. D. Jones. Flow Analysis of Lazy Higher-order Functional Programs. TCS, 375(1-3):120–136, 2007.

Digital Library

[34]

N. D. Jones and N. Bohr. Call-by-Value Termination in the Untyped lambda-Calculus. LMCS, 4(1), 2008.

[35]

S. Jost, K. Hammond, H.-W. Loidl, and M.Hofmann. Static Determination of Quantitative Resource Usage for Higher-order Programs. In Proc. of 37th POPL, pages 223–236. ACM, 2010.

Digital Library

[36]

J. Kochems and L. Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In Proc. of 22nd RTA, volume 10 of LIPIcs, pages 187–202, 2011.

[37]

M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp. Tyrolean Termination Tool 2. In Proc. of 20th RTA, volume 5595 of LNCS, pages 295–304, 2009.

Digital Library

[38]

J.-Y. Marion. Analysing the Implicit Complexity of Programs. IC, 183: 2–18, 2003.

Digital Library

[39]

J. Midtgaard. Control-flow Analysis of Functional Programs. ACM Comput. Surv., 44(3):10, 2012.

Digital Library

[40]

G. Moser. Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. CoRR, cs.LO/0907.5527, 2009. Habilitation Thesis.

[41]

F. Nielson, H. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 2005. ISBN 978-3-540-65410-0.

Digital Library

[42]

L. Noschinski, F. Emmes, and J. Giesl. A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. In Proc. of 23rd CADE, LNAI, pages 422–438. Springer, 2011.

Digital Library

[43]

C. Okasaki. Functional Pearl: Even Higher-Order Functions for Parsing. JFP, 8(2):195–199, 1998.

Digital Library

[44]

S. E. Panitz and M. Schmidt-Schauß. TEA: Automatically Proving Termination of Programs in a Non-Strict Higher-Order Functional Language. In Proc. of 4th SAS, pages 345–360, 1997.

Digital Library

[45]

B. C. Pierce. Types and programming languages. MIT Press, 2002. ISBN 978-0-262-16209-8.

Digital Library

[46]

G. D. Plotkin. LCF Considered as a Programming Language. TCS, 5 (3):223–255, 1977.

[47]

F. Rabhi and G. Lapalme. Algorithms: A Functional Programming Approach. Addison-Wesley, 1999. ISBN 978-0-201-59604-5.

Digital Library

[48]

J. C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998.

Digital Library

[49]

D. Sands. Complexity Analysis for a Lazy Higher-Order Language. In Proc. of 3rd ESOP, volume 432 of LNCS, pages 361–376, 1990.

Digital Library

[50]

M. Sinn, F. Zuleger, and H. Veith. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Proc. of 26th CAV, volume 8559 of LNCS, pages 745–761, 2014.

Digital Library

[51]

C. Sternagel and R. Thiemann. Generalized and Formalized Uncurrying. In Proc. of 8th FROCOS, volume 6989 of LNCS, pages 243–258, 2011.

Digital Library

[52]

TeReSe. Term Rewriting Systems, volume 55. Cambridge University Press, 2003. ISBN 978-0-521-39115-3.

[53]

P. B. Vasconcelos and K. Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In Revised Papers of 15th Workshop on IFL, pages 86–101, 2003.

Digital Library

[54]

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. The Worst Case Execution Time Problem - Overview of Methods and Survey of Tools. TECS, pages 1–53, 2008.

Digital Library

[55]

H. Zankl and M. Korp. Modular Complexity Analysis for Term Rewriting. LMCS, 10(1:19):1–33, 2014.

Cited By

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
Guo LKop C(2024)Higher-Order LCTRSs and Their TerminationProgramming Languages and Systems10.1007/978-3-031-57267-8_13(331-357)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_13
Colledan ADal Lago U(2024)Circuit Width Estimation via Effect Typing and Linear DependencyProgramming Languages and Systems10.1007/978-3-031-57267-8_1(3-30)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_1
Show More Cited By

Index Terms

Analysing the complexity of functional programs: higher-order meets first-order
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Analysing the complexity of functional programs: higher-order meets first-order
ICFP '15

We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalised versions of them, and feeding the result to existing tools for the complexity analysis of first-order ...
Relating Higher-order and First-order Rewriting

We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory. In particular, we obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting ...
Narrowing for First Order Functional Logic Programs with Call-Time Choice Semantics
Applications of Declarative Programming and Knowledge Management

In a recent work we have proposed <em>let</em> -rewriting, a simple one-step relation close to ordinary term rewriting but able, via local bindings, to express sharing of computed values. In this way, <em>let</em> -rewriting reflects the call-time ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

August 2015

436 pages

ISBN:9781450336697

DOI:10.1145/2784731

General Chair:
Kathleen Fisher
Tufts University, USA
,
Program Chair:
John Reppy
University of Chicago, USA

ACM SIGPLAN Notices Volume 50, Issue 9
ICFP '15
September 2015
436 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2858949
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 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 the author(s) 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

FWF
ANR

Conference

ICFP'15

Sponsor:

SIGPLAN

ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming

August 31 - September 2, 2015

BC, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

40
Total Citations
View Citations
333
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)3

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
Guo LKop C(2024)Higher-Order LCTRSs and Their TerminationProgramming Languages and Systems10.1007/978-3-031-57267-8_13(331-357)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_13
Colledan ADal Lago U(2024)Circuit Width Estimation via Effect Typing and Linear DependencyProgramming Languages and Systems10.1007/978-3-031-57267-8_1(3-30)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_1
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
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
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
Fan GChen TYin BChen LWang TWang J(2021)Static Bound Analysis of Dynamically Allocated Resources for C Programs2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE52982.2021.00048(390-400)Online publication date: Oct-2021
https://doi.org/10.1109/ISSRE52982.2021.00048
Das ABalzer SHoffmann JPfenning FSanturkar I(2021)Resource-Aware Session Types for Digital Contracts2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00004(1-16)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00004
Hofmann MLeutgeb LObwaller DMoser GZuleger F(2021)Type-based analysis of logarithmic amortised complexityMathematical Structures in Computer Science10.1017/S096012952100023232:6(794-826)Online publication date: 19-Oct-2021
https://doi.org/10.1017/S0960129521000232
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.

Figures

Tables

Media

View Table of Conten