From Rewrite Rules to Bisimulation Congruences
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. This paper considers 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 are 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 a test of the theory it is shown that
bisimulation for a fragment of CCS is recovered. The transitions
generated for a fragment of the Ambient Calculus of Cardelli and
Gordon, and for SKI combinators, are also discussed briefly.
Back to my home page.