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.

The main achievement of this project is a mechanized proof of the famous (at least among mathematicians) tree theorem due to Kruskal. Here, the word tree denotes a mathematical structure that is for example used to model arbitrary mathematical expressions and the syntax of arbitrary programming languages. Now the tree theorem states that for every infinite sequence of treesas would for example result from a looping computer programits elements steadily become more complex. This fact, in turn, can be employed to rule out such loops entirely for a certain class of programs, thereby proving termination. While the tree theorem was first proved in 1960 by Kruskal, we present the first mechanized proof. By which we mean that the proof was formalized inside a proof assistant, a computer program that allows for writing mathematical proofs in a stylized form and rigorously checks every intermediate step. Thus, leading to near 100 % trustability and paving the way for employing the tree theorem in other computer aided verification tools. Ultimately, this will result in highly reliable and powerful automated toolchains for proving the correctness of computer programs.Our certifier CeTA is an important step along the way to this ultimate goal. CeTA is a fully verified computer programming, again developed with the help of a proof assistant, that can certify the output of several existing termination tools (automated tools that try to prove termination of given computer programs) which are themselves written using conventional programming techniques and are thus susceptible to the same kind of errors that we want to rule out to begin with; thus the need for a certifier like CeTA. As part of this project we extended CeTAs capabilitiesmaking use of the earlier mentioned tree theorem and extrapolated a general framework that can be reused to build certifiers for other problem areas.