Provably Correct Key-Value Maps in Agda - Leveraging Membership to Reach Correctness
Ladda ner
Publicerad
Författare
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
This thesis describes the interface and implementation of a provably correct finite
map in the Agda programming language. Finite maps are fundamental data structures
in computer science, and existing finite maps in Agda can be improved in
terms of correctness and some implementation details. We present an extension of
‘A Theory of Finite Maps’ (Collins & Syme, 1995) and an Agda formalisation of that
extended theory. The formalisation is designed to be structure agnostic, allowing
for many underlying implementations, and its flexibility is demonstrated through a
proof-of-concept simply typed lambda calculus interpreter.
The core of the formalisation is implemented and proven for AVL trees, extending the
Agda standard library with additional proofs and operations. Among these are laws
defining the behaviour of delete and unionWith as well as an alternative unionWith
implementation. The implementation is also differentiated from the standard library
by using erasure to remove, among other things, ordering proofs from the tree data
type and operations. The performance of our implementation is compared to the
standard library and the results show no meaningful performance gains for our
implementation.
Finally, we discuss the inclusion of correct-by-construction membership properties
in the tree structure itself. Such properties have not been introduced in our implementation.
This is due to the constant need to update each proof on every operation
on the collection, since any operation that modifies the structure of the tree may
cause a proof to become irrelevant for the new map.
Beskrivning
Ämne/nyckelord
Agda, AVL Trees, Collections, Finite maps