The notion of confluence, which generalizes the one of determinism, is a central and ubiquitous property of computational and deductive systems. Its study is one of the main topics of rewriting theory, where it relates to other properties such as termination, modularity, commutation, and completion. It has been investigated in many formalisms of rewriting, such as conditional and unconditional first- and higher order rewriting, λ-calculi, and constraint rewriting. This special issue presents a selection of novel results and recent computational techniques related to confluence.
The conception of the edition of this special issue follows from the substantial progress on confluence, presented during the 9th International Workshop on Confluence (IWC) that took place remotely due to pandemics (as part of the Paris Nord Summer of LoVe 2020 organized at the Université Paris 13), which was collocated with the 5th International Conference on Formal Structures for Computation and Deduction (FSCD) and the 10th International Joint Conference on Automated Reasoning (IJCAR).
The six articles presented in this issue of Mathematical Structures in Computer Science have been carried out by researchers from renowned institutions on three continents. They cover many aspects of the different areas of computer science concerned by confluence:
String diagram rewrite theory III: Confluence with and without Frobenius, by Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and Fabio Zanasi, shows that confluence for double-pushout rewriting with interfaces is decidable, which includes string diagram rewriting as a particular case;
Confluence of algebraic rewriting systems, by Cyrille Chenavier, Benjamin Dupont, and Philippe Malbos, introduces the structure of algebraic polygraph modulo (which includes string, linear, and group rewriting systems) and shows a critical branching lemma for those;
Confluence of left-linear higher order rewrite theories by checking their nested critical pairs, by Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, and Jiaxiang Liu, shows that higher order rewriting in combination with β-reduction is confluent on untyped λ-terms if all its nested higher order critical pairs admit decreasing rewrite diagrams, with application to proof assistants;
On reduction and normalization in the computational core, by Claudia Faggian, Giulio Guerrieri, Ugo de’ Liguoro, and Riccardo Treglia, studies the reduction in an λ-calculus derived from Moggi’s computational λ-calculus, the computational core;
A Rewriting Coherence Theorem with Applications in Homotopy-Type Theory, by Nicolai Kraus and Jakob von Raumer, formalizes the construction of homotopy basis of rewriting systems from confluence and well-foundedness, with applications in homotopy-type theory;
Z property for the shuffling calculus, by Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa, gives a new proof of confluence for the call-by-value lambda calculus
with permutation rules.
with permutation rules.We want to thank all authors for their willingness and dedication; indeed, presenting in an amenable manner, and with the required rigour, such scientific developments are not easy. In addition to the kind and expeditious editorial work of the journal administrators, editing this issue was only possible due to the thoughtful contributions of anonymous referees. We thank them all for their readiness and competence, ensuring that accepted articles meet the highest standards of quality and validity.
Mauricio Ayala-Rincón and Samuel Mimram
Brasília and Paris
