*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] Lazy Lists*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Mon, 25 Jun 2012 15:09:08 +1000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FE7ED07.7090706@jaist.ac.jp>*References*: <4FE7D8D3.2070104@jaist.ac.jp> <77CDDEB7-20B7-41DB-9F18-0943AC91888B@gmail.com> <4FE7E49A.3070507@jaist.ac.jp> <37C404CC-2BF2-4ACD-88CE-204046C23389@gmail.com> <4FE7ED07.7090706@jaist.ac.jp>

Christian, On 25/06/2012, at 2:45 PM, Christian Sternagel wrote: >> 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"? Probably. Roughly I think Altenkirch et al show that if you have a function from an inductively-defined domain then there is an equivalent coinductive definition of that function. You can think of it as a generalisation of using lazy lists to memoise functions from the natural numbers, as Hutton and Gill did in their worker/wrapper paper. In their setting, for (partial) f :: nat -> 'a, f x is memoised by the x'th element of the lazy list. (In a total setting you'd want to use streams, not lazy lists.) In general you need to index into a more complex coinductive type (whose structure depends on the type of the function's domain). There's probably a link to differentiating datatypes, zippers and so forth too. Their framework probably handles the issue in the paper I mentioned earlier. BTW I think it is great you are contemplating putting Bird et al's work through a proof assistant. Parts of Bird's theory of lists (from circa 1987) are still visible in List.thy. One might hope the newer work is similarly useful. I'll leave the questions about code generation to Brian and Florian. cheers peter

**References**:**[isabelle] Lazy Lists***From:*Christian Sternagel

**Re: [isabelle] Lazy Lists***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Lazy Lists
- Next by Date: Re: [isabelle] Trying to rename Lattices.thy
- Previous by Thread: Re: [isabelle] Lazy Lists
- Next by Thread: Re: [isabelle] Lazy Lists
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list