gap-system / gap

Main development repository for GAP - Groups, Algorithms, Programming, a System for Computational Discrete Algebra
https://www.gap-system.org
GNU General Public License v2.0
803 stars 163 forks source link

Basic Group Constructors #2072

Open stevelinton opened 6 years ago

stevelinton commented 6 years ago

This comes from #2037.

At the moment neither the declaration of TrivialGroupCons in grp/basic.gd nor the installation of methods for it (in #2037 for instance) actually specifies that the group returned should be trivial. This means that

gap> TrivialGroupCons(IsGroup and IsTrivial and IsFpGroup)

fails. Other constructors defined in the same file have essentially the same problem. Whatever we do, the declarations must be updated to specify more precisely what the object returned should be.

What is less clear is what the method installations should look like. If we don't change the underlying machinery, then every method for (eg) TrivialGroupCons would need to specify that it did promise to return a trivial group so you might have

InstallMethod(TrivialGroupCons, [IsFpGroup and IsTrivialGroup],....)

The alternative is basically to supply these compulsory filters automatically, using the data stored with the constructor, so the above installation would just look like:

InstallMethod(TrivialGroupCons, [IsFpGroup],....)

but GAP Would know that it "really" promises to return a trivial (and therefore finite, abelian, simple, etc.) group and could select it when one was needed. The first is, perhaps, less prone to undetected errors creeping in, the second is more concise.

Thoughts?

stevelinton commented 6 years ago

@fingolfin has pointed out that, in addition, there is a problem with the handling of implications in this situation, which clearly needs to be dealt with too. For a normal method requirement there is no sense in adding implications before storing it, because any object satisfying the requirement as given will also satisfy the implications. That doesn't work for the first argument of a constructor though because the requirement is reversed.