Proving Divide and Conquer Complexities in Isabelle/HOL

摘要

The Akra-Bazzi method (Akra and Bazzi in Comput Optim Appl 10(2): 195210, 1998. doi: 10.1023A: 1018373005182), a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide and Conquer algorithms. This work describes a formalisation of the Akra-Bazzi method (as generalised by Leighton in Notes on better Master theorems for divide-and-conquer recurrences, 1996. http: courses. csail. mit. edu 6.046 spring04 handouts akrabazzi. pdf) in the interactive theorem prover Isabelle HOL and the derivation of a generalised version of the Master Theorem from it. We also provide some automated proof methods that facilitate the application of this Master Theorem and allow mostly automatic verification of T-bounds for these Divide and Conquer recurrences. To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.