Email Gateway (Aug 18 2022 at 17:06): Email Gateway (Aug 18 2022 at 17:06):From: Tobias Nipkow <nipkow@in.tum.de>
David Trachtenherz has contributed 3 new entries:
Infinite Lists
We introduce a theory of infinite lists in HOL formalized as functions
over naturals.
http://afp.sourceforge.net/entries/List-Infinite.shtml
Interval Temporal Logic on Natural Numbers
We introduce a theory of temporal logic operators using sets of natural
numbers as time domain, formalized in a shallow embedding manner.
http://afp.sourceforge.net/entries/Nat-Interval-Logic.shtml
AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
We formalize the AutoFocus Semantics (a time-synchronous subset of the
Focus formalism) as stream processing functions on finite and infinite
message streams represented as finite/infinite lists.
http://afp.sourceforge.net/entries/AutoFocus-Stream.shtml
Email Gateway (Aug 18 2022 at 17:07):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 17:08):From: John Matthews <matthews@galois.com>
I think there should be two standard theories here: one for "infinite only" lists, and one for "possibly infinite" (i.e. coinductive) lists. Infinite-only lists are more limited, but easier to reason about. There is a direct analogy here with having different theories for sets versus multisets.
-john
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC