Bisimilarity of Open Terms

Traditionally, in process calculi, relations over open terms, i.e., terms with free process variables, are defined as extensions of closed-term relations: two open terms are related if and only if all their closed instantiations are related. Working in the context of bisimulation, in this paper we study a different approach; we define semantic models for open terms, so-called conditional transition systems, and define bisimulation directly on those models. It turns out that this can be done in at least two different ways, one giving rise to De Simone's formal hypothesis bisimilarity and the other to a variation which we call hypothesis-preserving bisimilarity (denoted ~fh and ~hp, respectively). For open terms, we have (strict) inclusions ~fh c ~hp c ~ci (the latter denoting the standard “closed instance” extension); for closed terms, the three coincide. Each of these relations is a congruence in the usual sense. We also give an alternative characterisation of ~hp in terms of nonconditional transitions, as substitution-closed bisimilarity (denoted ~sb). Finally, we study the issue of recursion congruence: we prove that each of the above relations is a congruence with respect to the recursion operator; however, for ~ci this result holds under more restrictive conditions than for ~fh and ~hp.