[isabelle] Type abstraction - Re: free Abelian groups



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 at 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/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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.