Abstract

The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics.

In this talk I'll consider calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions can be given in each case, uniformly in the set of rewrite rules and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As examples, I'll show the labelled transitions for a fragment of CCS (for which the standard bisimulation is recovered), for SKI combinators, and for a fragment of the Ambient Calculus.