[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Call for help
From: |
daly |
Subject: |
[Axiom-developer] Call for help |
Date: |
Sat, 25 Jul 2015 06:38:02 -0500 |
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] Call for help,
daly <=