# [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:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Dear all,

`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.
`
Any opinions?
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`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
MHonArc.*