Re: [Hol-info] Abstract algebra in HOL4 and Isabelle/HOL – Re: Abstract algebra in HOL4 – Re: Re

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Thanks for the clarification that the Hol_datatype call establishes a type entirely within the logic.

However, in HOL/HOL4 a natural expression of a statement such as Grp(Z,+) or Grp(o, XOR) isn't possible for two reasons:

1. The group carrier set is represented at the type level only, but not at the term level.
Note that in my example, in the statement
	Grp o XOR
all three symbols (Grp, o, and XOR) are symbols at the term level: https://www.owlofminerva.net/files/formulae.pdf#page=420 <https://www.owlofminerva.net/files/formulae.pdf#page=420>
Due to type abstraction in R0 (binding of type variables with lambda) types can appear both at the term and at the type level.
Lambda application/conversion then causes substitution at the type level also.

2. The universal quantification of the type variable remains implicit, as (explicit) quantification over types is not available.

While it is true that the rather simple example I used (depending on only one type) can be expressed with weaker means in a less natural way (mentioning the group carrier set at the type level only, and with implicit universal quantification over types only), it should be easy to find examples not expressible in HOL/HOL4 at all (e.g., with two type variables, where the type of one type variable depends on the other type variable).
Obviously, existential quantification over types is not expressible at all, as Freek Wiedijk already pointed out:
	The quantification of this carrier type will be implicit. For that reason only universal quantification over these carrier types is possible. Which means that in HOL it is not possible to write
		There exists a carrier type together with a field with that carrier type . . .
	http://logika.uwb.edu.pl/studies/download.php?volid=23&artid=fw&format=PDF <http://logika.uwb.edu.pl/studies/download.php?volid=23&artid=fw&format=PDF> (p. 126)

Also, without quantification over types, it is not possible to make the use of the Axiom of Choice explicit, since, as Rob Arthan pointed out, in a hypothesis instantiation of type variables is not allowed:
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/msg00051.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-March/msg00051.html>
Making the Axiom of Choice explicit (as a hypothesis) allows one to view it as a non-logical axiom, as already considered by Andrews: "One may also wish to assume additional axioms, such as the Axiom Schema of Choice [...], though there is room for argument whether these are axioms of pure logic or of mathematics." [Andrews 2002 (ISBN 1-4020-0763-9), p. 204]

Finally, in HOL/HOL4 a separate rule "Type instantiation [INST_TYPE]" is required,
	https://sourceforge.net/projects/hol/files/hol/kananaskis-14/kananaskis-14-logic.pdf (p. 28)
while in R0 this is a derived rule, which is in the spirit of Andy Pitts' statement in the HOL handbook: “From a logical point of view, it would be better to have a simpler substitution primitive, such as ‘Rule R’ of Andrews’ logic Q0, and then to derive more complex rules from it.” [Gordon and Melham, 1993, p. 213]
	https://owlofminerva.net/files/fom_2018.pdf#page=6 <https://owlofminerva.net/files/fom_2018.pdf#page=6>
The rule "Type instantiation" then appears in R0 just as a special case of Andrews' Rule of Substitution (Sub) [Theorem 5221], where the substituted variable is a type variable (i.e., a variable of type tau).

Rule of Substitution / Proof Template A5221H (Sub):
	https://www.owlofminerva.net/files/formulae.pdf#page=82 <https://www.owlofminerva.net/files/formulae.pdf#page=82>
Example for type substitution:
	https://www.owlofminerva.net/files/formulae.pdf#page=347 <https://www.owlofminerva.net/files/formulae.pdf#page=347>

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100

> Am 06.02.2021 um 01:43 schrieb Norrish, Michael (Data61, Acton) <Mic...@da...>:
> 
> 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 <ma...@ke... <mailto:ma...@ke...>> 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 <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 <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 <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/ <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 <https://doi.org/10.4444/100>
>> 
>> 
>> 
>> Group Theory in HOL4: https://bitbucket.org/jhlchan/hol/src/master/algebra/group/group.hol <https://bitbucket.org/jhlchan/hol/src/master/algebra/group/group.hol>
>> Repository location: https://bitbucket.org/jhlchan/hol/src/ <https://bitbucket.org/jhlchan/hol/src/> (provided on p. 145 of the PhD thesis)
>> DOI Link PhD Thesis: https://doi.org/10.25911/5f58b06ca124e <https://doi.org/10.25911/5f58b06ca124e>
>> Release notes for HOL4, Kananaskis-14: https://sourceforge.net/p/hol/mailman/message/37211501/ <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 <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 <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 <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 <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) <Mic...@da... <mailto:Mic...@da...>>:
>>> 
>>> 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 <ma...@ke... <mailto:ma...@ke...>> 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) <Mic...@da... <mailto:Mic...@da...>>:
>>>>> 
>>>>>> 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...@li... <mailto:hol...@li...>
>>> https://lists.sourceforge.net/lists/listinfo/hol-info <https://lists.sourceforge.net/lists/listinfo/hol-info>
>> 
> 

Re: [Hol-info] Abstract algebra in HOL4 and Isabelle/HOL – Re: Abstract algebra in HOL4 – Re: Re

Re: [Hol-info] Abstract algebra in HOL4 and Isabelle/HOL – Re: Abstract algebra in HOL4 – Re: Release notes for HOL4, Kananaskis-14