*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Formalisations of infinite streams*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Wed, 13 Jun 2012 17:36:51 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FD8A559.6040905@kit.edu>*References*: <4FD8A559.6040905@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

On 06/13/2012 04:36 PM, Andreas Lochbihler wrote:

Dear all,there is a growing number of formalisations of infinite streams in theArchive of Formal Proofs. I am aware of the following, but I guessthere might be even more hidden in other entries:1. David Trachtenherz' entry Infinite Lists develops a stream view onthe type "nat => 'a". It tries to reuse as many standard operations onfunctions as possible for the list operations. For example, List.mapcorresponds to "op o", List.set to range. Additionally, he defines thesum type of finite and infinite lists called generalised lists.2. Stefan Friedrich's entry Lazy List II develops finite and infinitelists over a given alphabet based on coinductive lists from the entryCoinductive.3. Peter Gammie recently defined coinductive streams as a codatatypewhich I have now added to Coinductive in the development AFP. Supportfor operations on streams is still quite limited.4. Stephan Merz' entry Stuttering Equivalence models infinite stringsas functions "nat => 'a" and defines a suffix operation.Since there is considerable redundancy, I wonder whether and how weshould unify these developments. Some questions are:- Should we have a type of its own ('a stream) or operations onfunctions (nat => 'a) or both versions?- Should we do equality proofs by coinduction or induction on allindices?- Should we provide any of these versions as part of the Isabellelibrary such that there is an "official" version to be used in futuredevelopments?- 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 themoment, I cannot estimate at the moment how much of the AFP and thetheories in the wild depend on these formalisations.Any opinions?

Hi Andreas, some thoughts here from Munich:

Lukas

**References**:**[isabelle] Formalisations of infinite streams***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Unexpected assumptions in nested contexts
- Next by Date: Re: [isabelle] Formalisations of infinite streams
- Previous by Thread: Re: [isabelle] Formalisations of infinite streams
- Next by Thread: Re: [isabelle] Formalisations of infinite streams
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list