TY - GEN

T1 - A machine-checked proof of the average-case complexity of quicksort in coq

AU - Van Der Weegen, Eelis

AU - McKinna, James

PY - 2009

Y1 - 2009

N2 - As a case-study in machine-checked reasoning about the complexity of algorithms in type theory, we describe a proof of the average-case complexity of Quicksort in Coq. The proof attempts to follow a textbook development, at the heart of which lies a technical lemma about the behaviour of the algorithm for which the original proof only gives an intuitive justification. We introduce a general framework for algorithmic complexity in type theory, combining some existing and novel techniques: algorithms are given a shallow embedding as monadically expressed functional programs; we introduce a variety of operation-counting monads to capture worst- and average-case complexity of deterministic and nondeterministic programs, including the generalization to count in an arbitrary monoid; and we give a small theory of expectation for such non-deterministic computations, featuring both general map-fusion like results, and specific counting arguments for computing bounds. Our formalization of the average-case complexity of Quicksort includes a fully formal treatment of the 'tricky' textbook lemma, exploiting the generality of our monadic framework to support a key step in the proof, where the expected comparison count is translated into the expected length of a recorded list of all comparisons.

AB - As a case-study in machine-checked reasoning about the complexity of algorithms in type theory, we describe a proof of the average-case complexity of Quicksort in Coq. The proof attempts to follow a textbook development, at the heart of which lies a technical lemma about the behaviour of the algorithm for which the original proof only gives an intuitive justification. We introduce a general framework for algorithmic complexity in type theory, combining some existing and novel techniques: algorithms are given a shallow embedding as monadically expressed functional programs; we introduce a variety of operation-counting monads to capture worst- and average-case complexity of deterministic and nondeterministic programs, including the generalization to count in an arbitrary monoid; and we give a small theory of expectation for such non-deterministic computations, featuring both general map-fusion like results, and specific counting arguments for computing bounds. Our formalization of the average-case complexity of Quicksort includes a fully formal treatment of the 'tricky' textbook lemma, exploiting the generality of our monadic framework to support a key step in the proof, where the expected comparison count is translated into the expected length of a recorded list of all comparisons.

UR - http://www.scopus.com/inward/record.url?scp=68749097397&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02444-3_16

DO - 10.1007/978-3-642-02444-3_16

M3 - Conference contribution

AN - SCOPUS:68749097397

SN - 9783642024436

T3 - Lecture Notes in Computer Science

SP - 256

EP - 271

BT - Types for Proofs and Programs. TYPES 2008

PB - Springer

T2 - International Conference on Types for Proofs and Programs 2008

Y2 - 26 March 2008 through 29 March 2008

ER -