Proving Divide and Conquer Complexities in Isabelle/HOL
Proving Divide and Conquer Complexities in Isabelle/HOL
复制标题
DOI：
10.1007/s10817-016-9378-0
复制
发表时间：
2017-04-01
期刊：
影响因子：
--
通讯作者：
Eberl, Manuel
中科院分区：
文献类型：
--
作者：
Eberl, Manuel
《阿克拉-巴齐方法》(《计算机优化应用》10(2)：195210,1998年)。DOI：10.1023A：1018373005182)，是著名的主定理的推广，是分析分而治之算法复杂性的有用工具。这项工作描述了Akra-Bazzi方法的形式化(由Leighton在1996年关于分而治之递归的更好的大师定理的注释中概括)。Http：课程。CSAIL.麻省理工学院。EDU 6.046/04春季讲义阿克拉巴齐。Pdf)在交互式定理证明器Isabelle HOL中，并由此推导出主定理的一个推广版本。我们还提供了一些自动证明方法，方便了这个主定理的应用，并允许大多数情况下自动验证这些除法和征服递归的T-界。据我们所知，这是用于分析这种递归的第一个定理的形式化。
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.