[Axiom-developer] Call for help

[daly]

Axiom has moved into a new phase. The goal is to prove Axiom correct.

There are several tools and several levels of proof. I've added
the machinery to run proofs in COQ (for algebra) and ACL2 (for
the interpreter and compiler).

One of the first steps for the algebra proofs involves decorating
the categories with their mathematical axioms. That's where I am
asking for your help.

There are 241 categories, such as Monoid, which need to be annotated.
I've listed them below, sorted in the order by which they inherit
from prior categories, so that the complexity increases. The file
http://axiom-developer.org/axiom-website/endpaper.pdf
has a graph of the categories from the Jenks book which could be
a great help.

Please look at the categories and find or create the axioms.
If you have a particularly good reference page on the web or
a particularly good book that lists them, please let me know.

The axioms have to be in a certain form so they can be used in
the calculus of inductive constructions (the theory behind COQ).

The plan is to decorate the categories, then provide proofs for
category-default code. Unfortunately, Axiom is circular so some
of the domains are going to require proofs also. 

This task should be at least as hard as it was to get Axiom to
build stand-alone in the first place which took about a year.
The best case will be that the implementations are proven correct.
The bad case will be corner cases where the implementation cannot
be proven.

In any case, your help will make this first step easier. Drag out
your favorite reference book and decorate LeftModule :-).

Thanks,
Tim

==================================================================

