[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear types mailing list, thanks for the many responses and for the suggestions :) @arthur: what you suggest is (more or less) indeed what we’re looking into! cheers, marco > On 15 Nov 2018, at 12:11, Arthur Azevedo de Amorim <arthur...@gmail.com> > wrote: > > > > Em qui, 15 de nov de 2018 às 08:29, Paolo Giarrusso <p.giarru...@gmail.com> > escreveu: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > On Thu, 15 Nov 2018 at 12:13, Marco Patrignani <m...@cs.stanford.edu> 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. > > > In this vein, you could probably add another translation from iso- to > equi-recursive types and show that the translation and the original term > simulate each other. You could use the iso-recursive types to define the > logical relations, and transport the equivalences proved via this logical > relation to the equi-recursive final target. > > Cheers, > -- > Paolo G. Giarrusso --- Marco Patrignani http://theory.stanford.edu/~mp Stanford Computer Science Department, USA & CISPA, Saarland University, Germany