Post by José Manuel Rodriguez CaballeroThe 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
Post by José Manuel Rodriguez CaballeroPost by Lawrence PaulsonHOL 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.
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
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
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).
Text (advanced): https://ncatlab.org/nlab/show/natural+transformation
Video (elementary introduction): http://youtu.be/2LJC-XD5Ffo
Kind Regards,
Jose M.