IWC 2025

We show how Conway's Game of Life (GoL) can be modelled by means of orthogonal graph rewriting. More precisely, we model GoL by means of a graph rewrite system where each cell of the grid is represented by a node having 8 ports, each linked to one of its 8 neighbouring nodes. A rewrite rule then lets a node cyclically rotate its principal port to the next (either widdershins or deosil) port while updating its alive-neighbour-count. After a full rotation, its state is updated accordingly. We show this yields a graph rewrite system (GRS) where computing the next GoL-iteration may be achieved in 8 ticks by means of what we call ©locksteps better known in rewriting as full multisteps contracting all redex-patterns in the graph in parallel. The GRS being orthogonal liberates one from having to perform ©locksteps only, to always contract all redex-patterns: orthogonality makes that redex-patterns may be contracted asynchronously, even one at the time, need not be contracted in lockstep. There are no clogsteps (so to speak), making the modelling ideally suited for implementation on GPUs.

In the second part of the presentation we show in what sense the graph rewrite system used to model GoL in the first part is orthogonal. We show it constitutes a so-called Interaction Net (IN) and that a (single) step from graph G to graph H with respect to rule rule ρ : L → R can be decomposed into three phases:

1. the matching phase, an SC-expansion G_SC↞ C[L] exhibiting the to-be-replaced substructure L within G;
2. the replacement C[L] → C[R] of the exihibited substructure L, left-hand side of rule ρ, by its right-hand side R;
3. the substitution phase, an SC-reduction C[R] ↠_SC H plugging-in the substructure R yielding H.

References: there being an abundance of literature on Game of Life and on Interaction Nets, we only give references to the lesser-known approach to structured rewriting by means of Substitution Calculi: van Oostrom, PhD thesis, VUA, 1994, van Raamsdonk, PhD thesis, VUA, 1996, Hirokawa, Nagele, van Oostrom, Oyamaguchi, CADE, 2019, van Oostrom, HOR, 2025.

We lift two well-known confluence techniques—the redundant rules technique and the reduction method—from term rewrite systems to logically constrained term rewrite systems. We establish sufficient criteria for both techniques in the constrained setting, increasing flexibility of confluence analysis.

We generalize the concept of critical pairs from Nipkow’s pattern rewrite systems to higher-order rewrite systems where the left-hand sides of rules can be deterministic higher-order patterns.

For a programming language, there are two kinds of term rewriting: run-time rewriting (“evaluation”) and compile-time rewriting (“refinement”). Whereas refinement resembles general term rewriting, evaluation is commonly constrained by Felleisen’s evaluation contexts. While evaluation specifies a programming language, refinement models optimisation and should be validated with respect to evaluation. Such validation can be given by Sands’ notion of contextual improvement. We formulate evaluation in a term-rewriting-theoretic manner for the first time, and introduce Term Evaluation and Refinement Systems (TERS). We then identify sufficient conditions for contextual improvement, and provide critical pair analysis for local coherence that is the key sufficient condition. As case studies, we prove contextual improvement for a computational lambda-calculus and its extension with effect handlers.

The introduction of infinitary rewriting and in particular of infinitary λ-calculi created a syntactic bridge between the dynamics of rewriting systems and their semantics. Confluence, already a highly desirable property for a finitary rewriting system, becomes even more important in this setting as it ensures uniqueness of infinitary normal forms. A seemingly orthogonal line of work led to the advent of a linear approximation of the λ-calculus based on Taylor expansion, which allowed for a renewal and a refinement of the classic approach based on continuous approximation, and for a whole range of new, elegant proofs of key results in λ-calculus. In previous work (Cerda and Vaux Auclair, LMCS, 2023), we demonstrate how infinitary λ-calculus appears to be the “missing ingredient” thanks to which we could give a general, canonical presentation of the linear approximation of the λ-calculus. In this talk, we take a somehow dual perspective and explain what linear approximation brings to infinitary λ-calculi. In particular, we present a linear “Simulation” theorem for the 001- and 101-infinitary λ-calculi, and detail how confluence of the given infinitary λ-calculi can be deduced. We also evoke the remaining infinitary λ-calculi, stating a negative result preventing the construction of a suitable linear approximation.

Sets of equations E play an important computational role in rewriting-based systems R by defining an equivalence relation =_E inducing a partition of terms into E-equivalence classes on which rewriting computations, denoted →_R/E and called rewriting modulo E, are issued. This paper investigates confluence of →_R/E, usually called E-confluence, for conditional rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize the framework to be used with conditional systems. Then, we show how to define appropriate finite sets of conditional pairs to prove and disprove E-confluence. Our results apply to well-known classes of rewriting-based systems. In particular, to Equational (Conditional) Term Rewriting Systems.

Pattern completeness is the property that the left-hand sides of a functional program or term rewrite system cover all cases w.r.t. pattern matching. This or related properties are required, if one wants to perform ground confluence proofs by rewriting induction. In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness. The algorithm has an asymptotic optimal complexity, as it belongs to the complexity class co-NP. It has been verified in Isabelle/HOL and outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.

Given a first-order theory Th, we say that a boolean combination F of atoms is Th-feasible if there is a substitution σ such that σ(F) is deducible from Th, i.e., Th ⊢ σ(F) holds. Otherwise, F is infeasible. In the realm of (conditional) term rewriting, many interesting problems can be treated as (in)feasibility problems: joinability of terms (and critical pairs), reachability, reducibility, etc. This paper shows how general feasibility problems can be handled now with the new version of the tool infChecker.

Despite sixty percent of Newman’s seminal 1942 paper being devoted to residual theory, that remains obscure due to that his instantiation of the theory there to the (non-erasing) λβ-calculus was fatally flawed. We redeem the approach showing: 1) any rewrite system instantiating his theory induces a so-called 1-ra, an axiomatically orthogonal rewrite system, entailing co-initial reductions have least upperbounds; 2) the rewrite system underlying any (non-erasing) syntactically orthogonal TRS instantiates his theory.

In this presentation I give an incomplete overview of the many contributions of Hans Zantema to termination and confluence. Several of these were presented at earlier workshops on termination and confluence, and I include a biased overview of the development of these workshops and associated competitions.