License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2023.23
URN: urn:nbn:de:0030-drops-188201
URL: https://drops.dagstuhl.de/opus/volltexte/2023/18820/
Go to the corresponding LIPIcs Volume Portal


Grodin, Harrison ; Harper, Robert

Amortized Analysis via Coinduction (Early Ideas)

pdf-format:
LIPIcs-CALCO-2023-23.pdf (0.7 MB)


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.

BibTeX - Entry

@InProceedings{grodin_et_al:LIPIcs.CALCO.2023.23,
  author =	{Grodin, Harrison and Harper, Robert},
  title =	{{Amortized Analysis via Coinduction}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{23:1--23:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18820},
  URN =		{urn:nbn:de:0030-drops-188201},
  doi =		{10.4230/LIPIcs.CALCO.2023.23},
  annote =	{Keywords: amortized analysis, coinduction, data structure, mechanized proof}
}

Keywords: amortized analysis, coinduction, data structure, mechanized proof
Collection: 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Issue Date: 2023
Date of publication: 02.09.2023
Supplementary Material: Software (Source Code): https://github.com/jonsterling/agda-calf archived at: https://archive.softwareheritage.org/swh:1:dir:7750187b111d75acca1980e9abffae2d63ffbe69


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI