Reseña: “Formalizing bounded increase”

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre terminación titulado Formalizing bounded increase.

Su autor es René Thiemann (de la Univ. de Innsbruck, Austria) y lo presentará en la ITP 2013 (4th International Conference on Interactive Theorem Proving).

Su resumen es

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.