Relating step-indexed logical relations and bisimulations
Dimitrios Vytiniotis, Vasileios Koutavas · 2009
Operational logical relations and bisimulations are two particularly successful syntactic techniques for reason-ing about program equivalence. Although both tech-niques seem to have common intuitions, their basis is on different mathematical principles: induction for the for-mer, and co-induction for the latter. The intuitive un-derstanding of the two techniques seems more common, but their mathematical connection more ambitious, when each is combined with step-based reasoning, such as in the case of Appel-McAllester-Ahmed step-indexed (SI) logical relations [5, 4] and Koutavas-Wand (KW) bisimu-lations [12, 11]. In this paper we give an alternative formulation of a SI logical relation in the style of Appel-McAllester-Ahmed. We derive this from a definition that is parametric on the indexing scheme by requiring it to satisfy the desir-able properties of a SI logical relation. We then argue that SI logical relations and KW bisimulations approxi-mate the same relation each in a distinct way. Finally we prove a somewhat surprising commutation theorem be-tween unions and intersections that may be used as a new proof technique. 1