Discussing "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types"

 (Link)

Author: Amal Ahmed (Harvard University)

Reference: Ahmed, A. (2006). Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_6

Why this paper? Cited by Fractional Resources in Unbounded Separation Logic, and Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions, and Recursive Session Logical Relations

When are two programs equivalent? There are various answers one can give to this depending on whether one wishes to consider factors like time and memory usage, but one fundamental notion is contextual equivalence: two programs A and B are equivalent in this sense if any program in the language with A as a component will behave the same (with respect to termination) if that component is replaced by B. Hence, there is no context which can tell them apart. This is an intrinsically difficult fact to prove because one must consider all possible contexts, of which there are infinitely many to choose from. A general technique for demonstrating contextual equivalence in typed languages is the method of logical relations, in which a general relation between programs is built up by induction on types, and the problem of proving equivalence for particular programs is narrowed to the problem of proving that these programs are related.

The problem with defining a relation in the inductive style is that it relies on types being defined in terms of simpler subtypes. This paper looks at two important type constructors for which this fails. Inductive types like lists and trees refer to themselves – lists are defined in terms of lists – in a way that would make a naïve inductive definition on them immediately circular. Quantified types – universal types for parametric polymorphism and existential types, which resemble abstract data types – contain type variables which can be replaced by arbitrarily complicated types. This paper, picking up an idea from Appel and McAllester, shows that the unpleasant circularities can be removed if one adds a natural number ‘step-index’ to the relation to make sure that the induction remains well defined – when one is working with a type and must consider a type that is not smaller, one reduces the step-index towards zero to compensate. A lot is proved about this style of reasoning – the full version of the paper weighs in at a hefty 169 pages!

This is certainly a relevant ‘classic paper’ with respect to my own research interests; I get involved in this area via later work by Birkedal, Møgelberg, Schwinghammer and Støvring on ‘synthetic’ step-indexing, which uses a modality to hide some of the arithmetic of step-indexing. But that is, perhaps, a topic for another day.