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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to