workshops at Gutenberg Building (Gustav-Freytag-Straße 40) (street map, building map, campus views), in these rooms (all on the first floor):
lunch at Mensa Academica (across Gustav-Freytag street)
19:00 informal pre-workshop meeting, Restaurant Connstanze, map.
I (JW) book a table, everyone pays for themselves. If you want to join, tell me by email.
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:
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:
08:30 registration
09:00 - 10:00 IWC Session 5
10:00 coffee
10:25 - 11:45 IWC Session 6 = WST Session 1 (session chair: Johannes Waldmann)
11:45 short break
12:00 - 13:00 WST Session 2 (session chair: Aart Middeldorp)
13:00 lunch
14:30 - 15:30 WST Session 3 (session chair: Pierre Lescanne)
15:30 coffee
16:00 IWC + WST excursion and dinner
We present MU-TERM GTRS, a tool designed to prove termination of Generalized Term Rewriting Systems (GTRSs). In these systems, rewriting computations are defined by rules that may include conditions expressed using atoms defined by Horn clauses—particularly conditions involving reachability, joinability, and conversion. Termination control is enhanced through the use of a replacement map, which explicitly specifies the argument positions of function symbols where rewriting is allowed. GTRSs offer a powerful framework for modeling computations in advanced reduction-based languages such as Maude. paper
Concerts at Thomaskirche (where Johann Sebastian Bach worked as cantor from 1723 to 1750):