Conway's Game of Life and other orthogonal rewrite systems

We show how Conway's Game of Life (GoL) can be modelled using orthogonal graph rewriting. More precisely, we model GoL using 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 using 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 exhibited 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.
Here SC stands for Substitution Calculus, the calculus used for abstracting subgraphs into variables and substituting for them again (matching and substitution). In the case of INs the SC is particularly simple, and consists essentially in managing indirection nodes. We exemplify this decomposition extends to term rewrite systems (TRSs; having the simply typed λαβη-calculus as SC) and to term graph rewrite systems (TGRSs; having an SC, the ж-calculus, based on sharing), putting INs on a par with orthogonal TRSs and orthogonal TGRSs, thereby unlocking the theory of orthogonality to GoL and other cellular automata. For instance, that INs are confluent, even has least upperbounds, is an immediate consequence of orthogonality (confluence-by-parallelism).

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.