FORTissimo: Automating the First-Order Theory of Rewriting

Term rewriting is an abstract model of computation in which one can formally reason about computer programs written in a declarative programming language, for instance to infer that a program always computes a result (termination) or that different executions of the program yield the same result (confluence). To achieve this, a program is translated into a rewrite system that basically consists of rules for replacing expressions by equivalent but often simpler expressions. In this project we consider a syntactically restricted class of rewrite systems in which every property that can be expressed in the first-order theory of rewriting (first-order logic with rewrite relations as predicate symbols) is decidable. This includes properties like termination and confluence. The decision procedure was developed in the late 1980s and uses tree automata that operate on terms. A first implementation of the decision procedure was recently conducted by Franziska Rapp during her master thesis. The resulting tool FORT (First-Order Rewriting Tool) is equipped with a convenient synthesis mode to generate rewrite systems that satisfy a given property. Like any complex piece of software, FORT is likely to contain bugs. Formally proving its correctness is not an option because such a proof, if at all possible, is of limited value as FORT will further develop. Instead, to improve trust in FORT, one aim of this project is the certification of the output of FORT. This involves reproving the correctness of the tree automata constructions used in the decision procedure in an interactive proof assistant, resulting in a formalized tree automata library. Furthermore, suitable certificates have to be developed that can be produced by FORT and checked by the certifier that is obtained from the library via code generation. A second aim of the project is to improve the performance of FORT by adopting and developing state-of-the-art tree automata techniques. Parallel programming techniques will result in a further efficiency gain. Moreover, there are many different ways to transform a given formula into tree automata operation, all producing the same result but with a great variation in computation time and space. Techniques to find an efficient transformation will also be investigated. A final aim of the project is to improve the expressiveness of FORT by adding new features like support for properties that refer to two or more rewrite systems or the generation of witnesses. A better understanding of the limitations of FORT is also on the agenda. The expected outcome of the project is a highly efficient and trustworthy tool for the first-order theory of rewriting, ideally suited for educational purposes. Moreover, a comprehensive formalized tree automata library will be available for other developments.

FORTissimo: Automating the First-Order Theory of Rewriting Term rewriting is an abstract model of computation in which one can formally reason about computer programs written in a declarative programming language, for instance to infer that a program always computes a result (termination) or that different executions of the program yield the same result (confluence). To achieve this, a program is translated into a rewrite system that basically consists of rules for replacing expressions by equivalent but often simpler expressions. In this project we considered a syntactically restricted class of rewrite systems in which every property that can be expressed in the first-order theory of rewriting (first-order logic with rewrite relations as predicate symbols) is decidable. This includes properties like termination and confluence. The decision procedure was developed in the late 1980s and uses tree automata that operate on terms. An implementation of the decision procedure in the software tool FORT was the starting point of the project. Three new tools (FORT-h, FORT-s, FORTify) have been developed in the course of this project. These can be downloaded from the project website, where also a convenient web interface can be found. Like any complex piece of software, FORT is likely to contain bugs. To improve trust in FORT, we formalised a new variant of the underlying decision procedure in the proof assistant Isabelle. Compared to the original decision procedure, the new variant supports a richer language (e.g. properties involving multiple rewrite systems can be formulated) and handles a larger class of rewrite systems. We developed a formal language in which the key steps performed by the decision procedure can be expressed naturally. A new incarnation of FORT in Haskell, FORT-h, outputs certificates in this language. These certificates are checked for correctness by FORTify, a new and trustworthy program that is obtained from the Isabelle formalisation.