Email Gateway (Aug 18 2022 at 17:57): Email Gateway (Aug 18 2022 at 17:57):From: Peter Gammie <peteg42@gmail.com>
Hello,
Recently I've been in need of a theory of complete lattices.
There are two on offer:
This look really polished but uses a type class hierarchy distinct from the rest of the HOL image.
It includes a type for dual orders, which I need.
These use the standard HOL type classes. There are lots of proofs of dual results but no "dual" type constructor. Also the syntax for lattices gets nuked at the end of the development.
In both cases there is no support for product lattices, which is straightforward to add.
I am sure there are more differences than just these.
I also note that there is another definition of partial orders (etc) in HOLCF, and probably elsewhere.
Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth?
More generally, is there (or should there be) a bug/feature/wishlist tracker for Isabelle for these sorts of things? It might help reduce parallel developments, or least clarify what their relative strengths are.
cheers
peter
Email Gateway (Aug 18 2022 at 17:58):From: Brian Huffman <brianh@cs.pdx.edu>
Why don't you just start one yourself? I don't think it matters too
much who hosts it, as long as we can get enough people use it. I would
definitely use it.
Email Gateway (Aug 18 2022 at 17:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
first of all, HOL-Lattice is more an example than a library. I would
guess that the lattice in HOL-Algebra is what you want to start an. The
order development in HOLCF is traditionally something specific apart.
Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth?
Well, there has been a lots of effort to reduce the number of lattice
developments to effectively two. For the background, I quote here from
an e-mail from isabelle-dev:
a few years
ago, around 2006, when I entered this type class adventure in more deep,
I came to the conclusion that it is usually better to have
»constructive« type classes, e.g. if we specify a semilattice as type
class, we don't assume »there exists a inf such that …« but we add an
explicit parameter »inf« which a corresponding set of properties.Otherwise we would define »inf« with »THE x. …«, and this means that for
particular instances of lattices (sets, nats, …) you have to derive
type-specific primitive rules (e.g. inf on 0/Suc representation, inf on
{}/insert representation) manually starting with a »THE x. …«
definition. In practice, it is much more straightforward to define inf
on particular types directly and then prove that this instance conforms
to its axiomatic specification. As a side effect, you get reasonable
code equations, something which can hardly be achieved if inf would be a
generic polymorphic operation rather than a class parameter.Of course, these constructive type classes are more specific than the
mathematical concept they represent, but for meta-theory a
record/locale-based approach with explicit carrier sets as in
HOL-Algebra is much more feasible anyway. But see also the funny lemma
http://isabelle.in.tum.de/repos/isabelle/file/7270ae921cf2/src/HOL/Lattices.thy#l447
which shows how even the contructive type classes are able to talk about
uniqueness.
Cheers,
Florian
--
PGP available:
http://www.haftmann-online.de/florian/florian_at_haftmann_online_de
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Email Gateway (Aug 18 2022 at 17:59):From: Peter Gammie <peteg42@gmail.com>
Florian,
On 29/07/2011, at 3:58 PM, Florian Haftmann wrote:
first of all, HOL-Lattice is more an example than a library. I would
guess that the lattice in HOL-Algebra is what you want to start an.
OK. This being the case, could (/should) it be moved from the top-level, to e.g. HOL/Library/ or ex/, or maybe Proofs/?
On a related note, HOL/Library/ is a zoo. Would it be reasonable to introduce more structure there, ala Haskell's hierarchical libraries? How about the stuff in the top-level HOL/ directory?
The order development in HOLCF is traditionally something specific apart.
Indeed it was an entirely separate Isabelle logic (built on top of HOL), but Brian's recent work has made HOLCF a HOL library. It provides convenient ways of making recursive definitions over PCPOs that strike me as useful for doing the same thing over complete lattices.
Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth?
Well, there has been a lots of effort to reduce the number of lattice
developments to effectively two. For the background, I quote here from
an e-mail from isabelle-dev:<...>
Thanks for that. I am using the lattice theory in HOL/ (Complete_Lattice and friends) which is quite pleasant.
cheers
peter
Email Gateway (Aug 18 2022 at 17:59):From: Alexander Krauss <krauss@in.tum.de>
See also this thread on isabelle-dev from 2009:
http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.devel/793
We do indeed have a number of long-standing issues, which may be worth
documenting more formally, to make it easier for people to learn about
the deeper reasons behind them. But this won't make them go away sooner,
as most of them are due to conceptual problems in the interactions of
different parts of the system. As a consequence, the "report -> analyze
-> fix" cycle often takes many years.
btw: The original claim, that a tracker would help reduce parallel
developments is unclear to me.
Alex
Email Gateway (Aug 18 2022 at 18:11):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
OK. This being the case, could (/should) it be moved from the top-level, to e.g. HOL/Library/ or ex/, or maybe Proofs/?
here there are two misunderstandings mixed together:
a) Basically, everything inside HOL/ can be considered a library as long
it is a suitable development to build upon, be it HOL-Algebra or
HOL-Imperative_HOL. Typically the developer of a (let's call it)
extension is able to tell you whether it can suit your purpose.
b) Proofs/ is not a directory, it is a particular image of the HOL
session run with proof terms.
On a related note, HOL/Library/ is a zoo. Would it be reasonable to
introduce more structure there, ala Haskell's hierarchical libraries?
It would surely, but we have no hierarchical theory name space (yet).
Indeed it was an entirely separate Isabelle logic (built on top of HOL), but Brian's recent work has made HOLCF a HOL library. It provides convenient ways of making recursive definitions over PCPOs that strike me as useful for doing the same thing over complete lattices.
I dimly remember that once Brian and I discussed whether some ordering
stuff could be shared here, but AFAIR the major obstacle was that HOL
orderings have an explicit strict part <, which seems to be inconvenient
for HOLCF.
Hope this helps,
Florian
signature.asc
Last updated: Apr 24 2024 at 12:33 UTC