Re: [Axiom-developer] Call for help

[Raymond Rogers]

You will have to excuse me if I dozed off in the back seat during the trip.
Is this where we are?
We have a programming language (say SPAD or lisp) and a program in that 
language represented by a series of statements.
The intent is to construct, in a literate manner, a series of statements 
in MPL and SPAD that are flagged and readable by the respective 
compilers such that if the MPL statements are logically correct 
(assertions match conclusions) then SPAD will also reach the same 
conclusions as you stated in MPL.  Presumably that is also done by  MPL 
via a dictionary or some such.
For instance in Left Module Construction the assertions are equivalent 
to a triple F: (R(\cdot , +),G(+),RxG->G(+) and the base qualification is:
R is a ring
G is a group
RxG is legitimate map from R,G to G
etc...
And fail (hopefully informatively) if one of these fails
or Return a construct that has all of the functional properties of Left 
Modules.

Now the literate program has a "model" of Left Module in MPL and then 
checks the SPAD code to see if it correctly does all the of the above 
checks.  If you have done all that then it seems to me that there should 
also be a "hook" that check my custom code as well; of course that 
should be optional and only done when required.  And requires that I can 
define my expectations for my code (which unfortunately I sometimes can't).

Forgive any ignorance but I left off back in the 80's with a Sandia (I 
think) formalism to check the correctness of code.  That is: make 
assertions about what the code will do with the input and verify that 
the code does that.  To give credit this was supposed to be done by 
first order predicate expressions that can be verified.

I would appreciate constructive corrections and suggestions.
Ray



On 07/25/2015 07:38 AM, address@hidden wrote:
> 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
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer

--
 Two views on life:
life is an art not to be learned by observation.
George Santayana:Interpretations of Poetry and Religion
It's kinda nice to participate in your life
Raymond Rogers