From Confluence to Unique Normal Forms: Certification and Complexity

This project is about confluence and the related unique normal form property of rewrite systems. In the preceding years many powerful confluence methods have been developed and implemented in confluence tools that participate in the recently established confluence competition. Important first steps towards certification have been made, but much remains to be done. The aim of this successor project is to fill two important gaps concerning certification, investigate methods for the unique normal form property, study various complexity issues related to confluence and unique normal forms, and further develop the confluence tool CSI and the certification tool CeTA for confluence. More precisely, the aims are to 1. formalize the layer framework that captures important divide and conquer results for confluence like layer-preservation and modularity into a single abstract framework, 2. develop a formalized proof for the confluence of development closed left-linear (higher- order pattern) rewrite system based on proof terms and residual theory, 3. investigate conditional linearization and related techniques like Chew`s theorem to obtain automatable techniques for unique normal forms, 4. study (tractable) decidable classes for confluence and unique normal forms as well as ways to lower the complexity of the various search problems that underlie concrete confluence methods, 5. use the insights gained in the previous items to increase the confluence proving power and efficiency of the automatic confluence tool CSI and the automatic certification tool CeTA with regard to confluence.

An important question of programs is whether they always produce the same result on a given input. For programs that run in a distributed and parallel environment, this is not at all obvious. Unique normal forms is an abstract property that ensures that results are always the same, independent of the computation path. Confluence is a well-known property that guarantees unique normal forms. In the absence of confluence, unique normal forms is a desirable property. In this project we made several contributions to the theory of confluence and unique normal forms for term rewrite systems, in particular concerning automation and formal verification. Term rewriting is an abstract model of computation based on rewrite rules, which are directed equations between equivalent expressions, used to evaluate and simplify expressions. Numerous applications exist, ranging from program analysis and compiler optimization to deciding validity problems in logical and mathematical structures. Term rewriting comes in different flavours, depending on the expressions that are modeled (first-order terms, many-sorted terms, higher-order terms, terms with constraints, ...) and the restrictions placed on the evaluation mechanism (unrestricted rules, rules with side conditions, ...). Various new techniques for automatically (dis)proving confluence and unique formal forms were developed, both for first and higher-order rewrite systems. Besides advancing the theory, the main contributions of the project are automatic tools for first (CSI) and higher-order (CSI^ho) rewriting. Considerable effort went into formally verifying techniques that are used in CSI by an independent and highly trustworthy certification tool (CeTA). This includes important divide-and-conquer results for establishing confluence, like Toyama's celebrated modularity theorem, stating that the union of two confluent first-order rewrite systems that do not share function symbols is again confluent, and the result that confluence of a first-order rewrite systems follows from the confluence of its well-typed terms according to any compatible many-sorted sort attachment. The formal verification efforts were conducted in the Isabelle/HOL proof assistant, on top of the IsaFoR library. In addition, new complexity bounds were obtained for confluence and related properties for the decidable class of ground rewrite systems. To facilitate dissemination of our contributations and also to serve the research community, we actively developed the international Confluence Competition and surrounding infrastructure, which led to an increased activity world-wide in the development of software tools for confluence and related properties for a variety of rewrite formats. In the latest (May 2019) edition 15 different tools developed by research teams from 5 different countries competed in 12 categories. Compared to the previous year, 5 tools and 3 categories were new.