Saturating Sorting without Sorts

TL;DR

This work addresses the automated verification of recursive sorting algorithms implemented over parameterized lists in first-order logic. It introduces a saturation-based proof engine that integrates computation induction directly into deduction, enabling automatic proofs of sortedness and permutation equivalence for sorts like Quicksort and Mergesort without user-provided invariants. The approach leverages a parameterized list theory, a first-order formalization of permutation via filter-based multiset reasoning, and compositional proofs built from inductive lemmas derived during proof search. Empirical evaluation on Vampire demonstrates automated verification of key properties across several sorting algorithms, highlighting substantial reductions in manual proof effort and demonstrating the feasibility of automated inductive reasoning in a first-order setting.

Abstract

We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted first-order logic and integrate sortedness/permutation properties within our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories, such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and hence concrete sorts. We formalize the permutation property of lists in first-order logic so that we automatically prove verification conditions of such algorithms purely by superpositon-based first-order reasoning. Doing so, we adjust recent efforts for automating inducion in saturation. We advocate a compositional approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. Our work turns saturation-based first-order theorem proving into an automated verification engine by (i) guiding automated inductive reasoning with manual proof splits and (ii) fully automating inductive reasoning in saturation. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort.

Figures (5)

• Figure 1: Recursive algorithm of Quicksort, using the recursive function definitions append, $\texttt{filter}_<$ and $\texttt{filter}_{\geq}$ over lists of sort $a$.
• Figure 2: Recursive divide-and-conquer approach.
• Figure 3: Functions $filter_Q$ filtering elements of a list, by using a predicate $Q(y,x)$ over list elements $x,y$.
• Figure 4: Recursive Mergesort over lists of sort $a$.
• Figure 5: Recursive algorithm of Insertionsort.

Theorems & Definitions (1)

• Example 1: Compositional reasoning over sortedness in saturation