[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Call for help

From: Raymond Rogers
Subject: Re: [Axiom-developer] Call for help
Date: Sat, 25 Jul 2015 10:55:45 -0400
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.8.0

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
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.

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
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 :-).



ATADDVA AdditiveValuationAttribute
ATAPPRO ApproximateAttribute
ATARBEX ArbitraryExponentAttribute
ATARBPR ArbitraryPrecisionAttribute
AHYP    ArcHyperbolicFunctionCategory
ATRIG   ArcTrigonometricFunctionCategory
ATTREG  AttributeRegistry
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
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
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

 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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]