On the Finitary Characterization of pi-Congruences

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 pi-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 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 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 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.