[isabelle] Formalisations of infinite streams
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Formalisations of infinite streams
- From: Andreas Lochbihler <andreas.lochbihler at kit.edu>
- Date: Wed, 13 Jun 2012 16:36:09 +0200
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:188.8.131.52) Gecko/20120216 Thunderbird/3.1.19
there is a growing number of formalisations of infinite streams in the Archive
of Formal Proofs. I am aware of the following, but I guess there might be even
more hidden in other entries:
1. David Trachtenherz' entry Infinite Lists develops a stream view on the type
"nat => 'a". It tries to reuse as many standard operations on functions as
possible for the list operations. For example, List.map corresponds to "op o",
List.set to range. Additionally, he defines the sum type of finite and infinite
lists called generalised lists.
2. Stefan Friedrich's entry Lazy List II develops finite and infinite lists over
a given alphabet based on coinductive lists from the entry Coinductive.
3. Peter Gammie recently defined coinductive streams as a codatatype which I
have now added to Coinductive in the development AFP. Support for operations on
streams is still quite limited.
4. Stephan Merz' entry Stuttering Equivalence models infinite strings as
functions "nat => 'a" and defines a suffix operation.
Since there is considerable redundancy, I wonder whether and how we should unify
these developments. Some questions are:
- Should we have a type of its own ('a stream) or operations on functions (nat
=> 'a) or both versions?
- Should we do equality proofs by coinduction or induction on all indices?
- Should we provide any of these versions as part of the Isabelle library such
that there is an "official" version to be used in future developments?
- Should/can we rework the existing formalisations to use the new one?
- If yes: Can we somehow estimate the required effort?
I'll be happy to help in consolidating all this. However, at the moment, I
cannot estimate at the moment how much of the AFP and the theories in the wild
depend on these formalisations.
Karlsruher Institut für Technologie
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and