The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 7 Jun 2008, Conor McBride wrote:

> Problem 1: races
> If I define
>   oneones = cons (cons oneones)
> should
>   oneones = cons oneones ?
> It's clearly dangerous to play this game too
> often, although we clearly need
>   ones = cons (cons ones)
>
> Solution 1: no overtaking
> We're not trying to find simulations here;
> we're trying to get a more liberal intensional
> match, so when we see x = cocon ..., we just
> want to know if x can be unfolded to the
> cocon... expression. If unfolding x jumps over
> the rhs, then it's not the same mechanism at
> work. cons oneones is out of phase with
> oneones, so they shouldn't be equal.

Right. I thought about this an hour after I sent my email.  The problem is 
that we really want the lemma forall x:Stream, x=cons x to hold because 
exactly the same proof holds for

Inductive Stream' : Type := cons' : Stream' -> Stream'.

I'd wager that (forall x:Stream, x=cons x) ought to hold for any fixed 
point of Identity, whether it is greatest, least, or otherwise.

Perhaps if we treat oneones as shorthand for two mutually recursive 
cofixpoints (each cofixpoint exposing exactly one constructor), we can 
mangage to pull only one constructor at a time.  Then (because of the 
symmetry existing between the form of the mutually recursive cofixpoints) 
we will see that (cons oneones) is convertable to oneones.

But I worry that there are (as you say) more snakes.  CoInductive types 
are very strange.  They are the only objects where computation "simplfies" 
the introduction rule (cofix) rather than simplifying the elimination 
rule.

> Problem 2: transitivity
> Define
>   fred = cons fred
>   jim = cons fred
> Should fred = jim? Yes, if both defining
> equations hold, but where's the provocation
> to unfold? If you want this to work, you
> need to ensure that fred can only be defined
> lazily and that jim cannot be defined lazily,
> or is otherwise seen to be unfoldable without
> provocation.
>
> Solution 2: ????????????
> But I have an idea, based on taking the
> one-step coalgebra as the primitive notion,
> and coding more liberal notions of CoFix.
> This (I hope) prevents definitions such as
> jim being expressed as degenerate cofixpoints.

Ah, one-step coalgebra sounds like what I said above.

> As the numbering scheme should suggest, there
> may be other problems. The snakes are very
> definitely alive, but I'm still optimistic
> and on the case.
>
> We live in interesting times.

It seems that without European TYPES funding, the theory of types is 
starting to fall apart.  Who knew it was the money that was holding it 
together. ;)

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''