[Agda] Agda goes coinductive

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Conor,  I completely agree with you, the strategy you have described has
been implemented by my student Karl Mehltretter in Mugda (MUnich aGDA).

It should be easy to add this to Agda as well.

On termination checking mutual corecursive definitions:

The basic idea is to treat the output of a corecursive function as an
additional input for the purpose of termination checking.

Thus, if your output is guarded, it is like a decreasing argument. In
Ulf's example:

mutual
  data SP (A B : Set) : Set where
    get : (A -> SP A B) -> SP A B
    <_> : SP' A B -> SP A B

  codata SP' (A B : Set) : Set where
    put : B -> SP A B -> SP' A B

eat : {A B : Set} -> SP A B -> Stream A -> Stream B
eat (get f)      (a :: as) ~ eat (f a) as
eat < put b sp > as        ~ b :: eat sp as

You have a lexicographic argument (output,first input) for termination here.

line 1: do not change guardedness of output, but decrease input:
        this is (<=, <)

line 2: guard output, but destroy relation to input (note that
        coconstructors destroy the structural ordering)
        this is (<,  ?)

This extends to mutual recursion using the foetus termination checker,
which has been spiced up to size-change termination.

Cheers,
Andreas

Conor McBride wrote:
> Hi
>
> On 5 Jun 2008, at 21:54, Dan Doel wrote:
>
>> On Thursday 05 June 2008, Ulf Norell wrote:
>>> One of the code sprints in the recent Agda meeting was to add
>>> coinductive
>>> datatypes to Agda.
>>
>> Excellent! In celebration, here's everyone's favorite monad:
>> partiality (a mix
>> of stuff from Abstract Nonsense for Functional Programmers and General
>> Recursion via Coinductive Types).
>
> Yes, this is splendid news! Well done! Wish I'd
> been there, but I had drycleaning, ironing,
> shaving, and punctuality obligations to
> discharge...
>
> And I was very pleased to see a Hancock classic
> (with which, by the way, Coq has been known to
> struggle) working out of the box. Of course, I'm
> now hoping to understand the criteria for
> accepting mutual definitions. There's plenty more
> where that came from, so I'm confident the new
> equipment will get lots thrown at it.
>
> So now our troubles really begin...
>
> [..]
>
>> codata D (a : Set) : Set where
>>   now   : a -> D a
>>   later : D a -> D a
>>
>> never : {a : Set} -> D a
>> never ~ later never
>
> [..]
>
>> codata _↑ {a : Set} : D a -> Set where
>>   diverge : {dx : D a} -> dx ↑ -> later dx ↑
>>
>> -- problems here
>> -- diverge-never : never ↑
>> -- diverge-never ~ diverge diverge-never
>> -- complaint: never != later never
>
> Ulf's just remarked:
>
> Ulf> This is the expected behaviour. When checking equality
> Ulf> it's not safe to unfold corecursive functions.
>
> [Later addition: what follows is an idea
> which has tempted me for a while, but which
> may, it turns out, have difficulties. Rather
> than editing the text with hindsight, I thought
> I'd just let you watch the crash...]
>
> That's certainly the case for /evaluation/. As
> some of you know, I suspect that one might try
> a little bit harder in a type-directed equality
> on normal forms. The intuition behind the
> suggestion is that one should be able to tell
> if two normal forms constitute "intensionally
> the same computation in different stages of
> evolution" by running the /initially/ less
> involved one for finite time.
>
> That's to say, when faced with deciding whether
>
>   ne == cocon (cocon ... (ut)) : CoDataType
>
> where neither ne nor ut is coconstructor-headed
> (substitute whatever coalgebraic notion is
> actually in place); note, there may be multiple
> ut's.
>
> repeatedly unfold ne until one of 4 things
> inevitably happens
>
> (1) ne fails to evolve a coconstructor
> because of some inner neutral thing gumming
> up the works, so say NO
> (2) the coconstructors emerging from ne
> conspicuously differ from those around ut,
> in which case say NO
> (3) ne evolves to the same pattern of
> coconstructors, wrapped around some neutral
> ne', in which case compare ne' with ut
> as neutral values
> (4) in some step, the coconstructors from
> ne pass leapfrog those around ut, so that
> the left-hand side is strictly more evolved
> than the right, hence they cannot come
> from the same mechanism, so say NO
>
> Crucially, we decide up front which side to
> evolve: we don't race the two. Moreover,
> we're not trying to find a /simulation/,
> just a more liberal /intensional/ match.
> So if you define new constants
>
>   fred ~ C fred
>   jim ~ C jim
>
> you get
>
>   fred == C fred
>   fred /= jim
>
> (Of course, if you were to elaborate fred
> and jim in terms of some universal unfold,
> then they would become equal, but that's
> under at least a few laters.)
>
> Key questions:
>
> (1) Does this loop?
>   I don't think so. Productivity of ne
>   guarantees that the tree of
>   coconstructors evolved increases strictly,
>   towards a bound given by the tree of
>   coconstructors around the ut's. We
>   continue either by saying no, or by
>   comparing neutral terms.
> (2) Is it a congruence? I'm not sure. It
>   seems stable with respect to further
>   evolution. I guess we also need to check
>   that if ne and ne' evolve to the same
>   coconstructory agglomeration, then ne
>   and ne' coincide. That's a worry:
>   what about
>
>     fred ~ C fred
>     jim  ~ C fred
>
>   ? Maybe there's too much generativity
>   around to get away with this approach.
>   Maybe something more fundamental is
>   wrong. Maybe we can recognize the
>   distinction between evolving recursive
>   fred and non-recursive jim.
> (3) Is this too intensionally brittle to
>   be helpful? My hope is that making ~
>   imply == might save a lot of basic
>   misery. But if generativity introduces
>   too many unexpected distinctions, we
>   might consider ourselves worse off.
>
> Of course, if it's too brittle to be a
> congruence, then it's no good, so we need
> to record it as a mistake from which to
> learn.
>
> Perhaps it's hubristic to try to squeeze
> a bit more out of the definitional equality
> here. These are infinite objects, so
> equational reasoning is inevitably going to
> be evidence-based. A decent implementation
> of coinduction is just what we need to bang
> the last few nails into the coffin of
> intensional propositional equality...
>
> All the best
>
> Conor
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFISYApPMHaDxpUpLMRAlO9AJ93gC1SWFCUJjaUjFhtVikZ/UmUUQCeLmzA
uTWRQDOra85HYr2nwzdDGBU=
=kul7
-----END PGP SIGNATURE-----