Re: [isabelle] Lazy Lists


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.


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