Email Gateway (Aug 18 2022 at 20:23): Email Gateway (Aug 18 2022 at 20:23):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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:
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.
Stefan Friedrich's entry Lazy List II develops finite and infinite lists over
a given alphabet based on coinductive lists from the entry Coinductive.
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.
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?
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
Email Gateway (Aug 18 2022 at 20:23):From: Serguei Mokhov <serguei@gmail.com>
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
Email Gateway (Aug 18 2022 at 20:24):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Andreas,
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".)
Lukas
Email Gateway (Aug 18 2022 at 20:24):From: Tobias Nipkow <nipkow@in.tum.de>
I strongly believe that different coinductive formalizations should be unified,
if that's what they need. As much of it as possible should be in one place, and
the AFP is the right place for larger libraries. We could mark some entries as
"subsumed by ..." afterwards.
I would not try and unify the two models (coinductive and nat => 'a), they
have their own advantages and disadvantages. Nor would I unify different entries
using the nat => 'a model: that should be driven by some application, rather
than proactively.
Tobias
Email Gateway (Aug 18 2022 at 20:24):From: Peter Gammie <peteg42@gmail.com>
Just to clarify: I found myself in need of a plausible coinductive stream type and adapted the LList formulation in the Coinductive development in the AFP.
Concretely I could have gotten away with nat => 'a, but hoped the coinductive formulation would be more convincing to people versed in type theory.
cheers
peter
Last updated: Nov 21 2024 at 12:39 UTC