Email Gateway (Aug 19 2022 at 11:23): Email Gateway (Aug 19 2022 at 11:23):From: Josh Tilles <merelyapseudonym@gmail.com>
I was looking at the HOL-Algebra
"session"<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html>
and
I had a few questions.
First, the README<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/README.html>
refers
to type-classes disparagingly. Does the Isabelle community at large believe
that "axiomatic type classes" cannot be "first-class citizens of the
logic"? If so, I'd be interested to know why that's the case, but it's
not required so don't spend too much time explaining.
Second, many of the theories listed in HOL-Algebra are topically similar to
theories included in HOL's Main. Why are they split out?
Examples:
Algebra's Group<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Group.html>
vs
Main's Groups <http://isabelle.in.tum.de/dist/library/HOL/Groups.html>
Algebra's Lattice<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Lattice.html>
vs
Main's Lattices <http://isabelle.in.tum.de/dist/library/HOL/Lattices.html>
& Complete_Lattices<http://isabelle.in.tum.de/dist/library/HOL/Complete_Lattices.html>
Algebra's Bij<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/Bij.html>
vs
Main's Fun <http://isabelle.in.tum.de/dist/library/HOL/Fun.html>
Algebra's FuncSet<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/FuncSet.html>
vs
a number of theories in Main.
It seems plausible to me that some theories (particularly the dependencies
of Main and/or Complex_Main) would exist as means to some end, only to
compose into a more useful tool. Whereas other theories (certainly most
from IsarMathLib <http://isarmathlib.org/>) are meant as bodies of
mathematical knowledge. Is this a useful distinction to make when browsing
the Isabelle codebase? Does that distinction explain the difference between
Main's theories and Algebra's theories?
I'd really appreciate any answers —or even guidance— you can provide.
--Josh Tilles
(if it's useful to know anything about my background: I'm a programmer, not
a mathematician. I'm using Isabelle in conjunction with a few other
materials to review and explore math, but I'm probably won't venture
outside of upper-undergraduate-level mathematics for a while.)
Email Gateway (Aug 19 2022 at 11:23):From: Lars Noschinski <noschinl@in.tum.de>
On 27.07.2013 21:49, Josh Tilles wrote:
First, the README<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/README.html>
refers
to type-classes disparagingly. Does the Isabelle community at large believe
that "axiomatic type classes" cannot be "first-class citizens of the
logic"? If so, I'd be interested to know why that's the case, but it's
not required so don't spend too much time explaining.
The issue with type classes is that they only work with types. I.e., the
type class group can only used if the whole universe of a type is a
group. So e.g. the type int forms a group (Z). However, we cannot reason
about the subgroups of Z with the group typeclass.
So, HOL-Algebra does use an explicit domain set and locales instead of
type classes. This makes for a more cumbersome (as a user, you always
need to maintain that the elements you are talking about are elements of
the domain), but more general reasoning.
It seems plausible to me that some theories (particularly the dependencies
of Main and/or Complex_Main) would exist as means to some end, only to
compose into a more useful tool. Whereas other theories (certainly most
from IsarMathLib<http://isarmathlib.org/>) are meant as bodies of
mathematical knowledge. Is this a useful distinction to make when browsing
the Isabelle codebase? Does that distinction explain the difference between
Main's theories and Algebra's theories?
Yes, I think this is a good rule of thumb.
-- Lars
Email Gateway (Aug 19 2022 at 11:23):From: Makarius <makarius@sketis.net>
There are indeed some funny believes about certain aspects of Simple Type
Theory (Isabelle Pure and HOL), leading to Isabelle insider jokes like
"axiomatic type classes are definitional" and "HOL typedef is axiomatic".
(The second one is off-topic here.)
My master's thesis from 1994 demonstrates how type classes are made
first-class citizens of Isabelle/Pure in most respects; this was later
published on TPHOLs 1997, see also
http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
The more recent papers by Haftmann and Wenzel on "Constructive Type
Classes" http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf
and "Local theory specifications in Isabelle/Isar"
http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf explain
further how everything fits together: type classes, locales, definitional
specifications within any such "module system".
This is all very close to the actual logic, but as usual in Isabelle, the
logic alone only serves fountational purposes. Extra-logical add-ons like
code generation are just as important. For end-users it hardly matters
what is the core logic and what not, as long as it works in symphony.
Makarius
Email Gateway (Aug 19 2022 at 11:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Josh,
First, the
README<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/README.html>
refers
to type-classes disparagingly. Does the Isabelle community at large believe
that "axiomatic type classes" cannot be "first-class citizens of the
logic"? If so, I'd be interested to know why that's the case, but it's
not required so don't spend too much time explaining.Second, many of the theories listed in HOL-Algebra are topically similar to
theories included in HOL's Main. Why are they split out?
as a rule of thumb, there are basically two algebraic hierarchy
developments in HOL:
HOL-Main with type classes:
HOL-Algebra with locales:
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:46):From: Josh Tilles <merelyapseudonym@gmail.com>
On Mon, Jul 29, 2013 at 3:39 AM, Lars Noschinski <noschinl@in.tum.de> wrote:
On 27.07.2013 21:49, Josh Tilles wrote:
First, the README<http://isabelle.in.tum.de/dist/library/HOL/HOL-
Algebra/README.html<http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/README.html>
>refers
to type-classes disparagingly. Does the Isabelle community at large
believe
that "axiomatic type classes" cannot be "first-class citizens of the
logic"? If so, I'd be interested to know why that's the case, but it'snot required so don't spend too much time explaining.
The issue with type classes is that they only work with types. I.e., the
type class group can only used if the whole universe of a type is a group.
So e.g. the type int forms a group (Z). However, we cannot reason about the
subgroups of Z with the group typeclass.So, HOL-Algebra does use an explicit domain set and locales instead of
type classes. This makes for a more cumbersome (as a user, you always need
to maintain that the elements you are talking about are elements of the
domain), but more general reasoning.Thank you for the explanation! I can't say I completely understand what you
wrote, but this gives me material to pay attention to as I explore.
It seems plausible to me that some theories (particularly the dependencies
of Main and/or Complex_Main) would exist as means to some end, only to
compose into a more useful tool. Whereas other theories (certainly most
from IsarMathLib<http://**isarmathlib.org/ <http://isarmathlib.org/>>)
are meant as bodies ofmathematical knowledge. Is this a useful distinction to make when browsing
the Isabelle codebase? Does that distinction explain the difference
between
Main's theories and Algebra's theories?
Yes, I think this is a good rule of thumb.
And thank you for the confirmation.
-- Lars
Email Gateway (Aug 19 2022 at 11:46):From: Josh Tilles <merelyapseudonym@gmail.com>
Thank you for explaining your perspective. It's certainly different than
Lars's and I'll be revisiting both as I gain more experience.
And thank you for directing my attention to those papers as well. I expect
they'll help clarify some concepts.
Email Gateway (Aug 19 2022 at 11:46):From: Josh Tilles <merelyapseudonym@gmail.com>
Florian,
(As I've written more than once in this thread:) thank you for taking the
time for explain those distinctions. I may not understand everything you
wrote right now (e.g., what is a "proper meta theory"?) but I'll keep these
differences in mind.
Email Gateway (Aug 19 2022 at 11:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Josh,
the meaning of »meta theory« in this context is roughly that you can
reason about algebraic structures, not only on properties of their
elements. For example, the classification of all simple groups would be
meta theory, whereas the statement »The integers form a group wrt. +, 0
and -« is not.
Hope this helps,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC