From e3484a33d7823164f30c01cb20157df01f68542e Mon Sep 17 00:00:00 2001 From: Markus Pfeiffer <markus.pfeiffer@morphism.de> Date: Wed, 7 Jun 2017 08:51:12 +0100 Subject: [PATCH] Add some notes on aligning GAP with MMT --- source/alignment.txt | 289 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 289 insertions(+) create mode 100644 source/alignment.txt diff --git a/source/alignment.txt b/source/alignment.txt new file mode 100644 index 0000000..b286328 --- /dev/null +++ b/source/alignment.txt @@ -0,0 +1,289 @@ +// Some attempts at generating alignments for GAP - MMT + +// I use "Maybe" to signify that there are not guarantees as to +// what the return +// it I want to keep note of expected return filters. + +BASE_URI = http://www.gap-system.org/lib/ + +// this is not quite a set, because it's "homogeneous" as in things +// in a collection can only be in the same family +// The filter IsListOrCollection is implied by IsCollection (and that +// sohuld also be reflected in the GAP export) +?coll?IsListOrCollection : IsObject -> Bool +?coll?IsCollection : IsObject -> Bool + +// This is more general than groups... +?coll?Size : IsCollection -> Natural or infinity + +// How do we create, say, permutations or matrices? + +// this becomes a permutation group if one lumps permutations +// in +?grp?Group : List Stuff -> Maybe IsGroup + +// GroupWithGenerators, (part of) +// GAP export: +// IsCollection -> Maybe IsGroup +// IsCollection -> IsMultiplicativeElementWithInverse -> Maybe IsGroup +?grp?GroupWithGenerators : IsCollection -> Maybe IsGroup +?grp?GroupWithGenerators : IsCollection -> IsMultiplicativeElementWithInverse -> Maybe IsGroup + + +(Can we query all symbols that come out of the GAP export that have + "IsGroup" as one argument filter? + Things are applicable, like "Size") + +?grp?GeneratorsOfGroup : IsGroup -> IsListOrCollection + +?grp?NaturalHomomorphism : IsGroup -> IsGroup -> IsGroup + +?grp?RationalClasses : IsGroup -> List IsRationalClass + +// This is a generated thing, and a mutable attribute... +?grp?ComputedPRumps : IsGroup -> IsPosInt -> Maybe IsGroup +?grp?PRump : IsGroup -> IsPosInt -> IsGroup + +?grp?IsPSolvable : IsGroup -> IsPosInt -> Bool + + + +?grp?SylowSubgroupOp : IsGroup -> IsPosInt -> IsGroup +?grp?SylowSubgroup : IsGroup -> IsPosInt -> IsGroup + +?grp?Normalizer : IsGroup -> IsGroup -> IsGroup + +?grp?Agemo : IsGroup -> IsPosInt -> IsGroup +?grp?Agemo : IsGroup -> IsPosInt -> IsPosInt -> IsGroup +?grp?AgemoOp : IsGroup -> IsPosInt -> IsGroup + +constant RepresentativesPerfectSubgroups +constant IsomorphismFpGroupByCompositionSeries +constant RightTransversal +constant NormalClosureInParent +constant IsomorphismFpGroupByGeneratorsNC +constant ConjugateSubgroup +constant CanComputeSizeAnySubgroup +constant CanComputeSizeAnySubgroup_st0 +constant IsSolvableGroup +constant NormalClosureOp +constant GrowthFunctionOfGroup +constant IsRightTransversal +constant IsRightTransversal_st0 +constant IsRightTransversal_st1 +constant IsPNilpotentOp +constant RightTransversalInParent +constant IndependentGeneratorsOfAbelianGroup +constant IsRightTransversalRep +constant IsRightTransversalRep_st0 +constant IsRightTransversalRep_st1 +constant IsRightTransversalRep_st2 +constant IsRightTransversalRep_st3 +constant IsRightTransversalRep_st4 +constant ComputedHallSubgroups +constant IsFinitelyGeneratedGroup +constant ConjugateGroup +constant IsPGroup +constant RankPGroup +constant MaximalSubgroups +constant IsConjugate +constant PrefrattiniSubgroup +constant AbelianInvariants +constant IsSubsetLocallyFiniteGroup +constant CosetTableNormalClosure +constant MinimalGeneratingSet +constant HallSystem +constant IsPSolvableOp +constant PrimePowerComponents +constant IsPolycyclicGroup +constant CoreInParent +constant ComplementSystem +constant CommutatorFactorGroup +constant GeneratorsSmallest +constant Index +constant PRumpOp +constant IsSporadicSimpleGroup +constant CosetTable +constant ConjugacyClassesSubgroups +constant OmegaOp +constant IsSubnormal +constant IsAlmostSimpleGroup +constant AsSubgroup +constant IndexInParent +constant ConjugacyClassesPerfectSubgroups +constant KnowsHowToDecompose +constant SylowSystem +constant FrattiniSubgroup +constant IsGroupOfFamily +constant IsomorphismPermGroup +constant JenningsSeries +constant CanEasilyTestMembership +constant DerivedSeriesOfGroup +constant PCore +constant IndexOp +constant IsElementaryAbelian +constant IsomorphismFpGroupBySubnormalSeries +constant IsomorphismFpGroup +constant PCoreOp +constant NormalSubgroups +constant NormalClosure +constant LowIndexSubgroups +constant LargestElementGroup +constant IsNormal +constant RadicalGroup +constant IsMonomialGroup +constant ConjugateSubgroups +constant FactorGroupNC +constant DerivedSubgroup +constant IsCyclic +constant IsCharacteristicSubgroup +constant IsNormalOp +constant ClassMultiplicationCoefficient +constant ComputedPCentralSeriess +constant IndexInWholeGroup +constant CanComputeIndex +constant UpperCentralSeriesOfGroup +constant Exponent +constant IntermediateSubgroups +constant CentralizerModulo +constant MaximalAbelianQuotient +constant SubnormalSeries +constant NrConjugacyClassesInSupergroup +constant Core +constant ElementaryAbelianSeriesLargeSteps +constant MinimalNormalSubgroups +constant LowerCentralSeriesOfGroup +constant NrConjugacyClasses +constant RightTransversalOp +constant HallSubgroupOp +constant Isomorphism +constant ClosureGroup +constant Socle + +constant PowerMapOfGroup + +constant MaximalSubgroupClassReps + +constant NormalIntersection + +constant CommutatorLength + +constant ChiefSeriesThrough + +constant NormalizerOp + +constant ComputedPCores + +constant MaximalNormalSubgroups + +constant LatticeSubgroups + +constant IsSupersolvableGroup + +constant IsomorphismSpecialPcGroup + +constant IsomorphismPcGroup + +constant HirschLength + +constant AsGroup + +constant PCentralSeriesOp + +constant NormalHallSubgroups + +constant PCentralSeries + +constant RepresentativesSimpleSubgroups + +constant ComputedOmegas + +constant IsPNilpotent + +constant SylowComplementOp + +constant GroupByGenerators + +constant ComputedIsPNilpotents + +constant IsNilpotentGroup + +constant CommutatorSubgroup + +constant GroupString + +constant SylowComplement + +constant HallSubgroup + +constant SubnormalSeriesInParent + +constant PerfectResiduum + +constant SmallGeneratingSet + +constant PrimePGroup + +constant ChiefSeries + +constant FittingSubgroup + +constant NormalMaximalSubgroups + +constant CoreOp + +constant CompositionSeries + +constant EulerianFunction + +constant NormalizerInParent + +constant InvariantForm + +constant DerivedLength + +constant NilpotencyClassOfGroup + +constant SubnormalSeriesOp + +constant ElementaryAbelianSeries + +constant SupersolvableResiduum + +constant ConjugacyClassesMaximalSubgroups + +constant IsSimpleGroup + +constant IndexNC + +constant ChiefSeriesUnderAction + +constant IndependentGeneratorExponents + +constant Factorization + +constant IsPerfectGroup + +constant IsomorphismFpGroupByChiefSeries + +constant ConjugacyClasses + +constant IsInfiniteAbelianizationGroup + +constant IsGroupdefinition + +constant PrimePowerComponent + +constant Omega + +constant ComputedIsPSolvables + +constant PClassPGroup + +constant ElementTestFunction + +constant IsNormalInParent + +constant DimensionsLoewyFactors + +constant GroupWithGenerators -- GitLab