Computer Laboratory

Technical reports

From rewrite rules to bisimulation congruences

Peter Sewell

May 1998, 72 pages

Abstract

The dynamics of many calculi can be most clearly defined by 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 arbitary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is esentially 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.

Full text

PS (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-444,
  author =	 {Sewell, Peter},
  title = 	 {{From rewrite rules to bisimulation congruences}},
  year = 	 1998,
  month = 	 may,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-444.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-444}
}