ATADDVA AdditiveValuationAttribute
ATAPPRO ApproximateAttribute
ATARBEX ArbitraryExponentAttribute
ATARBPR ArbitraryPrecisionAttribute
AHYP    ArcHyperbolicFunctionCategory
ATRIG   ArcTrigonometricFunctionCategory
ATTREG  AttributeRegistry
BASTYPE BasicType
ATCANON CanonicalAttribute
ATCANCL CanonicalClosedAttribute
ATCUNOR CanonicalUnitNormalAttribute
ATCENRL CentralAttribute
KOERCE  CoercibleTo
CFCAT   CombinatorialFunctionCategory
ATCS    CommutativeStarAttribute
KONVERT ConvertibleTo
ELEMFUN ElementaryFunctionCategory
ELTAB   Eltable
ATFINAG FiniteAggregateAttribute
HYPCAT  HyperbolicFunctionCategory
IEVALAB InnerEvalable
ATJACID JacobiIdentityAttribute
ATLR    LazyRepresentationAttribute
ATLUNIT LeftUnitaryAttribute
MAGCDOC ModularAlgebraicGcdOperations
ATMULVA MultiplicativeValuationAttribute
ATNOTHR NotherianAttribute
ATNZDIV NoZeroDivisorsAttribute
ATNULSQ NullSquareAttribute
OM      OpenMath
ATPOSET PartiallyOrderedSetAttribute
PTRANFN PartialTranscendentalFunctions
PATAB   Patternable
PRIMCAT PrimitiveFunctionCategory
RADCAT  RadicalCategory
RETRACT RetractableTo
ATRUNIT RightUnitaryAttribute
ATSHMUT ShallowlyMutableAttribute
SPFCAT  SpecialFunctionCategory
TRIGCAT TrigonometricFunctionCategory
TYPE    Type
ATUNIKN UnitsKnownAttribute
AGG     Aggregate
COMBOPC CombinatorialOpsCategory
COMPAR  Comparable
ELTAGG  EltableAggregate
EVALAB  Evalable
FORTCAT FortranProgramCategory
FRETRCT FullyRetractableTo
FPATMAB FullyPatternMatchable
LOGIC   Logic
PPCURVE PlottablePlaneCurveCategory
PSCURVE PlottableSpaceCurveCategory
REAL    RealConstant
SEGCAT  SegmentCategory
SETCAT  SetCategory
TRANFUN TranscendentalFunctionCategory
ABELSG  AbelianSemiGroup
BLMETCT BlowUpMethodCategory
DSTRCAT DesingTreeCategory
FORTFN  FortranFunctionCategory
FMC     FortranMatrixCategory
FMFUN   FortranMatrixFunctionCategory
FVC     FortranVectorCategory
FVFUN   FortranVectorFunctionCategory
FEVALAB FullyEvalableOver
FILECAT FileCategory
FINITE  Finite
FNCAT   FileNameCategory
GRMOD   GradedModule
LORER   LeftOreRing
HOAGG   HomogeneousAggregate
IDPC    IndexedDirectProductCategory
LFCAT   LiouvillianFunctionCategory
MONAD   Monad
NUMINT  NumericalIntegrationCategory
OPTCAT  NumericalOptimizationCategory
ODECAT  OrdinaryDifferentialEquationsSolverCategory
ORDSET  OrderedSet
PDECAT  PartialDifferentialEquationsSolverCategory
PATMAB  PatternMatchable
RRCC    RealRootCharacterizationCategory
SEGXCAT SegmentExpansionCategory
SGROUP  SemiGroup
SETCATD SetCategoryWithDegree
SEXCAT  SExpressionCategory
STEP    StepThrough
SPACEC  ThreeSpaceCategory
ABELMON AbelianMonoid
AFSPCAT AffineSpaceCategory
BGAGG   BagAggregate
CACHSET CachableSet
CLAGG   Collection
DVARCAT DifferentialVariableCategory
ES      ExpressionSpace
GRALG   GradedAlgebra
IXAGG   IndexedAggregate
MONADWU MonadWithUnit
MONOID  Monoid
ORDFIN  OrderedFinite
PLACESC PlacesCategory
PRSPCAT ProjectiveSpaceCategory
RCAGG   RecursiveAggregate
ARR2CAT TwoDimensionalArrayCategory
BRAGG   BinaryRecursiveAggregate
CABMON  CancellationAbelianMonoid
DIOPS   DictionaryOperations
DLAGG   DoublyLinkedAggregate
GROUP   Group
LNAGG   LinearAggregate
MATCAT  MatrixCategory
OASGP   OrderedAbelianSemiGroup
ORDMON  OrderedMonoid
PSETCAT PolynomialSetCategory
PRQAGG  PriorityQueueAggregate
QUAGG   QueueAggregate
SETAGG  SetAggregate
SKAGG   StackAggregate
URAGG   UnaryRecursiveAggregate
ABELGRP AbelianGroup
BTCAT   BinaryTreeCategory
DIAGG   Dictionary
DQAGG   DequeueAggregate
ELAGG   ExtensibleLinearAggregate
FLAGG   FiniteLinearAggregate
FAMONC  FreeAbelianMonoidCategory
MDAGG   MultiDictionary
OAMON   OrderedAbelianMonoid
PERMCAT PermutationCategory
STAGG   StreamAggregate
TSETCAT TriangularSetCategory
FDIVCAT FiniteDivisorCategory
FSAGG   FiniteSetAggregate
KDAGG   KeyedDictionary
LZSTAGG LazyStreamAggregate
LMODULE LeftModule
LSAGG   ListAggregate
MSETAGG MultisetAggregate
NARNG   NonAssociativeRng
A1AGG   OneDimensionalArrayAggregate
OCAMON  OrderedCancellationAbelianMonoid
RSETCAT RegularTriangularSetCategory
RMODULE RightModule
RNG     Rng
BMODULE BiModule
BTAGG   BitAggregate
NASRING NonAssociativeRing
NTSCAT  NormalizedTriangularSetCategory
OAGROUP OrderedAbelianGroup
OAMONS  OrderedAbelianMonoidSup
OMSAGG  OrderedMultisetAggregate
RING    Ring
SFRTCAT SquareFreeRegularTriangularSetCategory
SRAGG   StringAggregate
TBAGG   TableAggregate
VECTCAT VectorCategory
ALAGG   AssociationListAggregate
CHARNZ  CharacteristicNonZero
CHARZ   CharacteristicZero
COMRING CommutativeRing
DIFRING DifferentialRing
ENTIRER EntireRing
FMCAT   FreeModuleCat
LALG    LeftAlgebra
LINEXP  LinearlyExplicitRingOver
MODULE  Module
ORDRING OrderedRing
PDRING  PartialDifferentialRing
PTCAT   PointCategory
RMATCAT RectangularMatrixCategory
SNTSCAT SquareFreeNormalizedTriangularSetCategory
STRICAT StringCategory
OREPCAT UnivariateSkewPolynomialCategory
XALG    XAlgebra
ALGEBRA Algebra
DIFEXT  DifferentialExtension
FLINEXP FullyLinearlyExplicitRingOver
LIECAT  LieAlgebra
LODOCAT LinearOrdinaryDifferentialOperatorCategory
NAALG   NonAssociativeAlgebra
VSPACE  VectorSpace
XFALG   XFreeAlgebra
DIRPCAT DirectProductCategory
DIVRING DivisionRing
FINAALG FiniteRankNonAssociativeAlgebra
FLALG   FreeLieAlgebra
INTDOM  IntegralDomain
MLO     MonogenicLinearOperator
OC      OctonionCategory
QUATCAT QuaternionCategory
SMATCAT SquareMatrixCategory
XPOLYC  XPolynomialsCat
AMR     AbelianMonoidRing
FMTC    FortranMachineTypeCategory
FRNAALG FramedNonAssociativeAlgebra
GCDDOM  GcdDomain
OINTDOM OrderedIntegralDomain
FAMR    FiniteAbelianMonoidRing
INTCAT  IntervalCategory
PSCAT   PowerSeriesCategory
PID     PrincipalIdealDomain
UFD     UniqueFactorizationDomain
DIVCAT  DivisorCategory
EUCDOM  EuclideanDomain
MTSCAT  MultivariateTaylorSeriesCategory
PFECAT  PolynomialFactorizationExplicit
UPSCAT  UnivariatePowerSeriesCategory
FIELD   Field
INS     IntegerNumberSystem
LOCPOWC LocalPowerSeriesCategory
PADICCT PAdicIntegerCategory
POLYCAT PolynomialCategory
UTSCAT  UnivariateTaylorSeriesCategory
ACF     AlgebraicallyClosedField
DPOLCAT DifferentialPolynomialCategory
FPC     FieldOfPrimeCharacteristic
FINRALG FiniteRankAlgebra
FS      FunctionSpace
INFCLCT InfinitlyClosePointCategory
PACPERC PseudoAlgebraicClosureOfPerfectFieldCategory
QFCAT   QuotientFieldCategory
RCFIELD RealClosedField
RNS     RealNumberSystem
RPOLCAT RecursivePolynomialCategory
ULSCAT  UnivariateLaurentSeriesCategory
UPXSCAT UnivariatePuiseuxSeriesCategory
UPOLYC  UnivariatePolynomialCategory
ACFS    AlgebraicallyClosedFunctionSpace
XF      ExtensionField
FFIELDC FiniteFieldCategory
FPS     FloatingPointSystem
FRAMALG FramedAlgebra
PACFFC  PseudoAlgebraicClosureOfFiniteFieldCategory
ULSCCAT UnivariateLaurentSeriesConstructorCategory
UPXSCCA UnivariatePuiseuxSeriesConstructorCategory
FAXF    FiniteAlgebraicExtensionField
MONOGEN MonogenicAlgebra
PACRATC PseudoAlgebraicClosureOfRationalNumberCategory
COMPCAT ComplexCategory
FFCAT   FunctionFieldCategory
PACEXTC PseudoAlgebraicClosureOfAlgExtOfRationalNumberCategory