On the Finitary Characterization of tex2html_wrap_inline20-Congruences

Paola Quaglia

December 1997


Some alternative characterizations of late full congruences, either strong or weak, are presented. Those congruences are classically defined by requiring the corresponding ground bisimilarity under all name substitutions.

We first improve on those infinitary definitions by showing that congruences can be alternatively characterized in the tex2html_wrap_inline20-calculus by sticking to a finite number of carefully identified substitutions, and hence, by resorting to only a finite number of ground bisimilarity checks.

Then we investigate the same issue in both the ground and the non-ground tex2html_wrap_inline24-calculus, a CCS-like process algebra whose ground version has already been proved to coincide with ground tex2html_wrap_inline20-calculus. The tex2html_wrap_inline24-calculus perspective allows processes to be explicitly interpreted as functions of their free names. As a result, a couple of alternative characterizations of tex2html_wrap_inline20-congruences are given, each of them in terms of the bisimilarity of one single pair of tex2html_wrap_inline24-processes. In one case, we exploit tex2html_wrap_inline34-closures of processes, so inducing the effective generation of the substitutions necessary to infer non-ground equivalence. In the other case, a more promising call-by-need discipline for the generation of the wanted substitutions is used. This last strategy is also adopted to show a coincidence result with open semantics.

By minor changes, all of the above characterizations for late semantics can be suited for congruences of the early family

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.