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

[Konrad Slind]

> I just want to point out that the goalposts have shifted
> slightly. The material pointed to by Michael shows that a fair
> bit of basic abstract algebra can be cleanly done in HOL's type
> theory, which I gather was the original point in question.
>
> re: Ken's questions.
>
> 1. The carrier is expressed as a predicate on a polymorphic type,
>so it is indeed a term. Moreover, the UNIV operator can be
>used to get the set of elements of a type. So I am not really
>seeing this as an impediment, at least for the simple examples
>being discussed.
>
> 2. Yes, there is no quantification of type variables in the HOL
>logic. This has been discussed at length in earlier postings
>on this list. Extensions of HOL with type quantification have
>been proposed by Melham and, later, by Homeier. These have
>been implemented and applied to interesting examples, but
>HOL4 hasn't moved to type quantification yet.
>
> Konrad.
>

(Deleted previous messages in thread because MailMan complains)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Ken Kubota]

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 

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 
 
(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 

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 

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 

Example for type substitution:
https://www.owlofminerva.net/files/formulae.pdf#page=347 


Kind regards,

Ken Kubota



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



> Am 06.02.2021 um 01:43 schrieb Norrish, Michael (Data61, Acton) 
> :
> 
> 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 > > 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 defi

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

[Norrish, Michael (Data61, Acton)]

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