[TYPES] Equi recursive types: logical relations and intuition

[Marco Patrignani]

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.aa at gmail.com> wrote:
> 
> 
> 
> Em qui, 15 de nov de 2018 às 08:29, Paolo Giarrusso <p.giarrusso at 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 <mp at 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