TY - JOUR AU - Quaglia, Paola PY - 1997/06/22 Y2 - 2024/03/28 TI - On the Finitary Characterization of pi-Congruences JF - BRICS Report Series JA - BRICS VL - 4 IS - 52 SE - Articles DO - 10.7146/brics.v4i52.19273 UR - https://tidsskrift.dk/brics/article/view/19273 SP - AB - 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. <br />We first improve on those infinitary definitions by showing that congruences can be alternatively characterized in the pi-calculus by sticking to a finite<br />number of carefully identified substitutions, and hence, by resorting to only a finite number of ground bisimilarity checks.<br />Then we investigate the same issue in both the ground and the non-ground pi-xsi-calculus, a CCS-like process algebra whose ground version has already been proved to coincide with ground pi-calculus. The pi-xsi-calculus perspective allows processes to be explicitly interpreted as functions of their free names. As a<br />result, a couple of alternative characterizations of pi-congruences are given, each of them in terms of the bisimilarity of one single pair of pi-xsi-processes. In one case, we exploit lambda-closures of processes, so inducing the effective generation<br />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. <br />By minor changes, all of the above characterizations for late semantics can be suited for congruences of the early family. ER -