Wednesday 13 July 2022, 10:30 PM, room 3U42: Stability of mergesort, almost for free, Kazuhiko Sakaguchi (University of Tsukuba).

Effective optimization techniques for an algorithm may depend on its usage and the evaluation strategy in functional programming. For example, while a tail-recursive mergesort algorithm avoids using up stack space and is efficient in call-by-value evaluation, a non-tail-recursive mergesort algorithm can compute the output incrementally in call-by-need evaluation. We show that a non-tail-recursive mergesort algorithm in call-by-need evaluation performs only O(n + k log k) comparisons to compute the least (or greatest) k items of a list of length n. To prove the correctness of several such implementations of mergesort, we present a novel characterization of stable sort functions using traces—binary trees reflecting the divide-and-conquer structure of mergesort—and relational parametricity. Thanks to our characterization and the parametricity translation, we deduced some correctness results, including stability, of various implementations of mergesort for lists, including highly optimized ones, in the Coq proof assistant.