[isabelle-dev] Of lazy lists and friendly corecs

[Andreas Lochbihler]

Hi Manuel,

a function is friendly if it produces at least one constructor after applying at most one 
constructor to the codatatype argument. This does not have anything to do with primitive 
corecursion, because the codatatype result type need not be a argument type---and even if 
it is, there are primcorec functions which are not friendly, e.g.,

primcorec odds :: "'a stream => 'a stream"
where "odds xs = SCons (shd xs) (odds (stl (stl xs)))"

I leave it to Dmitriy and Jasmin to reply to your problem with the error message about 
lmerge. But in theory this should work (and in fact I've already done it for streams).

 > 1. Something like "if lnull xs then ys" works in primcorec, but in corec and
 > friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl ys)". Is that a known
 > limitation?
Yes, this is known to us, but we currently don't have the time to implement all the 
preprocessing features of primcorec for friend_of_corec.

Best,
Andreas

On 07/10/16 14:22, Manuel Eberl wrote:
> Hallo,
>
> I've been playing around with corec and friends in combination with the lazy lists from
> "$AFP/Coinductive/Coinductive_List" and encountered the following problem:
>
> Suppose I want a function that takes two (implicitly sorted) lazy lists and merges them in
> the following fashion:
>
> primcorec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
>   "lmerge xs ys = (if lnull xs then ys
>                    else if lnull ys then xs
>                    else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) ys)
>                    else LCons (lhd ys) (lmerge xs (ltl ys)))"
>
> I've still not fully understood what ‘friendly’ means, but I should be very surprised if
> this function were not friendly. So I tried this:
>
> friend_of_corec lmerge where
>   "lmerge xs ys = (if lnull xs ∧ lnull ys then LNil
>                    else if lnull xs then LCons (lhd ys) (ltl ys)
>                    else if lnull ys then LCons (lhd xs) (ltl xs)
>                    else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) ys)
>                    else LCons (lhd ys) (lmerge xs (ltl ys)))"
>
> Unfortunately, I get the following error:
>
> exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant
> "Coinductive_List.llist.LNil" :: 'b
>
> I now have the following questions:
> 1. Something like "if lnull xs then ys" works in primcorec, but in corec and
> friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl ys)". Is that a known
> limitation?
> 2. What is the relationship between primcorec and friendliness? If I have a function
> defined by primcorec, is the additional step with friend_of_corec fundamentally necessary
> or is that just a technical issue? (I would have naïvely assumed that
> primitively-corecursive functions are always friendly or something like that)
> 3. What causes the above error and how do I get around it?
>
>
> Cheers,
>
> Manuel
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>