Re: [isabelle] Lazy Lists in HOL



The files LList.thy and SList.thy represent experiments in the development of datatypes. Because HOL does not offer a domain theory, lazy lists are defined using corecursion, which derives from the category-theoretic notion of finality.

The idea of corecursion is that you do a certain amount of computation and then return either
  * None: the result is the empty list
* Some(x,z): the result begins with x, and remaining elements can be obtained using corecursion with the value z.

Zip should be easy to define corecursively, but filter is tricky because an unlimited computation may be necessary to obtain the next element.

My paper "Mechanizing coinduction and corecursion in higher-order logic" may be helpful:
<http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-304.html>

Larry Paulson


On 18 Mar 2007, at 12:02, Thomas Göthel wrote:

I wanted to use the LazyList - theory of HOL (LList.thy) from Lawrence
Paulson. Unfortunately I didn't find a theory containing the typical
higher-order functions like filter, zip, etc for "'a llist". Furthermore I miss a predicate like is_finite for checking finiteness of a lazy list. Is
there such an additional theory or do I have to define these functions
myself?
Maybe it is possible to use the definitions of SList.thy, does anybody know
how?






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