Confluence: Automation, Certification, Extensions

This project is concerned with confluence of term rewrite systems. In contrast to termination, automating confluence conditions is a research topic which has received little attention so far and we are not aware of any efforts towards certification. The aim of this project is to change this. More precisely, the aims are to 1. automate confluence criteria, 2. certify confluence proofs, and 3. extend confluence research. The first aim is to automate sufficient conditions for confluence that go beyond the techniques implemented in ACP, a confluence prover which was recently developed in Japan. This will stimulate research for new criteria and as a long-term effect we intend to establish an international competition for confluence tools (similar to the existing competition for termination provers). Various bugs in termination provers have shown the need for independent certification of the tools` output. The second aim of the project is to certify confluence proofs. To this end powerful sufficient criteria for confluence will be formalised and a format for representing proofs will be designed. The third aim of the project is to extend confluence research. One extension is concerned with a variation of the Knuth-Bendix completion procedure to derive confluent systems in the absence of termination. Another extension is to lift sufficient criteria to higher-order rewrite systems. The third topic for extensions is concerned with extending known results for orthogonal rewrite systems to a larger class of confluent rewrite systems.

An important property of programs is termination: Will a program produce a result eventually? In the context of first-order term rewriting, this property has been widely studied, and some of the techniques developed in this context are applied to analyze real- world programs. Another interesting question one may ask about programs is whether they always produce the same result, given the same input. This issue is of increasing importance because many programs are running their computations in parallel, which often makes them non-deterministic. Confluence is a property that ensures that results are always the same even with non-deterministic evaluation.This project makes several contributions to the theory of confluence of first-order term rewrite systems and its automation and certification, which is a stepping stone towards verifying correctness of software mechanically. We developed various new techniques for automatically proving confluence. Besides advancing the theory of confluence, our main contribution is an automatic tool, CSI, which can establish or disprove confluence of many first-order term rewriting systems automatically. Furthermore, we have made significant progress to verifying the resulting proofs by an independent, highly trustworthy certification tool.Our object of study are first-order term rewrite systems, which are sets of directed equations that can be used to rewrite terms, for example to simplify them. Such systems of rewrite rules can be very powerful. In fact they can express arbitrary computer pro- grams. Thanks to the simple theoretical foundation, studying term rewrite systems is an attractive stepping stone for developing techniques for analyzing real-life programs.In this project, we developed a tool (CSI) that can establish or disprove confluence of many first-order term rewrite systems automatically. Because CSI is just a computer program, another problem arises: Are the answers produced by the tool actually correct? The code is non-trivial and therefore may contain bugs. In order to increase the trust in the generated proofs, we have begun to extend CeTA, a certifier for termination proofs, to cover confluence proofs as well. In contrast to CSI, CeTA is actually developed in an interactive theorem prover, and all its code is provably correct. Therefore, CSI in combination with CeTA will produce highly trustworthy proofs of confluence (or non- confluence) of first-order term rewrite systems.In the course of the project a dedicated workshop on the topic of confluence and a competition of automated confluence provers have been initiated. These take place annually since 2012 and have given a renewed interest to the topic of confluence.