[Agda] Agda's coinduction incompatible with initial algebras

[Andreas Abel]

On 04.10.11 5:32 PM, Dan Doel wrote:
> On Tue, Oct 4, 2011 at 7:33 AM, Ulf Norell<ulf.norell at gmail.com>  wrote:
>> The problem, as I see it, is that sized types doesn't work with coinduction,
>> which we already knew.
>
> I've never looked into sized types much. Are we supposed to be able to
> apply a function whose termination is justified by decreasing size to
> a value whose size is ∞? Because that seems like part of the conflict
> here: infinite coinductive values get an infinite size, but then we're
> allowed to fold them anyway because the fold decreases the size (from
> ∞ to ∞ at each step :)).

Right.

But the principle of sized types can also be applied to coinduction, 
under the interpretation of "size" as "depth", i.e., number of guarding 
constructors.  Corecursion is sound if it increases the guardedness of 
the result in the body surrounding the recursive call (rather than 
increasing the size of the function argument as in the recursion case).

Yet that does not happen here.

> Of course, the way that Mu becomes Nu when applied to a particular
> functor is also weird.

That is the root of the problem.  Using sized types we reason 
inductively (Mu), using guardedness coinductively (Nu), about the same 
type, that is bound to fail.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/