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