Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Treaps


view this post on Zulip Email Gateway (Aug 22 2022 at 16:43):

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

there is a second new AFP entry today on an interesting data structure: treaps.

Enjoy,
René

Treaps
by Manuel Eberl, Max Haslbeck and Tobias Nipkow

A Treap is a binary tree whose nodes contain pairs consisting of some payload and an associated priority. It must have the search-tree property w.r.t. the payloads and the heap property w.r.t. the priorities. Treaps are an interesting data structure that is related to binary search trees (BSTs) in the following way: if one forgets all the priorities of a treap, the resulting BST is exactly the same as if one had inserted the elements into an empty BST in order of ascending priority. This means that a treap behaves like a BST where we can pretend the elements were inserted in a different order from the one in which they were actually inserted.

In particular, by choosing these priorities at random upon insertion of an element, we can pretend that we inserted the elements in random order, so that the shape of the resulting tree is that of a random BST no matter in what order we insert the elements. This is the main result of this formalisation.

view this post on Zulip Email Gateway (Aug 22 2022 at 16:43):

From: Lars Hupel <hupel@in.tum.de>

there is a second new AFP entry today on an interesting data structure:
treaps.

It also appears to be AFP entry #400!

Cheers,
Lars


Last updated: Mar 28 2024 at 12:29 UTC