The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Thursday 17 September 2009 10:27:58 am Edsko de Vries wrote:

Pardon if this reply is too Agda-like. It's what I know, and this topic isn't 
particularly dependent on the specifics of either it or Coq.

> Suppose we have a simple coinductive data type:
> 
> CoInductive T : Set :=
> 
>    | A : T
>    | B : T
>    | C : T -> T.
> 
> Now there are terms that live in T such as
> 
>    C (C (C ... A))
>    C (C (C ... B))
> 
> with infinitely many C's followed by an A or a B.

I've conferred with some people on this, and I don't think I believe this is 
the case. It may be the case that in, say, traditional set theory, you can 
define some set via transfinite induction with values like these. But I don't 
think it's a good idea to say that, because you can do so in set theory, the 
type-theory type contains those values, but Coq merely doesn't allow us to 
talk about them, or something of that sort. Rather, I'd probably say that the 
type theoretic T doesn't contain values like that.

Indeed, if we go back to the category theory that coinductive data gets 
pulled 
from, values of T aren't "built of" constructors (not even infinitely many) 
at 
all. Rather, they are opaque values (more on this later) that can only be 
observed, and those observations come in three types:

  observe t = A
  observe t = B
  observe t = C t'

where t' is another opaque T value. Now, one can rephrase your original 
assertion in this sort of language, too, and say:

  there are terms that t and t' live in T such that
   the first infinitely many observations of t are C, and then after that we
    observe an A
   the first ... of t' ... and after that we observe a B

But how do you do infinitely many observations (let alone stuff after that)? 
Observations are in the inductive, evaluable part of Coq, so you can't. You 
could imagine of something like:

  EndsWithA' : Nat -> T -> Type

where values of type EndsWithA' n t are proofs what we observe an A after n 
or 
fewer observations of t. Then we can have:

  EndsWithA t = {n:Nat & EndsWithA' n t}

Now to express the above "infinitely many Cs" proof, it seems like we'd want 
to move from naturals to ordinals, and say something like:

  EndsWithA' (omega+1) t

However, I don't know of a constructive notion of ordinals that'd work for 
this, assuming it even works in classical set theory. Rather, in a 
formulation 
like:

  Inductive Ordinal : Set :=
    | Zero : Ordinal
    | Suc  : Ordinal -> Ordinal
    | Lim  : (Nat -> Ordinal) -> Ordinal.

the limit ordinals (Lim f) are used for parts of a process that take a number 
of steps corresponding to some f n, but n isn't necessarily known before that 
part of the process is reached (hopefully that isn't too vague). They aren't 
used to denote doing some step infinitely many times (after all, how could 
they? Coq/Agda/etc. functions are supposed to be terminating when dealing 
with 
inductive data).

So, hopefully I haven't rambled too much. In summary, I don't think it's 
helpful to think of T as really containing these transfinite sorts of values 
that Coq doesn't let us talk about. Rather, I'd say that T doesn't contain 
values like that, and of course we can't talk about them. :)

> Can I prove that if for [t1 t2 : T] we have [t1 <> t2], where [t1] and
> [t2] are constructively definable, then I must be able to distinguish
> between [t1] and [t2] in finite time? How can I define "constructively
> definable"?

I said I'd get back to the "opaque values" thing, and equality is where that 
pops up. Coinductives only being able to be observed (which is how the 
category theory defines them, more or less), means that (if you ask me) it's 
incorrect to treat them as being subject to evaluation. So, if you have 
definitions like:

  t1, t2 : T
  t1 = C t1
  t2 = C t1

You do *not* get, intensionally, t1 = t2. You cannot evaluate both to find 
out 
that you want C t1 = C t1, because they are not subject to evaluation (Coq 
actually treats them as if they are, unless I've missed some changes, which 
leads to problems in subject reduction).

This means that useful equality on coinductive types is extensional, defined 
by bisimulation: t1 = t2 iff observe t1 = observe t2, more or less. However, 
Coq's built-in equality is not extensional, and so it's not very useful 
coupled with this way of thinking.

(Last time I was talking about this here, someone demonstrated how to go from 
bisimulation to intensional equality in Coq, which I don't exactly 
understand, 
but it has to do with the above weirdness about coinductive terms actually 
being treated similarly to inductive terms with respect to evaluation, along 
with the rewrite tactic, I think. So while I don't think it *ought* to be 
possible, it apparently is.)

Anyhow, if you think about equality in terms of bisimulation, then a proof 
that t and t' are not bisimilar would be a proof that the two differ after 
some number of observations, and since I've above argued that T doesn't 
contain values that have transfinite numbers of Cs applied to A or B, you can 
safely make such proofs inductive. However, I don't really know how easy it 
is 
to go from t <> t' to the more extensional-type proofs. I'd wager it's 
possible, since t <> t' is a positive proof that they aren't equal, rather 
than just a lack of proof that they are, though.

> Any pointers to relevant literature would be appreciated,

If it's general thinking about coinduction, I think the paper

  A Tutorial on (Co)Algebras and (Co)Induction

is a good start, although it might be a little difficult if you don't have 
any 
prior experience with category theory. My understanding has also been 
influenced a lot by reading Anton Setzer's posts on the Agda mailing list, so 
you might want to investigate those, and maybe browse his publications 
(although I don't have anything specific there to recommend).

I hope this mail helped a little, and wasn't so rambling as to be useless. :)

Cheers,

-- Dan