Re: [isabelle] Lazy Lists



On 06/25/2012 01:21 PM, Peter Gammie wrote:
Christian,

(We could have this conversation on the list if you like - just post any followup there.)

On 25/06/2012, at 2:10 PM, Christian Sternagel wrote:

thanks for the pointer to HOLCF. Assuming code generation works (almost) as usual for HOLCF, this is indeed what I was looking for.

AFAIK the code generator does not work at all for HOLCF.
If that is the case, it would be interesting to know whether this is an inherent restriction or would "just" require more work (I know by painful experience that such "just"s can get quite huge ;)).

I would love to be able to formalize functions as is done in lazy functional programming papers and get generated code "for free".

PS: I wanted to download your paper on the worker/wrapper transformation from your website, but the file seems to be damaged (at least that's what two of my pdf reader applications are claiming).

Oops, thanks for that.

I'd recommend you scrape the theory out of the AFP - it subsumes the JFP paper.
Good to know, thanks.

BTW this transformation should apply to other inductively-defined things, e.g. inductive definitions in HOL.

However I have not investigated how you'd connect an inductive thing (e.g. a function nat => 'a) to it's coinductive counterpart (e.g. an 'a llist) using it. (It works in a domain theoretic setting as recursive domain equations have unique fixed points.)
I guess this is the same problem as relating "'a list" to "'a llist"?

There's some work on this by Thorsten Altenkirch et al that is heavy on the category theory (TLCA 2001?) - I think the keyword is "containers". See the original worker/wrapper paper by Hutton and Gill for the reference.

cheers

chris





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.