Re: [isabelle] Lazy Lists
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] Lazy Lists
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Mon, 25 Jun 2012 13:45:59 +0900
- In-reply-to: <37C404CC-2BF2-4ACD-88CE-204046C23389@gmail.com>
- References: <4FE7D8D3.email@example.com> <77CDDEB7-20B7-41DB-9F18-0943AC91888B@gmail.com> <4FE7E49A.firstname.lastname@example.org> <37C404CC-2BF2-4ACD-88CE-204046C23389@gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:13.0) Gecko/20120615 Thunderbird/13.0.1
On 06/25/2012 01:21 PM, Peter Gammie wrote:
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 ;)).
(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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and