11
$\begingroup$

You can encode ordinals in Coq as

Inductive ord := O | S (n: ord) | Lim (s: nat -> ord).

Suppose you use the following encoding instead

CoInductive stream A := {
  head: A ;
  tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).

Can you make an induction principle go through?

I tried in both Coq and Agda but the obvious induction principle doesn't seem to work

{-# OPTIONS --guardedness #-}
module ord where

record stream (A : Set) : Set where
  coinductive
  constructor _::_
  field
    head : A
    tail : stream A

record Forall {A : Set} (P : A → Set) (x : stream A) : Set where
  coinductive
  constructor _:>_
  field
    forhead : P (stream.head x)
    fortail : Forall P (stream.tail x)

data ord : Set where
  o : ord
  s : ord → ord
  sup : stream ord → ord

open stream
open Forall

ind : (P : ord → Set) → P o → ((x : ord) → P x → P (s x)) → ((x : stream ord) → Forall P x → P (sup x)) → (x : ord) → P x
ind P onO onS onSup = loop where
  loop : (x : ord) → P x
  loop o = onO
  loop (s x) = onS x (loop x)
  loop (sup x) = onSup x (gen x) where
    gen : (y : stream ord) → Forall P y
    forhead (gen y) = loop (head y)
    fortail (gen y) = gen (tail y)

(Agda termination checker complains about the recusive calls to gen and loop.)

$\endgroup$

1 Answer 1

6
$\begingroup$

It makes sense to want something like this, but Agda's termination/productivity checker does not actually validate this interpretation of the types. The reasoning behind your induction principle is presumably:

  1. $\mathsf{stream}\ A$ is an infinitely long stream of whatever $A$ is.
  2. $\mathsf{ord}$ is a well-founded tree that delegates to $\mathsf{stream}$ to achive an infinitely wide branching factor.

However, Agda accepts the following definition:

bad : ord
bads : stream ord

bad = lim λ where
  .head → zero
  .tail → bads

bads .head = bad
bads .tail = bads

$\mathsf{bad}$ is not a well-founded tree, and contradicts the induction principle:

P : ord → Set
P zero = ⊤
P (suc o) = ⊤
P o@(lim s) = o ≡ head (tail s) → ⊥

lemma : ⊥
lemma =
  ind P _ (λ _ _ → _)
    (λ s fp eq → subst P (sym eq) (forhead (fortail fp)) eq)
    bad refl

The issue is that coinduction in Agda (and I suppose also Coq) does not really act in a 'compositional' way. You can't just say that $\mathsf{ord}$ is the initial algebra of the functor $1 + o + \mathsf{stream}\ o$; it actually has some more complicated specification owing to $\mathsf{stream}$ being defined coalgebraically.

There are some (not great) justifications you could use for this behavior. The above functor is not strictly covered by the more rigorous foundational schemas for (co)inductive definitions, so in that sense it requires some interpretation, and that interpretation could well be one that matches Agda's checker. Also, if the two types were mutually defined, it's a lot less clear whether it should mean something primarily algebraic or coalgebraic. But it's unfortunate that some mixed (co)inductive specifications just can't be written in Agda/Coq.

(Note, I'm not very familiar with coinduction in Coq; just assuming based on the question that it behaves similarly to Agda.)

Addendum: if you want to more reliably predict what definitions Agda will accept for types involving coinduction, it helps to imagine that they are actually picking out certain well-defined values of an analogous domain-theoretic definition (where coinduction is more 'lazy'). But even that is not completely straight forward. For instance, using

bad = lim bads

above would be rejected.

$\endgroup$
6
  • 1
    $\begingroup$ You'd assume as stream A is isomorphic to nat -> A there'd be some way of making things work though. $\endgroup$ Mar 6 at 3:25
  • 2
    $\begingroup$ Whoa, that's bizarre. In Cubical Agda, at least, stream A is provably equivalent to nat -> A, right? So doesn't this make it inconsistent, since the nat -> A version does satisfy the induction principle? $\endgroup$ Mar 6 at 17:42
  • 1
    $\begingroup$ @MikeShulman but it's not an initial algebra of 1 + o + stream o. IIRC polynomial endofunctors are equivalent to just endofunctors but translating stream to a polynomial just gives you a weird encoding of nat -> o. So Agda could have that interpretation but it doesn't. It still confuses me. $\endgroup$ Mar 6 at 18:35
  • $\begingroup$ Also I'm not sure I made this clear but I kind of suspected that the induction principle wasn't quite right from the beginning and was looking for a more appropriate one. I also tried relators and sized types. gist.github.com/mstewartgallus/c2e6c39e5f45a9b52f836d3ddb4cf6f4 gist.github.com/mstewartgallus/… relators (see joachim-breitner.de/blog/… ) don't really work in the obvious way as you can't construct reflexivity for eq. $\endgroup$ Mar 6 at 18:43
  • 2
    $\begingroup$ @MikeShulman I think the answer to this is no. You can't just define the induction principle by transporting through ℕ → ord, because the checker won't accept that the recursive call is smaller. I think you also can't prove that the two types are equivalent, because one of those functions will be rejected just like the induction principle (for the stream one). Essentially, data definitions do not respect paths. It's possible I just haven't been devious enough to trick it, though. $\endgroup$
    – Dan Doel
    Mar 6 at 20:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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