Bisimilarity of Open Terms

The standard way of lifting a binary relation, R, from closed terms of an algebra to open terms is to de ne its closed-instance extension, Rci, which holds for a given pair of open terms if and only if R holds for all their closed instantiations. In this paper, we study alternatives for the case of (strong) bisimulation: we de ne semantic models for open terms, so-called conditional transition systems, and de ne bisimulation directly on those models. It turns out that this can be done in at least two di erent ways, giving rise to formal hypothesis bisimulation fh (due to De Simone) and hypothesis-preserving bisimilarity hp. For open terms, we have (strict) inclusions fh hp ci for closed terms, the three relations coincide. We show that each of these relations is a congruence in the usual sense, and we give an alternative characterisation of hp in terms of non-conditional transitions. Finally, we study the issue of recursive congruence: we give general theorems for the congruence of ea...

• Type: Journal
• Year: 2000
• Where: IANDC
• Authors: Arend Rensink
• Keywords: Bisimulation, IANDC 2000, Ne Semantic Models, Open Terms