*To*: José Manuel Rodriguez Caballero <josephcmac at gmail.com>*Subject*: [isabelle] Type abstraction - Re: free Abelian groups*From*: Ken Kubota <mail at kenkubota.de>*Date*: Wed, 5 Sep 2018 14:54:27 +0200*Cc*: "Prof. Thomas F. Melham" <thomas.melham at balliol.ox.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAA8xVUjV6_2GAJSDuv_MRcDeqs7n=qcpj_6GCEavsvYYM-xYhA@mail.gmail.com>*References*: <CAA8xVUjV6_2GAJSDuv_MRcDeqs7n=qcpj_6GCEavsvYYM-xYhA@mail.gmail.com>

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.

**Follow-Ups**:**Re: [isabelle] Type abstraction - Re: free Abelian groups***From:*José Manuel Rodriguez Caballero

**References**:**Re: [isabelle] free Abelian groups***From:*José Manuel Rodriguez Caballero

- Previous by Date: Re: [isabelle] Concurrent/counter.ML
- Next by Date: Re: [isabelle] free Abelian groups
- Previous by Thread: Re: [isabelle] Mailing list archive configuration (was: free Abelian groups)
- Next by Thread: Re: [isabelle] Type abstraction - Re: free Abelian groups
- Cl-isabelle-users September 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list