Deriving Sorting Algorithms

TL;DR

This paper introduces a novel derivation method for three classic sorting algorithms using functional programming, combining algebraic transformations, inductive-coinductive reasoning, and structural invariants.

Contribution

It presents a new derivation approach that simplifies sorting algorithms from specifications through program transformations and algebraic reasoning.

Findings

Derived three well-known sorting algorithms functionally

Unified inductive and coinductive reasoning in derivations

Enhanced correctness proofs with structural invariants

Abstract

This paper proposes new derivations of three well-known sorting algorithms, in their functional formulation. The approach we use is based on three main ingredients: first, the algorithms are derived from a simpler algorithm, i.e. the specification is already a solution to the problem (in this sense our derivations are program transformations). Secondly, a mixture of inductive and coinductive arguments are used in a uniform, algebraic style in our reasoning. Finally, the approach uses structural invariants so as to strengthen the equational reasoning with logical arguments that cannot be captured in the algebraic framework.