You have misunderstood. The Hol_datatype call establishes a type entirely within the logic and is *not* an SML entity at all. The mathematical content is entirely within the logic.
The definition of Group that you found is expressed in terms of Monoid. (Every group is a monoid.) The monoid type mentions the carrier set with the Hol_datatype definition, as you found, and so we can, within the logic, talk about groups’ carrier sets. Your examples are trivial to establish given the framework, and again, entirely within the logic. Michael On 6 Feb 2021, at 02:35, Ken Kubota <m...@kenkubota.de<mailto:m...@kenkubota.de>> wrote: Thanks, Michael. I have provided links and quotes from the source with definitions below. My knowledge on the technical details of the HOL/HOL4 implementation is limited. Is it correct to say that 'a is the polymorphic type-variable, and that the (monoid and) group definition is based on an ML datatype (which is syntactically in some sense equivalent to a struct in C or a class in C++, as type information is bundled there)? val _ = Hol_datatype` monoid = <| carrier: 'a -> bool; op: 'a -> 'a -> 'a; id: 'a |>`; https://bitbucket.org/jhlchan/hol/src/master/algebra/monoid/monoid.hol (February 5, 2021) My criticism would be that part of the mathematical content is represented outside of the mathematical logic, as is the case with group theory in Isabelle/HOL. In HOL4, features of the meta-language (datatypes in ML) are deployed to represent type information, and in Isabelle/HOL group theory, the meta-logic of the logical framework is used to represent type dependencies. This leads to an only implicit type handling within the mathematical logic (e.g., in HOL4: "Group_def |- !g. Group g <=> [...]"), where the carrier set (the type of group elements) is not mentioned. However, one would like to express _within_ the mathematical logic that, for example, (Z,+) is a group: Grp(Z,+) In my example, I had shown that (o, XOR) is a group: Grp(o, XOR) Quote: Grp o XOR https://www.owlofminerva.net/files/formulae.pdf#page=420 Definition of group: := Grp [λgτ .[λlggg.(∧oooGrpAsco(∃o(o\3)τ gτ [λeg.(∧oooGrpIdyoGrpInvo)o]))o](o(ggg))] # wff 266 : [λg.[λl.(∧ GrpAsc (∃ g [λe.(∧ GrpIdy GrpInv)]))]]o(\4\4\3)τ := Grp https://www.owlofminerva.net/files/formulae.pdf#page=362 Note that the type of group elements (the carrier set g) is bound by lambda (type abstraction). See also section "Type abstraction" at: https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/ The well-formed formula lggg (or l: g -> g-> g) corresponds to the HOL4 expression of the binary operation of group op: 'a -> 'a -> 'a; and the wff eg (or e: g) corresponds to the HOL4 expression of the identity element of group id: 'a quoted above. Kind regards, Ken Kubota ____________________________________________________ Ken Kubota https://doi.org/10.4444/100 Group Theory in HOL4: https://bitbucket.org/jhlchan/hol/src/master/algebra/group/group.hol Repository location: https://bitbucket.org/jhlchan/hol/src/ (provided on p. 145 of the PhD thesis) DOI Link PhD Thesis: https://doi.org/10.25911/5f58b06ca124e Release notes for HOL4, Kananaskis-14: https://sourceforge.net/p/hol/mailman/message/37211501/ Quote from group.hol: (* ------------------------------------------------------------------------- *) (* Group Documentation *) (* ------------------------------------------------------------------------- *) (* Data type (same as monoid): The generic symbol for group data is g. g.carrier = Carrier set of group, overloaded as G. g.op = Binary operation of group, overloaded as *. g.id<http://g.id> = Identity element of group, overloaded as #e. g.exp = Iteration of g.op (added by monoid) g.inv = Inverse of g.op (added by monoid) *) (* Definitions and Theorems (# are exported): Definitions: Group_def |- !g. Group g <=> Monoid g /\ (G* = G) [...] (* ------------------------------------------------------------------------- *) (* Group Definition. *) (* ------------------------------------------------------------------------- *) (* Set up group type as a record A Group has: . a carrier set (set = function 'a -> bool, since MEM is a boolean function) . an identity element . an inverse function (unary operation) . a product function called multiplication (binary operation) *) (* Monoid and Group share the same type: already defined in monoid.hol val _ = Hol_datatype` group = <| carrier:'a -> bool; id: 'a; inv:'a -> 'a; -- by val _ = add_record_field ("inv", ``monoid_inv``); mult:'a -> 'a -> 'a |>`; *) val _ = type_abbrev ("group", Type `:'a monoid`); (* Define Group by Monoid *) val Group_def = Define` Group (g:'a group) <=> Monoid g /\ (G* = G) `; https://bitbucket.org/jhlchan/hol/src/master/algebra/group/group.hol (February 5, 2021) Quote from monoid.hol: (* ------------------------------------------------------------------------- *) (* Monoid Documentation *) (* ------------------------------------------------------------------------- *) (* Data type: The generic symbol for monoid data is g. g.carrier = Carrier set of monoid, overloaded as G. g.op = Binary operation of monoid, overloaded as *. g.id<http://g.id> = Identity element of monoid, overloaded as #e. Overloading: * = g.op #e = g.id<http://g.id> ** = g.exp G = g.carrier GITSET g s b = ITSET g.op s b *) (* Definitions and Theorems (# are exported): Definitions: Monoid_def |- !g. Monoid g <=> (!x y. x IN G /\ y IN G ==> x * y IN G) /\ (!x y z. x IN G /\ y IN G /\ z IN G ==> ((x * y) * z = x * (y * z))) /\ #e IN G /\ (!x. x IN G ==> (#e * x = x) /\ (x * #e = x)) [...] (* ------------------------------------------------------------------------- *) (* Monoid Definition. *) (* ------------------------------------------------------------------------- *) (* Monoid and Group share the same type *) (* Set up monoid type as a record A Monoid has: . a carrier set (set = function 'a -> bool, since MEM is a boolean function) . a binary operation (2-nary function) called multiplication . an identity element for the binary operation *) val _ = Hol_datatype` monoid = <| carrier: 'a -> bool; op: 'a -> 'a -> 'a; id: 'a |>`; [...] (* Using symbols m for monoid and g for group will give excessive overloading for Monoid and Group, so the generic symbol for both is taken as g. *) (* set overloading *) val _ = overload_on ("*", ``g.op``); val _ = overload_on ("#e", ``g.id<http://g.id>``); val _ = overload_on ("G", ``g.carrier``); (* Monoid Definition: A Monoid is a set with elements of type 'a monoid, such that . Closure: x * y is in the carrier set . Associativity: (x * y) * z = x * (y * z)) . Existence of identity: #e is in the carrier set . Property of identity: #e * x = x * #e = x *) (* Define Monoid by predicate *) val Monoid_def = Define` Monoid (g:'a monoid) <=> (!x y. x IN G /\ y IN G ==> x * y IN G) /\ (!x y z. x IN G /\ y IN G /\ z IN G ==> ((x * y) * z = x * (y * z))) /\ #e IN G /\ (!x. x IN G ==> (#e * x = x) /\ (x * #e = x)) `; https://bitbucket.org/jhlchan/hol/src/master/algebra/monoid/monoid.hol (February 5, 2021) Quote from bossLib.Hol_datatype.html: Hol_datatype : hol_type quotation -> unit STRUCTURE bossLib SYNOPSIS Define a concrete datatype (deprecated syntax). DESCRIPTION The Hol_datatype function provides exactly the same definitional power as the Datatype function (which see), with a slightly different input syntax, given below: spec ::= [ <binding> ; ]* <binding> binding ::= <ident> = [ <clause> | ]* <clause> | <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |> clause ::= <ident> | <ident> of [<type> => ]* <type> https://hol-theorem-prover.org/kananaskis-14-helpdocs/help/Docfiles/HTML/bossLib.Hol_datatype.html (February 5, 2021) Quote from bossLib.Datatype.html: Datatype : hol_type quotation -> unit STRUCTURE bossLib SYNOPSIS Define a concrete datatype. DESCRIPTION Many formalizations require the definition of new types. For example, ML-style datatypes are commonly used to model the abstract syntax of programming languages and the state-space of elaborate transition systems. In HOL, such datatypes (at least, those that are inductive, or, alternatively, have a model in an initial algebra) may be specified using the invocation Datatype `<spec>`, where <spec> should conform to the following grammar: spec ::= [ <binding> ; ]* <binding> binding ::= <ident> = [ <clause> | ]* <clause> | <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |> clause ::= <ident> <tyspec>* tyspec ::= ( <type> ) | <atomic-type> where <atomic-type> is a single token denoting a type. For example, num, bool and 'a. https://hol-theorem-prover.org/kananaskis-14-helpdocs/help/Docfiles/HTML/bossLib.Datatype.html (February 5, 2021) Am 03.02.2021 um 23:29 schrieb Norrish, Michael (Data61, Acton) <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>: Hing Lun Chan’s thesis (linked to in the notes below) provides pretty good documentation of the approach taken, as do the various papers arising from the work. The short version of the story is that the “obvious” approach of working with a polymorphic type-variable to represent the type of group elements doesn’t make the task of proving the required results too arduous. Michael On 4 Feb 2021, at 01:13, Ken Kubota <m...@kenkubota.de<mailto:m...@kenkubota.de>> wrote: Is there any documentation on how abstract algebra is implemented in HOL4? Usually the HOL type system is considered too weak. Freek Wiedijk: “The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.” John Harrison, Josef Urban, and Freek Wiedijk: “Another limitation of the simple HOL type system is that there is no explicit quantifier over polymorphic type variables, which can make many standard results [...] awkward to express [...]. [...] For example, in one of the most impressive formalization efforts to date [Gonthier et al., 2013] the entire group theory framework is developed in terms of subsets of a single universe group, apparently to avoid the complications from groups with general and possibly heterogeneous types.” https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00074.html Kind regards, Ken Kubota ____________________________________________________ Ken Kubota https://doi.org/10.4444/100 Am 03.02.2021 um 03:47 schrieb Norrish, Michael (Data61, Acton) <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>: Release notes for HOL4, Kananaskis-14 (Released: 3 February 2021) We are pleased to announce the Kananaskis-14 release of HOL4. New examples: * algebra: an abstract algebra library for HOL4. The algebraic types are generic, so the library is useful in general. The algebraic structures consist of monoidTheory for monoids with identity, groupTheory for groups, ringTheory for commutative rings, fieldTheory for fields, polynomialTheory for polynomials with coefficients from rings or fields, linearTheory for vector spaces, including linear independence, and finitefieldTheory for finite fields, including existence and uniqueness. _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
