Re: [isabelle] Formalisations of infinite streams



On 6/13/12, Andreas Lochbihler <andreas.lochbihler at kit.edu> wrote:
> 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?

I wholeheartedly support the idea of infinite stream unification and
the ideas of the stream type and its potential eventual inclusion into
the "official" Isabelle distribution. It of course makes sense then to
adapt the existing AFP formalizations to use the unified type (and
operators). I support this is because I am working on formalization of
my Forensic Lucid language, which is based on Lucid where the
variables are in general infinite multidimensional streams. I will be
on the lookout of any developments, and contribute if time permits as
well.

(I however have no idea at the moment on the effort required for the
above proposal.)

-s





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