[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
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
- [Axiom-developer] Call for help, daly, 2015/07/25
- Re: [Axiom-developer] Call for help, daly, 2015/07/25
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/27