Proving Divide and Conquer Complexities in Isabelle/HOL
by Manuel Eberl
In: Journal of Automated Reasoning (2016)
DOI:
10.1007/s10817-016-9378-0Abstract:
The Akra–Bazzi method, a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide & Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton) 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 Θ-bounds for Divide & Conquer recurrences.
To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.
Download preprint PDF (381 KiB)
BibTeX:
@Article{eberl17jar,
author="Manuel Eberl",
title="Proving Divide and Conquer Complexities in {I}sabelle/{HOL}",
journal="Journal of Automated Reasoning",
year="2017",
month="Apr",
day="01",
volume="58",
number="4",
pages="483--508",
doi="10.1007/s10817-016-9378-0",
issn="1573-0670"
}