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 _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
