Abstract

Bounded increase is a termination technique where it is tried to find an argument x of a recursive function that is increased repeatedly until it reaches a bound b, which might be ensured by a condition x < b. Since the predicates like < may be arbitrary user-defined recursive functions, an induction calculus is utilized to prove conditional constraints.

In this paper, we present a full formalization of bounded increase in the theorem prover Isabelle/HOL. It fills one large gap in the pen-and-paper proof, and it includes generalized inference rules for the induction calculus as well as variants of the Babylonian algorithm to compute square roots. These algorithms were required to write executable functions which can certify untrusted termination proofs from termination tools that make use of bounded increase. And indeed, the resulting certifier was already useful: it detected an implementation error that remained undetected since 2007.

BibTeX

@inproceedings{RT-ITP13,
  author      = "Ren{\'e} Thiemann",
  title       = "Formalizing Bounded Increase",
  booktitle   = "Proceedings of the 4th International Conference on
                 Interactive Theorem Proving",
  editor      = "Sandrine Blazy and Christine Paulin-Mohring and
                 David Pichardie",
  series      = "Lecture Notes in Computer Science",
  volume      = 7998,
  pages       = "245--260",
  publisher   = "Springer-Verlag",
  year        = 2013,
  doi         = "10.1007/978-3-642-39634-2_19"
}