Formalizing Open Induction, The Tree Theorem, and Simple Termination

Proving termination is an important part of program verification. To facilitate reusable and abstract results, instead of a concrete programming language, termination is usually considered relative to a mathematical model of computation, for this project, term rewriting. Nowadays, there are many tools that can prove termination of term rewriting automatically. However, these tools may contain bugs and hence the need for an independent and reliable certification of their results arises. This is done by so called certifiers, tools that can automatically check, whether a proof that was generated by a termination tool, is correct. The high reliability of such certifiers comes from the fact that they are built upon formalizations of the underlying theory using proof assistants, like Isabelle/HOL. One such formalization is IsaFoR, an Isabelle Formalization of Rewriting. Naturally, formalizations in Isabelle can only build upon facts that have already been formalized in Isabelle before. Hence, one aim of this project is to widen the body of mathematics that is available to Isabelle users. The concrete new contributions will be a formalization of (possibly infinite) trees and upon that a proof of the famous Tree Theorem by Kruskal in Isabelle. The Tree Theorem, in turn, will allow to formalize the connection between simple termination and termination: every simply terminating term rewrite system is also terminating. This result will then be used to incorporate the Knuth-Bendix order (and possibly other simplification orders) into IsaFoR, thereby increasing the number of termination proofs that can be certified automatically. However, we are not only interested in the Tree Theorem with respect to simple termination, but also in its computational content. To this end, we will formalize the principle of open induction in Isabelle, in order to be able to give an alternative and more constructive proof of the Tree Theorem. Furthermore, we will search for other theorems, where open induction could facilitate a formalized proof. Finally, open induction can also be used to define total functions. Since proof assistants based on higher-order logic (as Isabelle) rely on all defined functions being total, we will use open induction to extend Isabelle’s definitional function package by open inductively defined functions.

project start: November 2011
project end: November 2014

  • Christian Sternagel
FWF Erwin Schrödinger Fellowship Abroad project number



Nach oben scrollen