Document Open Access Logo

Amortized Analysis via Coinduction (Early Ideas)

Authors Harrison Grodin , Robert Harper

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2023.23.pdf
  • Filesize: 0.67 MB
  • 6 pages

Document Identifiers

Author Details

Harrison Grodin
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Robert Harper
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the United States Air Force Office of Scientific Research under grant number FA9550-21-0009 (Tristan Nguyen, program manager) and the National Science Foundation under grant number CCF-1901381. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR or NSF.

Acknowledgements

We are grateful to Yue Niu, Max New, and David Spivak for insightful discussions about this research.

Cite AsGet BibTex

Harrison Grodin and Robert Harper. Amortized Analysis via Coinduction (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 23:1-23:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.23

Abstract

Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented inductively, in terms of finite sequences of operations. We give an alternative coinductive formulation and prove that it is equivalent to the standard inductive definition. We describe a classic amortized data structure, the batched queue, and outline a coinductive proof of its amortized efficiency in calf, a dependent type theory for cost analysis.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
  • Software and its engineering → Functional languages
  • Theory of computation → Program reasoning
  • Theory of computation → Categorical semantics
Keywords
  • amortized analysis
  • coinduction
  • data structure
  • mechanized proof

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming infinite structures by observations. ACM SIGPLAN Notices, 48(1):27-38, January 2013. URL: https://doi.org/10.1145/2480359.2429075.
  2. Adriana Balan and Alexander Kurz. On Coalgebras over Algebras. Electronic Notes in Theoretical Computer Science, 264(2):47-62, August 2010. URL: https://doi.org/10.1016/j.entcs.2010.07.013.
  3. F. Warren Burton. An efficient functional implementation of FIFO queues. Information Processing Letters, 14(5):205-206, July 1982. URL: https://doi.org/10.1016/0020-0190(82)90015-1.
  4. William R. Cook. Object-oriented programming versus abstract data types. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, Lecture Notes in Computer Science, pages 151-178, Berlin, Heidelberg, 1991. Springer. URL: https://doi.org/10.1007/BFb0019443.
  5. William R. Cook. On understanding data abstraction, revisited. In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '09, pages 557-572, New York, NY, USA, October 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1640089.1640133.
  6. Joseph W. Cutler, Daniel R. Licata, and Norman Danner. Denotational recurrence extraction for amortized analysis. Proceedings of the ACM on Programming Languages, 4(ICFP):97:1-97:29, August 2020. URL: https://doi.org/10.1145/3408979.
  7. Nils Anders Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. ACM SIGPLAN Notices, 43(1):133-144, January 2008. URL: https://doi.org/10.1145/1328897.1328457.
  8. Norman Danner, Daniel R. Licata, and Ramyaa Ramyaa. Denotational cost semantics for functional languages with inductive types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 140-151, New York, NY, USA, August 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2784731.2784749.
  9. Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. Enriching an Effect Calculus with Linear Types. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, Lecture Notes in Computer Science, pages 240-254, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-04027-6_19.
  10. David Gries. The Science of Programming. Springer New York, April 1989. Google Scholar
  11. Robert Hood and Robert Melville. Real-time queue operations in pure LISP. Information Processing Letters, 13(2):50-54, November 1981. URL: https://doi.org/10.1016/0020-0190(81)90030-2.
  12. Bart Jacobs. Mongruences and cofree coalgebras. In V. S. Alagar and Maurice Nivat, editors, Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, pages 245-260, Berlin, Heidelberg, 1995. Springer. URL: https://doi.org/10.1007/3-540-60043-4_57.
  13. Bart Jacobs. Objects And Classes, Co-Algebraically. In Burkhard Freitag, Cliff B. Jones, Christian Lengauer, and Hans-Jörg Schek, editors, Object Orientation with Parallelism and Persistence, The Kluwer International Series in Engineering and Computer Science, pages 83-103. Springer US, Boston, MA, 1996. URL: https://doi.org/10.1007/978-1-4613-1437-0_5.
  14. Shin-ya Katsumata, Exequiel Rivas, and Tarmo Uustalu. Interaction Laws of Monads and Comonads. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 604-618, New York, NY, USA, July 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394808.
  15. G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. Recurrence extraction for functional programs through call-by-push-value. Proceedings of the ACM on Programming Languages, 4(POPL):15:1-15:31, December 2019. URL: https://doi.org/10.1145/3371083.
  16. Gregory Maxwell Kelly. Basic Concepts of Enriched Category Theory. CUP Archive, February 1982. Google Scholar
  17. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis. Springer Netherlands, Dordrecht, 2003. URL: http://link.springer.com/10.1007/978-94-007-0954-6, URL: https://doi.org/10.1007/978-94-007-0954-6.
  18. Yue Niu, Jon Sterling, Harrison Grodin, and Robert Harper. calf: A Cost-Aware Logical Framework. URL: https://github.com/jonsterling/agda-calf.
  19. Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. A cost-aware logical framework. Proceedings of the ACM on Programming Languages, 6(POPL):9:1-9:31, January 2022. URL: https://doi.org/10.1145/3498670.
  20. Chris Okasaki. Purely Functional Data Structures. PhD thesis, Carnegie Mellon University, 1996. URL: https://doi.org/10.1007/3-540-61628-4_5.
  21. Gordon Plotkin and John Power. Tensors of Comodels and Models for Operational Semantics. Electronic Notes in Theoretical Computer Science, 218:295-311, October 2008. URL: https://doi.org/10.1016/j.entcs.2008.10.018.
  22. John Power and Olha Shkaravska. From Comodels to Coalgebras: State and Arrays. Electronic Notes in Theoretical Computer Science, 106:297-314, December 2004. URL: https://doi.org/10.1016/j.entcs.2004.02.041.
  23. Robert Endre Tarjan. Amortized Computational Complexity. SIAM Journal on Algebraic Discrete Methods, 6(2):306-318, April 1985. URL: https://doi.org/10.1137/0606031.
  24. D. Turi and G. Plotkin. Towards a mathematical operational semantics. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 280-291, June 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact