The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Russell

On 7 Jun 2008, at 07:18, 
roconnor AT theorem.ca
 wrote:

> On Fri, 6 Jun 2008, Conor McBride wrote:
>
> > > Definition p : ones = cons ones
> >
> > Canonicity tells us that p's type should not
> > be inhabited.
>
> Why shouldn't ones and (cons ones) be convertable?  Can't we just  
> expand the cofixpoint of ones until the same number of constructors  
> are exposed as is in (cons ones), and then compare the resulting  
> terms?

You're right. Indeed, I've been known to suggest such
a thing. (Again, there's been some chat about it on
the Agda mailing list: coinduction has just arrived
in Agda and is getting some serious testing.) And..(*)

Nicolas's example highlights an imbalance between
match's enthusiasm for unfolding and conversion's
reluctance. It seems that one could restore this
balance in one of two ways: making match lazier,
or making conversion more enthusiastic.

I'm very much in favour of separating evaluation
from definitional equality (with the latter being
a type-indexed family of equivalences on values).
Definitional equality doesn't have to be some
(suitably optimized) alpha-equivalence of normal
forms arising from some SN and CR rewrite system.
If you want ones = cons ones, definitionally, you
clearly need to do more work in equality than you
do in evaluation.

> I'm probably being naive here.

(*)..the jury's out. I wrote an email to the Agda
list yesterday which was really enthusiastic
about this at the start and then more troubled at
the end. It seems very sensitive to the setup.

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.

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.

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.

All the best

Conor