Re: [isabelle] Formalisations of infinite streams
On 06/13/2012 04:36 PM, Andreas Lochbihler wrote:
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
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
- 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
- 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.
some thoughts here from Munich:
- Having dedicated type "'a stream" for functions (nat => 'a) has
similar benefits and drawbacks as the set/'a => bool distinction. Alex
Krauss sent a nice summary (Summary: WHY have 'a set back?) on
isabelle-dev about a year ago. Creating a new type has been recently
simplified by the lift_definition command and transfer method.
- Dmitriy Traytel and Andrej Popescu are developing a codatatype
package, which might be useful for your work. (The package will be done
in "two weeks".)
This archive was generated by a fusion of
Pipermail (Mailman edition) and