Email Gateway (Aug 22 2022 at 18:27): Email Gateway (Aug 22 2022 at 18:27):From: Ken Kubota <mail@kenkubota.de>
José wrote:
The problem is that Abstract Algebra concerns the properties of structures
which are independent from their concrete presentations. For any R-module
In order to express this properly, type abstraction is required, which abstracts
from the concrete type ("their concrete presentations"). It creates a link between
the type and the term level, e.g.
[\t.\*:ttt . a * id = a ]
or
[\t.\x_{ttt} . a x id = a ]
for some identity element id.
Note that the variable t appears both at the term and at the type (subscript) level.
Standard HOL doesn't provide this feature, which was already suggested by
HOL founder Mike Gordon (he called it "'second order' λ-terms" [Gordon, 2001, p. 22]).
Extended HOL (Melham) provides quantification over types, but not the binding
of type variables with lambda (type abstraction) - like Andrews' system Q presented
in his Ph.D. thesis [Andrews, 1965] to which Tom refers explicitly in [Melham, 1993b].
With type abstraction, it is possible to prove abstract properties ("properties of
structures") and then transfer them to concrete objects.
Group theory is best suited to demonstrate this, and I also chose group theory:
http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/#type_abstraction
See the definitions "Grp" and "GrpIdy" there.
In my example I proved that the identity element of a group is unique (p. 367),
and then instantiated (p. 423) this general theorem valid for any group to a concrete
group (XOR) after proving that XOR is a group (p. 420) at
http://doi.org/10.4444/100.10.2
In order to verify the abstract proof and to see the group definition details, run
make group_identity_element_unique.r0.out.html && open $_
make group.r0.out.html && open $_
on any Mac after downloading the software (license restrictions apply) at
http://doi.org/10.4444/100.10.3
It is possible to use auxiliary constructs such as the Isabelle axiomatic type classes,
but then additional checks have to be implemented since the syntax of the formal language
doesn't have the expressiveness which would be necessary for naturally representing
the mathematical structure in question.
For references, please see: http://doi.org/10.4444/100.111
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100
Am 04.09.2018 um 03:22 schrieb José Manuel Rodriguez Caballero <josephcmac@gmail.com>:
Larry wrote:
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.Manuel wrote:
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.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/9780387953854First, 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_moduleThe 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-XD5FfoKind Regards,
Jose M.
Email Gateway (Aug 22 2022 at 18:27):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I am interested in this subject because I am working with the free abelian
group of primitive Pythagorean triangles (motivated for number-theoretic
reasons):
Eckert, Ernest J. "Primitive pythagorean triples." The College Mathematics
Journal 23.5 (1992): 413-417.
https://www.jstor.org/stable/pdf/2686417.pdf?casa_token=eoApY3SZBlIAAAAA:rx2mm61ERF6Y_xQ4vt2P3cIDyRPVibbLSqXZqBveMv_I6L0EPqsS12vpgZBxU4vBRyiHbqG-yX2FJR_nI14nfSOUSLhe44WOJGAUIxVFuO4ewTG9TA
Could the universal property of free abelian groups be stated in
Isabelle/HOL?
I recall the universal property of a free abelian group F with basis B: for
every function f from B to an abelian group A, there exists a unique group
homomorphism from F to A which extends f.
Kind Regards,
Jose M.
Last updated: Apr 26 2024 at 04:17 UTC