Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: "A Combinator Library for Pref...


view this post on Zulip Email Gateway (Apr 19 2022 at 08:12):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce two new AFP entries, both written by Emin Karayel.

A Combinator Library for Prefix-Free Codes [1]

This entry contains a set of binary encodings for primitive data types, such as
natural numbers, integers, floating-point numbers as well as combinators to
construct encodings for products, lists, sets or functions of/between such
types. For natural numbers and integers, the entry contains various encodings,
such as Elias-Gamma-Codes and exponential Golomb Codes, which are efficient
variable-length codes in use by current compression formats. A use-case for this
library is measuring the persisted size of a complex data structure without
having to hand-craft a dedicated encoding for it, independent of Isabelle's
internal representation.

Formalization of Randomized Approximation Algorithms for Frequency Moments [2]

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. But, also higher-order frequency
moments that provide information about the skew of the data stream. (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.) This entry formalizes three
randomized algorithms for the approximation of F_0, F_2 and F_k for k ≥ 3 based
on [3, 4] and verifies their expected accuracy, success probability and space
usage.

Enjoy,
René

1: https://www.isa-afp.org/entries/Prefix_Free_Code_Combinators.html
2: https://www.isa-afp.org/entries/Frequency_Moments.html
3: https://doi.org/10.1006/jcss.1997.1545
4: https://doi.org/10.1007/3-540-45726-7_1


Last updated: Jul 15 2022 at 23:21 UTC