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

[Ken K. <ma...@ke...>]

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



> Am 03.02.2021 um 03:47 schrieb Norrish, Michael (Data61, Acton) <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.
>>