Email Gateway (Aug 22 2022 at 18:19): Email Gateway (Aug 22 2022 at 18:19):From: Lawrence Paulson <lp15@cam.ac.uk>
HOL Light defines a type “frag” of free Abelian groups over some other type: finite maps from type elements to integers. Each such map represents a monomial with integer exponents. Do we have such a thing already? (We have finite maps, of course.)
Larry Paulson
Email Gateway (Aug 22 2022 at 18:22):From: Manuel Eberl <eberlm@in.tum.de>
I don't think we have anything like that. It is a very nice structure,
but I have never really run into a situation where I needed anything
like it.
I guess you need that for homology, right?
Manuel
pEpkey.asc
Email Gateway (Aug 22 2022 at 18:23):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
One option is to use the Poly_Mapping theory in AFP/Polynomials:
https://www.isa-afp.org/browser_info/current/AFP/Polynomials/Poly_Mapping.html
These are the finite maps where the default value is 0. To represent free Abelian group over 'a
use: 'a ⇒⇩0 int the group structure is given by the additive operations.
What is missing is the map to interpret a free Abelian group as a formal sum:
map :: ('a = 'b::ab_group_add) => ('a ⇒⇩0 int) => 'b
map f G = (SUM a | lookup G a ~= 0. lookup G a *_i f a)
where *_i is scalar multiplication with an integer, defines as:
(n + 1) *_i a = n *_i a + a
(n - 1) *_i a = n *_i a - a
0 *_i a = 0
- Johannes
Email Gateway (Aug 22 2022 at 18:24):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
There is a deep theoretical reason in order to explain why the above
mentioned frag from HOL Light is avoided, whenever it is possible, in
Abstract Algebra, e.g., in Serge Lang's approach:
https://www.springer.com/gp/book/9780387953854
First, a little bit of terminology. Let M be a module over the ring R
(R-module for short). The R-module of finite maps from elements in M to R,
which are homomorphisms, is denoted M* and it is called the dual R-module
of M. An Abelian group is the same as an R-module, where R is the ring of
integers, denoted Z. If M a free Z-module, i.e. a free Abelian group, then
M* can be identified with the above-mentioned frag of HOL Light, endowed
with the componentwise addition. Reference for dual modules:
https://en.wikipedia.org/wiki/Dual_module
The problem is that Abstract Algebra concerns the properties of structures
which are independent from their concrete presentations. For any R-module
M, its dual R-module M* depends upon both M and a set S of generators of M.
In general, for a given M, there are many choices of the set S. So, in
order to prove a property of M from a property of M*, the set S should be
arbitrary from the beginning of the proof. Otherwise, the property of M*
will be translated into a property of the pair (M, S), not just of M.
Abstract Algebra is not interested in the pair (M, S), although
Computational Algebra may be interested in such a pair.
This problem was the main motivation for the introduction of the concept of
natural transformation, and then for the development of Category Theory.
For example, there is a natural transformation between M and M** (its
double dual, i.e., the dual of its dual).
References for natural transformations:
Text (advanced): https://ncatlab.org/nlab/show/natural+transformation
Video (elementary introduction): https://www.youtube.com/watch?v=2LJC-XD5Ffo
Kind Regards,
Jose M.
Email Gateway (Aug 22 2022 at 18:26):From: Lawrence Paulson <lp15@cam.ac.uk>
That background is very interesting, thanks! However, I merely need this in order to port some HOL Light proofs involving homology theory. As I port these proofs with almost no knowledge of the subject matter, I'm seldom able to improve them very much. I leave that to people who know what they are doing. Meanwhile, even in their original form, the ported HOL Light libraries seem to be very useful.
Larry
Email Gateway (Aug 22 2022 at 18:27):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for the suggestion. I've already reported a decent chunk of the HOL Light code, but it's surely better to work with this more general development.
I wonder whether Poly_Mapping.thy should be moved to the Library directory? It doesn't depend on anything else in the Polynomial entry.
Larry
Email Gateway (Aug 22 2022 at 18:28):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi, Lawrence. Look how your e-mail looks like in archive:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00041.html .
As you can see, it transforms to one big line which is very hard to
read, because you have to scrool horizontally. Please, configure your mail
client properly or (better) configure mailing list archive to display mails
properly.
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:28):From: Lawrence Paulson <lp15@cam.ac.uk>
That’s annoying. Looks like Mailman wants to work for Linux only. The rest of the world formats paragraphs as single lines.
I don’t see any formatting options on the mailing list configuration page, but I’m open to hints.
Larry
Email Gateway (Aug 22 2022 at 18:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Larry,
I wonder whether Poly_Mapping.thy should be moved to the Library directory? It doesn't depend on anything else in the Polynomial entry.
this would be feasible of course, with the following issues:
I still do not have a more appropriate name at hand than poly_mapping
and I am open to suggestions.
Since the theory has a strong bias towards constructing and executing
algebraic concepts, Computational_Algebra might be a better session.
The theory contains auxiliary concerning lists with no trailing zeros,
which would be useful as separate theory also: for radix representations
and HOL-Library.Polynomial also.
Another prospective application: ‹(nat, 8 word) poly_mapping› would be
a suitable model for big integers as bytes.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:31):From: Lawrence Paulson <lp15@cam.ac.uk>
I would be equally happy to see it in Computational_Algebra. Presumably its dependence on three other theories from HOL-Library isn't relevant.
Presumably no_trailing_zeros could be transferred to Library.More_List, since it builds on primitives defined in that theory.
I have no suggestions for a more appropriate name.
Larry
signature.asc
Email Gateway (Aug 22 2022 at 18:31):From: Manuel Eberl <eberlm@in.tum.de>
If the 'b is restricted to int, one has the subgroup of a finite Abelian
group where all the elements have finite support. This is commonly
called a the group of ‘formal sums’. Another possible name would be
‘signed multisets’.
Not of course, ‘poly_mapping’ is a bit more general than that in that it
allows an arbitrary result type, not just integers. Perhaps ‘formal sum’
is still good enough. Or ‘formal quasisum’?
Manuel
pEpkey.asc
Last updated: Apr 27 2024 at 01:05 UTC