Email Gateway (Aug 22 2022 at 19:25): Email Gateway (Aug 22 2022 at 19:25):From: Akihisa Yamada <ayamada@trs.cm.is.nagoya-u.ac.jp>
Hello,
E.g., monoid_mult (type class, in HOL) vs. monoid (locale, in
HOL-Algebra). The classes have the advantage of being easier to use than
locales in many cases (at least I feel that way), but they have the
limitation of always having UNIV as the carrier.
(I had asked this question long ago here, though.) I had tried to unify
them, but gave up due to a locale behavior that I don't understand.
My approach was defining locales with a predicate for carrier, like
locale magma =
fixes f (infixl "❙*" 70) and member
assumes closed: "⋀a b. member a ⟹ member b ⟹ member (a ❙* b)"
By instantiating member by "λx. True", and simplifying "True ⟹" away we
get unrestricted statements. However, after
interpretation mult: magma where member = "λx. True" and f = "( * )"
rewrites "⋀P. (True ⟹ PROP P) ≡ PROP P"
by (unfold_locales, simp_all)
mult.closed is still "True ⟹ True ⟹ True" not "True".
I'm happy to contribute my code and some work if someone can make this
rewrites work.
Best,
Akihisa
As far as I know, all proofs are simply done twice. And someone building
a development on these things needs to pick on approach and is then
"locked in", which is problematic, since some material is only available
in the HOL approach and some only in the HOL-Algebra approach.In case of an overhaul, perhaps these concepts could be unified as well?
I am not sure what the best approach is for such a unification, but some
idea would be:* Have compatible names as far as possible. E.g., if the class is
called XXX, then the locale is called l_XXX or something.
* Have the possibility to transfer theorems between compatible classes
and locales. (Compatible means: when the class is the locale with
carrier:=UNIV.)
o For transferring from locale to class, that might work
automatically (haven't checked) if we prove "sublocale XXX <=
l_XXX UNIV".
o For transferring from class to locale it more difficult.
Possibly something involving the Types_To_Sets tools might work?Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.What if instead of editing HOL-Algebra, a new session HOL-Algebra2 is
created? And then deprecating HOL-Algebra. (Or even renaming HOL-Algebra
to HOL-Algebra-Old.)Then it will be optional to update old AFP material building on
HOL-Algebra.I also don't think there are any "heavy" users of HOL-Algebra these days
I wonder whether that might partially be because of the incompatibility
with the type-class approach. (I, at least, never look at HOL-Algebra
because we are building on real_vector_space in our formalizations and
thus "locked in".)Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,
There is the additional problem that there is a lot of duplication of
concepts, using classes vs locales.E.g., monoid_mult (type class, in HOL) vs. monoid (locale, in
HOL-Algebra). The classes have the advantage of being easier to use than
locales in many cases (at least I feel that way), but they have the
limitation of always having UNIV as the carrier.As far as I know, all proofs are simply done twice. And someone building
a development on these things needs to pick on approach and is then
"locked in", which is problematic, since some material is only available
in the HOL approach and some only in the HOL-Algebra approach.In case of an overhaul, perhaps these concepts could be unified as well?
I do not say that this is not possible, but IMHO there are too many open
questions to tackle that on one step; the existing algebraic type class
hierarchy is essential for the HOL bootstrap e.g. wrt. numeric types
without subtyping. Personally I got used to view the class / locale
dichotomy (which carries over to the sessions distinctive HOL-Algebra
and HOL-Computational_Algebra) as an inherent consequence of Isabelle's
higher-order logic »as it is«.
Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.What if instead of editing HOL-Algebra, a new session HOL-Algebra2 is
created? And then deprecating HOL-Algebra. (Or even renaming HOL-Algebra
to HOL-Algebra-Old.)Then it will be optional to update old AFP material building on
HOL-Algebra.
There is some danger to reproduce the situation with
(Old/New)_Number_Theory as it was from 2009 until 2016.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:26):From: Dominique Unruh <unruh@ut.ee>
I was not suggesting to remove the type classes. In fact, I believe that
they are much easier to use. What I was suggesting is much less
ambitous: If HOL-Algebra is overhauled, make sure the locales stand in
1-1 correspondence with the classes. I agree with you that the dichotomy
is necessary, but what isn't necessary but rather historical is that,
e.g., naming conventions are incompatible. (Purely a usability issue,
not a mathematical consideration.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:40):From: Lawrence Paulson <lp15@cam.ac.uk>
A notable peculiarity of Algebra is its locale abelian_group, which is based on comm_group (groups with commutative multiplication) but with the weird twist of requiring a ring; it appears to be, in reality, the specification that a ring’s addition operator is commutative. Except that all rings have this property, and the very existence of this locale is confusing. Does anybody know any more about this?
Larry
record 'a ring = "'a monoid" +
zero :: 'a ("𝟬ı")
add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)
abbreviation
add_monoid :: "('a, 'm) ring_scheme ⇒ ('a, 'm) monoid_scheme"
where "add_monoid R ≡ ⦇ carrier = carrier R, mult = add R, one = zero R, … = (undefined :: 'm) ⦈"
locale abelian_monoid =
fixes G (structure)
assumes a_comm_monoid:
"comm_monoid (add_monoid G)"
locale abelian_group = abelian_monoid +
assumes a_comm_group:
"comm_group (add_monoid G)"
Email Gateway (Aug 22 2022 at 19:40):From: Manuel Eberl <eberlm@in.tum.de>
HOL-Algebra is a bit messy. A big part of that, I think, comes from
quirks of Isabelle/HOL itself.
My guess would be that one can write groups either additively (G, +, 0)
or multiplicatively (G, *, 1). Of course, more abstract syntax (G, ∘, e)
is also possible. There are various conventions about when to use which
notation – in particular, I think the convention is that if you use "+",
the group is always commutative (i.e. abelian).
In HOL-Algebra, groups are /always/ written multiplicatively. There is
no other way. When you have a ring, you can write "+" for addition, but
that is not formally associated to any group. The additive group of the
ring has all its properties stated w.r.t. the "*" of "add_monoid R".
"abelian_group" is apparently some kind of attempt to have an abelian
group that is written additively. Due to the fact that the "+" operator
is defined for the ring record, this requires us to use a ring record
even though there is (in general) no multiplication operation. We also
don't have any locale assumption that this "ring record" is an actual
ring (i.e. fulfils the ring axioms). Just the addition operation in it
is required to form an abelian group.
As for why this strange "abelian_group" locale exists, I cannot say. One
would have to examine where it is used and what for.
I agree that it's all very confusing. Maybe it is simply the case that
this ad-hoc "single-inheritance record" "locale with structure
parameters" is just fraught with problems. But as far as I know, it's
the only way we have in Isabelle to do abstract algebra, and I don't
know of a better one. Unless we can find a way to emulate the more
modular typeclass/implicit parameter approach and elaborators that
systems like Coq and Lean have.
Manuel
Email Gateway (Aug 22 2022 at 19:40):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Larry,
when reading HOL-Algebra you need to keep in mind that much of the
material pre-dates modern locales. Then locales were not based on local
theories, and expressions were limited to renaming; instantiation and
rewriting were unavailable.
The approach of combining locales with records dates back to that time.
Definitions in locales were unavailable, and the solution was to extract
the signature part of an algebraic structure into a record, on which
definitions could be made globally. Locales would only deal with the
specification part.
Regarding the locale abelian_group: an abelian group by convention is a
commutative group with additive notation. A ring then is a
(multiplicative) monoid and an abelian group. What you see is an
attempt of expressing that. Unfortunately, since there isn't multiple
inheritance for records, I needed to resort to using the ring record
also for abelian groups, which is, of course, awkward.
Clemens
Email Gateway (Aug 22 2022 at 19:40):From: Manuel Eberl <eberlm@in.tum.de>
Hello Clemens,
that's interesting. It would certainly be of interest to think of a
large-scale overhaul of HOL-Algebra using modern locale features.
Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.
I also don't think there are any "heavy" users of HOL-Algebra these days
who could champion such an endeavour and come up with better designs. If
there are – please come forward! (Larry had two students who might
actually be the two heaviest recent users.
I've used HOL-Algebra sporadically over the last two years or so and
would like to see it improved. Unfortunately, I do not have the time to
do that myself in the foreseeable future, and I also don't think I am an
ideal candidate to do it considering my lack of expertise with
HOL-Algebra and locales.
Manuel
Email Gateway (Aug 22 2022 at 19:40):From: Slawomir Kolodynski via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Manuel,
as far as I know, it's the only way we have in Isabelle to do abstract algebra
I assume you mean Isabelle/HOL here.
In IsarMathLib notation details are deferred to the presentation layer so they are not tied to definitions. Multiplicative notation happens to be used in context of semigroups, groups and abelian groups, while additive notation is used for abelian semigroups and topological groups (see Semigroup_ZF, Group_ZF, AbelianGroup_ZF and CommutativeSemigroup_ZF, TopologicalGroup_ZF at isarmathlib.org ).
Kind regards,
Slawomir Kolodynski
http://savannah.nongnu.org/projects/isarmathlib Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Email Gateway (Aug 22 2022 at 19:40):From: Dominique Unruh <unruh@ut.ee>
Hi,
that's interesting. It would certainly be of interest to think of a
large-scale overhaul of HOL-Algebra using modern locale features.
There is the additional problem that there is a lot of duplication of
concepts, using classes vs locales.
E.g., monoid_mult (type class, in HOL) vs. monoid (locale, in
HOL-Algebra). The classes have the advantage of being easier to use than
locales in many cases (at least I feel that way), but they have the
limitation of always having UNIV as the carrier.
As far as I know, all proofs are simply done twice. And someone building
a development on these things needs to pick on approach and is then
"locked in", which is problematic, since some material is only available
in the HOL approach and some only in the HOL-Algebra approach.
In case of an overhaul, perhaps these concepts could be unified as well?
I am not sure what the best approach is for such a unification, but some
idea would be:
* Have compatible names as far as possible. E.g., if the class is
called XXX, then the locale is called l_XXX or something.
* Have the possibility to transfer theorems between compatible classes
and locales. (Compatible means: when the class is the locale with
carrier:=UNIV.)
o For transferring from locale to class, that might work
automatically (haven't checked) if we prove "sublocale XXX <=
l_XXX UNIV".
o For transferring from class to locale it more difficult.
Possibly something involving the Types_To_Sets tools might work?
Unfortunately, I fear that even though there is not /that/ much material
building on HOL-Algebra, it would involve a lot of work.
What if instead of editing HOL-Algebra, a new session HOL-Algebra2 is
created? And then deprecating HOL-Algebra. (Or even renaming HOL-Algebra
to HOL-Algebra-Old.)
Then it will be optional to update old AFP material building on HOL-Algebra.
I also don't think there are any "heavy" users of HOL-Algebra these days
I wonder whether that might partially be because of the incompatibility
with the type-class approach. (I, at least, never look at HOL-Algebra
because we are building on real_vector_space in our formalizations and
thus "locked in".)
Best wishes,
Dominique.
Last updated: Apr 26 2024 at 12:28 UTC