Email Gateway (Aug 18 2022 at 10:20): Email Gateway (Aug 18 2022 at 10:20):From: Thomas Göthel <tgoethel@cs.tu-berlin.de>
Hello,
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?
Bye,
Thomas
Email Gateway (Aug 18 2022 at 10:20):From: Alexander Krauss <krauss@in.tum.de>
Thomas,
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?
Unfortunately, the theory of lazy lists is not so well developed, so you
have to define the concepts you need yourself.
You might also want to look at the "Lazy Lists II" theory in the Archive
of Formal Proofs (http://afp.sourceforge.net) by Stefan Friedrich, which
might contain some of the definitions you need.
Maybe it is possible to use the definitions of SList.thy, does anybody know
how?
No. Strict and lazy lists are different types, and there is no easy way
to lift definitions. You can of course take the "SList.thy" as a
guideline, but the definition principles on lazy lists are very
different (corecursion vs. recursion) and not automated very well at the
moment. Notably, you must use the "llist_corec" combinator, as in the
definitions of "lmap", "lappend" etc.
Should you decide to extend the available theories with more generally
useful definitions and theorems, your contribution is welcome of course...
Alex
Email Gateway (Aug 18 2022 at 10:20):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: May 03 2024 at 12:27 UTC