4
$\begingroup$

I was messing around with induction stuff again and some stuff seems to require bisimilarity relations instead of just equality when dualizing for coinductive types.

CoInductive stream A := {
  head: A ;
  tail: stream A ;
}.
Arguments head {A}.
Arguments tail {A}.

Requires something like

CoInductive eq_stream {A} (x y: stream A) := {
  eq_head: head x = head y ;
  eq_tail: eq_stream (tail x) (tail y) ;
}.

I vaguely recall a little about bisimulation and coinductive types but I would really like if someone could explain the situation in detail.

I understand the situation is a little like extensionality for functions but I don't quite get the details why. Maybe a system like Cubical Agda doesn't require the same workarounds?

I vaguely recall it's consistent to add an axiom like Axiom bisim: forall {A} (x y: stream A) -> eq_stream x y -> x = y. But this is a bit ad-hoc.

You can maybe use M types/containers for a single generic axiom. Something like the following where there's a small amount of annoyance rewriting a dependent field I didn't want to figure out right now.

CoInductive M {A} (B: A -> Type) := {
  tag: A ;
  field (x: B tag): M B ;
}.
Arguments tag {A B}.
Arguments field {A B}.

CoInductive M_eq {A} {B: A -> Type} (x y: M B):= {
  eq_tag: tag x = tag y ;
  eq_field f: M_eq (field x f) (field (rw eq_tag y) f)  ;
}.

Axiom bisim: forall {A} {B -> Type} (x y: M B), M_eq x y -> x = y.

But I'm definitely not sure of all the details of this. Not at all sure universe polymorphism would make this generic enough either.

Why do coinductive types require bisimilarity relations? And given for now we have to work around it what's the best way of doing so?

Improve this question
$\endgroup$
4
  • 4
    $\begingroup$ There is a thread discussing this topic in groups.google.com/g/homotopytypetheory/c/tYRTcI2Opyo/m/… . Have a look at first 2 answers from Peter Le Fanu Lumsdaine and Mike Shulman. $\endgroup$
    – L. Garde
    Jun 4, 2022 at 9:55
  • 1
    $\begingroup$ Incidentally, I think it's correct (per that thread) that univalence does not imply extensional equality of coinductive types in e.g. normal Agda. The proofs for function extensionality rely on η for functions, but no such principle is available for codata. So, the analogous proofs about streams would be stuck on lemmas like $s = \mathsf{map}\ \mathsf{id}\ s$, unless someone knows how to derive η from univalence (I haven't seen it). However, cubical Agda makes extensional equality of coinductives very natural. $\endgroup$
    – Dan Doel
    Jun 4, 2022 at 23:36
  • $\begingroup$ @DanDoel Ok so I don't really get the eta stuff in Coq but it sounds to me today it would be simplest to postulate function extensionality + eta equality. Then coinductive extensionality ought to be provable as a theorem. So something like Axiom eta: forall A (B: A -> Type) (x: M B), x = {| tag := tag x ; field := field x |}.. $\endgroup$
    – Molly Stewart-Gallus
    Jun 5, 2022 at 5:21
  • 1
    $\begingroup$ I don't know exactly what kind of eta rule is necessary. For instance, a one-step rule might not be sufficient to prove that $\mathsf{map\ id}$ is the identity. The analogous fact for functions is $f = (λx. \mathsf{id}(f\ x))$. By reducing under the binder, we perform the analogue of infinitely many reductions on a coinductive type. In cubical Agda, what allows this to work is that $s \equiv t$ is a special sort of $I → \mathsf{Stream}$, which can be defined by corecursion. Perhaps univalence somehow lets the one-step rule expand to the corecursive rule, though. I don't really know. $\endgroup$
    – Dan Doel
    Jun 5, 2022 at 20:04

2 Answers 2

Reset to default
4
$\begingroup$

Coinductive types "require bisimilarity instead of =" for the same reason function types "require forall x, f x = g x instead of f = g." In the absence of axioms (in the closed context), every element of x = y is supposed to compute down to eq_refl. Further, in order for eq_refl : x = y to be type-correct, x and y should be definitionally equal (i.e. the typechecker should be able to automatically synthesize a series of reductions that automatically brings them to the same form). But proofs of stream bisimilarity or function equality-at-all-points (can be) infinite objects, representing infinitely many steps of reduction. Automatically generating and checking the right sequence of infinitely many steps is undecidable, so the typechecker cannot do it. So neither eq_refl nor any "computing" term of type x = y can prove bisimilar streams (or equal-everywhere functions) equal. (This is a metatheoretic statement. There are no terms in the language of Coq that prove e.g. map id nats = nats but Coq does not "know" that about itself: It doesn't prove map id nats <> nats either.)

Your general M-type bisimilarity axiom seems reasonable. A similar thing is in fact provable in Cubical Agda (where refl is no longer the only way to prove equality). Therefore, I would say you've stated your axiom correctly, and nothing should blow up if you continue using it (since Coq + your axiom is roughly a sublanguage of Cubical Agda). I'm not sure how it will interact with other axioms, though.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ An opinionated view on things like cubical Agda: it is natural to think that coinductive types should have equality/path types that are themselves coinductive. Then refl is a derived notion, given by any definition that yields observation-wise reflexive paths, not a constructor. We are not (necessarily) adding other ways to prove equality, we are just no longer under the delusion that we can feasibly detect reflexive paths, or that e.g. $\mathsf{J}$ could reasonably wait to do so. The identity obtained from the point-wise reflexive bisimulation is reflexive, just not observably so. $\endgroup$
    – Dan Doel
    Jun 8, 2022 at 0:18
5
$\begingroup$

Semantically, bisimulation just is the correct notion of equality for coinductive types. A nice intuition for it comes from parametricity.

The Church encoding of a coinductive stream type $\nu a.\,(\Bbb{N} \times a)$ is $\exists a.\, a \times (a \to \Bbb{N} \times a)$.

Parametricity for existential types tells that two elements of this type $(A, x, f)$ and $(B, y, g)$ are related when:

  • There is a relation $R \subseteq A \times B$, such that
  • $(x, y) \in R$, and
  • for all $(a, b) \in R$, if $f(a) = (n, a')$ and $g(b) = (m, b')$ then $(a',b') \in R$ and $n = m$.

This is exactly the definition of a bisimulation!

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.