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.ITP.2022.21
URN: urn:nbn:de:0030-drops-167308
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16730/
Go to the corresponding LIPIcs Volume Portal

Karayel, Emin

Formalization of Randomized Approximation Algorithms for Frequency Moments

pdf-format:
LIPIcs-ITP-2022-21.pdf (0.9 MB)

Abstract

In 1999 Alon et al. introduced the still active research topic of approximating the frequency moments of a data stream using randomized algorithms with minimal space usage. This includes the problem of estimating the cardinality of the stream elements - the zeroth frequency moment. Higher-order frequency moments provide information about the skew of the data stream which is, for example, critical information for parallel processing. (The k-th frequency moment of a data stream is the sum of the k-th powers of the occurrence counts of each element in the stream.) They introduce both lower bounds and upper bounds on the space complexity of the problems, which were later improved by newer publications. The algorithms have guaranteed success probabilities and accuracies without making any assumptions on the input distribution. They are an interesting use case for formal verification because their correctness proofs require a large body of deep results from algebra, analysis and probability theory. This work reports on the formal verification of three algorithms for the approximation of F₀, F₂ and F_k for k ≥ 3. The results include the identification of significantly simpler algorithms with the same runtime and space complexities as the previously known ones as well as the development of several reusable components, such as a formalization of universal hash families, amplification methods for randomized algorithms, a model for one-pass data stream algorithms or a generic flexible encoding library for the verification of space complexities.

BibTeX - Entry

@InProceedings{karayel:LIPIcs.ITP.2022.21,
  author =	{Karayel, Emin},
  title =	{{Formalization of Randomized Approximation Algorithms for Frequency Moments}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16730},
  URN =		{urn:nbn:de:0030-drops-167308},
  doi =		{10.4230/LIPIcs.ITP.2022.21},
  annote =	{Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments}
}

Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software (Isabelle/HOL Formalization): https://isa-afp.org/entries/Frequency_Moments.html

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