[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Thu, 15 Nov 2018 at 12:13, Marco Patrignani <[email protected]> wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear types mailing list, > I have some questions related to equi recursive types. > However, this seems a limitation that stems purely out of the proof technique. > If we had something else to “decrease" rather than an operational step, the > proof would go through. > ** Q1 : logical relation for equi-recursive types ** > Looking at logical relations for languages with recursive types, they all > seem to have iso-recursive ones. > Is there a sound logical relation for a calculus with equi-recursive types? Yes, equirecursive types are used by both Appel and McAllester [2001, An Indexed Model of Recursive Types for Foundational Proof-Carrying Code] and Ahmed's PhD thesis (Sec. 4.2.1); they also appear in Appel et al. [2007] tho in a different context. Beware Appel and McAllester's binary logical relation has an issue, fixed by Ahmed [2006, Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types]. Contrast that model with the one by Dreyer, Ahmed and Birkedal [2011, Logical Step-indexed Logical Relations]: in that model only fold-unfold reductions are counted as steps in the expression relation, because that's the only reduction that produces a result that is only valid *later*. Instead, with equirecursive types, it's easier to give meaning to mu X. F X if F is *contractive* (that is, only depends on X *later* — the name is 'well-founded' in earlier papers), so models with equirecursive types make all their type constructors contractive; as a result, all reduction steps must be counted. ================ > However, for logical relations it seems that the operational aspect (the > extra reduction step) introduced by iso recursive types is a key > distinguishing feature between iso and equi recursive types. The importance of step counts, here and elsewhere, it's one of the few downsides of step-indexing. This is discussed by Svendsen et al. [2016, Transfinite Step-Indexing: Decoupling Concrete and Logical Steps] and earlier by Benton and Hur [2010, Step-Indexing: The Good, the Bad and the Ugly, http://drops.dagstuhl.de/opus/volltexte/2010/2808/]. There is often an (inelegant but effective) fix, which I haven't seen in the literature but appears to be folklore among specialists; I describe this to emphasize that the problem is artificial. One can add a "nop" instruction to terms, `t ::= nop t | ...`, and emit it when translating terms, just to consume one more step; that would play the role of the extra steps. One can then "postprocess" terms to remove the nop instructions, and show this preserves equivalence through a simulation lemma. It is more elegant to hide such steps into the elimination forms of some type, but such hiding is a purely syntactic operation. Cheers, -- Paolo G. Giarrusso
