Relating step-indexed logical relations and bisimulations

  • Dimitrios Vytiniotis ,
  • Vasileios Koutavas

MSR-TR-2009-25 |

Operational logical relations and bisimulations are two particularly successful syntactic techniques for reasoning about program equivalence. Although both techniques seem to have common intuitions, their basis is on different mathematical principles: induction for the former, and co-induction for the latter. The intuitive understanding 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 and Koutavas-Wand (KW) bisimulations.

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 desirable properties of a SI logical relation. We then argue that SI logical relations and KW bisimulations approximate the same relation each in a distinct way. Finally we prove a somewhat surprising commutation theorem between unions and intersections that may be used as a new proof technique.