[Agda] Termination checking on coinduction

[Alex Rozenshteyn]

I've skimmed the paper (I think I understood up to and including section 2.4).

It seems that I can't write a split function of this sort at all, even
if it produces a Colist (List A), because there exist pathological
inputs which produce no progress.

I think I could require a proof of something...

I'm trying to write a relatively trivial (or so I thought) program
that does IO which takes a file containing a newline separated list of
decimal numbers and outputs the largest one.

I guess if I validate the input (and rule out numbers longer than an
arbitrary number of digits) and postulate that the file is of bounded
size, I could do it.

Any advice?

On Fri, Feb 17, 2012 at 9:53 AM, Alex Rozenshteyn <rpglover64 at gmail.com> wrote:
> Thank you!
>
> On Fri, Feb 17, 2012 at 8:09 AM, Nils Anders Danielsson <nad at chalmers.se> wrote:
>> On 2012-02-17 13:50, Alex Rozenshteyn wrote:
>>>
>>>   split : {A : Set} → (A → Bool) → Colist A → Colist (Colist A)
>>>   split f [] = [ [] ]
>>>   split f (x ∷ xs') with  ♭ xs' | f x
>>>   ... | xs | true  = addToListOfLists x (split f xs)
>>>   ... | xs | false = split f xs
>>
>>
>> This definition is not productive: split (λ _ → false) (repeat unit)
>> does not produce any output.
>>
>> Section 2 of the following paper contains an introduction to coinduction
>> and corecursion in Agda:
>>
>>  Subtyping, Declaratively
>>  An Exercise in Mixed Induction and Coinduction
>>  Myself and Thorsten Altenkirch
>>  http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-subtyping.html
>>
>> --
>> /NAD
>>
>
>
>
> --
>           Alex R



-- 
          Alex R