[TYPES] Equi recursive types: logical relations and intuition

[Paolo Giarrusso]

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.

Cheers,
-- 
Paolo G. Giarrusso