[Agda] Termination checking on coinduction
Alex Rozenshteyn
rpglover64 at gmail.com
Sat Feb 18 00:03:52 CET 2012
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
More information about the Agda
mailing list