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 = 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 = Identity element of monoid, overloaded as #e.
Overloading:
* = g.op
#e = 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``);
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>:
>
> 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
>> <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 <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
> 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
