Email Gateway (Aug 18 2022 at 17:07): Email Gateway (Aug 18 2022 at 17:07):From: David Trachtenherz <trachten@in.tum.de>
An additional remark on infinite lists in my entry: I designed them very
pragmatically; the definitions and lemmas are named similar to those for
finite lists and also work similar, also w. r. t. lemmas added to the
simpset. Some lemmas work even simpler because infinite lists naturally
don't need assumptions of the form "i < length xs" or "length xs =
length ys". So I do hope that everybody used to work with finite lists
will also be comfortable with this formalization of infinite lists.
Additionally, the relation and transition between infinite and finite
lists is very direct: truncating an infinite list returns a finite list,
appending an infinite list to a finite list returns an infinite list,
and finite lists can also be prefixes of infinite lists. (For example, I
used this direct relation in my other entry, AutoFocus-Stream, which
formalizes AutoFocus stream processing: the computation of an AutoFocus
component/model/system is an infinite stream of results delivered for an
infinite stream of input messages, represented by infinite lists; this
way we can reason about AutoFocus computations. When truncating the
infinite input stream/list, we obtain a finite input stream, represented
by a finite list, and can not only reason about the resulting finite
computation, but also operationally simulate it using the Isabelle
evaluation function "value" with the finite input stream/list.)
David
Andreas Lochbihler wrote:
Email Gateway (Aug 18 2022 at 17:07):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear David,
my point was not to criticize your work. I merely wanted to point out that at
present, any user has to buy into one of the three versions. Switching from one
to the other might be difficult because of the small differences, in particular
different names for constants and lemmas and types of constants. Like you, I
have tried to stay close to HOL/List for Coinductive, too. In fact, many
definitions of yours and mine are equivalent. So I wondered whether there is any
interest in combining the formalisations into one - and how that would be done.
Andreas
David Trachtenherz schrieb:
An additional remark on infinite lists in my entry: I designed them very
pragmatically; the definitions and lemmas are named similar to those for
finite lists and also work similar, also w. r. t. lemmas added to the
simpset. Some lemmas work even simpler because infinite lists naturally
don't need assumptions of the form "i < length xs" or "length xs =
length ys". So I do hope that everybody used to work with finite lists
will also be comfortable with this formalization of infinite lists.[...]
David
Email Gateway (Aug 18 2022 at 17:08):From: David Trachtenherz <trachten@in.tum.de>
Dear Andreas,
I merely wanted to point out that at present, any user has to buy into
one of the three versions.
This is why I've written the previous mail. I just wanted to point out
the options provided (and not provided) in my version of infinite lists
in the ListInf theory, and why I've made the infinite lists like this.
What I wanted to do was embedding infinite lists into the already
available frame of the finite list theory, in fact I didn't even
introduce new data types for infinite lists but just operator
definitions and/or abbreviations (especially: types 'a ilist = "nat =>
'a"); the only new data type was the one for generalized lists capable
of taking both finite and infinite lists (datatype 'a glist = FL "'a
list" | IL "'a ilist").
As far as I've understood from a first glimpse at your theory (so,
please correct me where necessary) you went the way of defining the new
data type llist suitable for both finite and infinite lists, and using
conversion operators between "standard" finite lists and llist.
Therefore, I see some (limited) similarity between llist and glist in my
ListInf, as glist is the only new data type in ListInf and takes both
finite and infinite lists; notably I have defined it first of all for
the sake of completeness; in fact I used only the pure finite and
infinite lists in my other theories (also in the unpublished ones). So
if I get it right, you have established an elaborate framework for the
llist data type with special attention to coinduction, while I have
(intentionally) taken the way of making as few as possible new data type
definitions and rather adding operations and/or lemmas for interpreting
functions "nat => 'a" as infinite lists in a manner making there usage
as similar as possible to finite lists.
Moreover, both Coinductive and Infinite Lists contain additions to
Nat_Infinity in HOL/Library (theories Coinductive_Nat and Util_NatInf,
resp.). Interestingly, both of them instantiate the type class minus
for inat in exactly same way. Alas, no Isabelle session can import
both because that type classes can be instantiated only once. As
Util_NatInf's setup for arithmetic is more elaborate than
Coinductive_Nat's, I suggest to move this to Nat_Infinity in
Isabelle's library. Is there anyone using Nat_Infinity with other type
class instantiations, which would break then?
It would be a pity if the instantiation of the type class minus would
prevent using both theories simultaneously, because I see absolutely no
reason why not employing both where useful. If the Isabelle developers
team would opt for moving any of the theories from List-Infinite (be it
concerning arithmetics, sets, or anything else) to the Isabelle Library,
no matter whether partially, fully and/or adjusted, I certainly wouldn't
mind.
David
Andreas Lochbihler wrote:
Dear David,
I merely wanted to point out that at present, any user has to buy
into one of the three versions. Switching from one to the other might
be difficult because of the small differences, in particular
different names for constants and lemmas and types of constants. Like
you, I have tried to stay close to HOL/List for Coinductive, too. In
fact, many definitions of yours and mine are equivalent. So I
wondered whether there is any interest in combining the
formalisations into one - and how that would be done.Andreas
David Trachtenherz schrieb:
An additional remark on infinite lists in my entry: I designed them
very pragmatically; the definitions and lemmas are named similar to
those for finite lists and also work similar, also w. r. t. lemmas
added to the simpset. Some lemmas work even simpler because infinite
lists naturally don't need assumptions of the form "i < length xs"
or "length xs = length ys". So I do hope that everybody used to work
with finite lists will also be comfortable with this formalization
of infinite lists.Additionally, the relation and transition between infinite and
finite lists is very direct: truncating an infinite list returns a
finite list, appending an infinite list to a finite list returns an
infinite list, and finite lists can also be prefixes of infinite
lists. (For example, I used this direct relation in my other entry,
AutoFocus-Stream, which formalizes AutoFocus stream processing: the
computation of an AutoFocus component/model/system is an infinite
stream of results delivered for an infinite stream of input
messages, represented by infinite lists; this way we can reason
about AutoFocus computations. When truncating the infinite input
stream/list, we obtain a finite input stream, represented by a
finite list, and can not only reason about the resulting finite
computation, but also operationally simulate it using the Isabelle
evaluation function "value" with the finite input stream/list.)David
Andreas Lochbihler wrote:
It's great to see that people are working with infinite data
structures.
However, there are now three different formalisations of (possibly)
infinite lists in the AFP: Lazy Lists II by Stefan Friedrich,
Infinite Lists by David Trachtenherz and Coinductive by myself. At
present, they are pairwise incompatible, and each of them has a
different focus: Lazy Lists II focuses on lists over alphabets,
Infinite Lists on infinite lists, and Coinductive on coinductive
definitions and proofs.
I think it would be great if there was just one theory similar to
HOL/List that unified these three as far as possible such that
future users do not have to pick one (or reinvent their own) and
relinquish the other developments.Moreover, both Coinductive and Infinite Lists contain additions to
Nat_Infinity in HOL/Library (theories Coinductive_Nat and
Util_NatInf, resp.). Interestingly, both of them instantiate the
type class minus for inat in exactly same way. Alas, no Isabelle
session can import both because that type classes can be
instantiated only once. As Util_NatInf's setup for arithmetic is
more elaborate than Coinductive_Nat's, I suggest to move this to
Nat_Infinity in Isabelle's library. Is there anyone using
Nat_Infinity with other type class instantiations, which would
break then?Andreas
Last updated: Nov 21 2024 at 12:39 UTC