Re: [EXTERNAL] Re: Axiom musings...

[Tim Daly]

No, the name 'Axiom" is used by many different companies.

Trademarks only cover infringement "in the same area"
(although the Lexus car company sued a diner named
Lexus and "won" because the diner couldn't compete
against big corporate lawyer money).

One company in New Jersey named their language "Axiom"
and I keep getting calls from recruiters because that company
will pay big bucks to hire an "Axiom Developer". Sigh.

I just thought the space one was "over the top".

I'd sign up to go to space in a heartbeat.
I applied to be an astronaut in the 1990s. NASA
wanted someone with at least a Master's degree,
a background in Robotics, and less than 5'9" tall.
I fit the criteria but never heard back.

Tim







On 9/25/20, William Sit <wsit@ccny.cuny.edu> wrote:
> Axiom Space, a Houston-based company, is not related to Axiom the scientific
> computation system. Or is it?
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> ________________________________________
> From: Axiom-developer
> <axiom-developer-bounces+wyscc=sci.ccny.cuny.edu@nongnu.org> on behalf of
> Tim Daly <axiomcas@gmail.com>
> Sent: Thursday, September 24, 2020 4:26 AM
> To: Ricardo Corral C.
> Cc: axiom-developer@nongnu.org
> Subject: [EXTERNAL] Re: Axiom musings...
>
> Today's Headline:
>
> Axiom finalizing agreements for private astronaut mission to space station
>
> https://urldefense.proofpoint.com/v2/url?u=https-3A__spaceflightnow.com_2020_09_23_axiom-2Dfinalizing-2Dagreements-2Dfor-2Dprivate-2Dastronaut-2Dmission-2Dto-2Dspace-2Dstation_&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=AvUAZpZ9vnJiQ37yQyMSdNeJQH8qv3HLt5_V1qQ3q2g&e=
>
> Wow. I HAVE been busy :-)
>
> Tim
>
>
> On 9/24/20, Tim Daly <axiomcas@gmail.com> wrote:
>> Ricardo,
>>
>> Yes, I'm familar with Sage. Axiom was originally connected
>> back around 2006 / 2007. William Stein showed me that it
>> runs fine in the latest version.
>>
>> Unfortunately it doesn't do all of the things Axiom supports.
>>
>> I will look at Elixer LiveView. Thanks.
>>
>> Tim
>>
>>
>> On 9/24/20, Ricardo Corral C. <ricardocorralc@gmail.com> wrote:
>>> Elixir LiveView offers a nice way to interact with the browser. I’ve been
>>> playing rendering OpenAI Atari frames from their Python objects (using
>>> erlport), so it seems like a plausible option for interacting with axiom
>>> too. Note that sagemath.org already interacts with axiom, so maybe
>>> connecting through it serves like a bridge.
>>>
>>> On Thu 24 Sep 2020 at 0:06 Tim Daly <axiomcas@gmail.com> wrote:
>>>
>>>> The new Axiom version needs to have a better user interface.
>>>>
>>>>
>>>>
>>>> I'm experimenting with a browser front end that has an Axiom
>>>>
>>>> editor that runs Axiom in the background. This isn't really
>>>>
>>>> a new idea. Maxima has been doing it for years.
>>>>
>>>>
>>>>
>>>> Using the browser has the advantage of integrating the
>>>>
>>>> compiler, interpreter, graphics, and documentation in one
>>>>
>>>> interface.
>>>>
>>>>
>>>>
>>>> I managed to get the editor-in-browser working.
>>>>
>>>>
>>>>
>>>> Axiom already has a browser connection (book volume 11)
>>>>
>>>> designed to replace hyperdoc and working as an
>>>>
>>>> interpreter I/O so this editor would be an extension.
>>>>
>>>>
>>>>
>>>> Since almost all of Axiom is already in hyperlinked PDF
>>>>
>>>> files it will be possible to jump directly to related sections
>>>>
>>>> in the various books.
>>>>
>>>>
>>>>
>>>> Tim
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> On 9/23/20, Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>> > Rich Hickey gave a keynote:
>>>>
>>>> > https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtube.com_watch-3Fv-3DoyLBGkS5ICk&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=oF9rfp-E-CqJ8LCcpq87aURaYtjVP8DwSljlOvjZUFw&e=
>>>>
>>>> > which, like all of Hickey's talks, is worth watching.
>>>>
>>>> >
>>>>
>>>> > He talks about programs breaking due to things like
>>>>
>>>> > library changes. Around minute 30 he started to talk
>>>>
>>>> > about why "semantic versioning" (e.g. version 1.2.3)
>>>>
>>>> > is meaningless.
>>>>
>>>> >
>>>>
>>>> > I realized this years ago and changed Axiom to use
>>>>
>>>> > the date of the release. It provides the same sort of
>>>>
>>>> > "non-information" but it is easy to find in the changelog.
>>>>
>>>> >
>>>>
>>>> > Tim
>>>>
>>>> >
>>>>
>>>> >
>>>>
>>>> > On 9/5/20, Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>> >> Geometric algebra also affects another "in-process" goal.
>>>>
>>>> >>
>>>>
>>>> >> I have BLAS and LAPACK in the Axiom sources (volume 10.5).
>>>>
>>>> >>
>>>>
>>>> >> I've spent some time on the question of changing BLAS to use
>>>>
>>>> >> John Gustafson's UNUM representation, which eliminates a lot
>>>>
>>>> >> of code because various "standard errors" cannot occur. See
>>>>
>>>> >> his book "The End Of Error"
>>>>
>>>> >>
>>>> https://urldefense.proofpoint.com/v2/url?u=https-3A__www.amazon.com_End-2DError-2DComputing-2DChapman-2DComputational_dp_1482239868&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=yWXuK9IV2lgeUVht6IFybABGGvhsgr0zuqsb6jwFr-4&e=
>>>>
>>>> >>
>>>>
>>>> >> But since Geometric algebra is coordinate free, many of the
>>>>
>>>> >> computations can be done symbolically and then evalulated
>>>>
>>>> >> in final form.
>>>>
>>>> >>
>>>>
>>>> >> BLAS re-caste in Geometric Algebra means that some of the
>>>>
>>>> >> errors, such as roundoff, cannot occur in the symbolic form.
>>>>
>>>> >>
>>>>
>>>> >> This has the potential to make Axiom's BLAS and LAPACK
>>>>
>>>> >> computations faster and more accurate.
>>>>
>>>> >>
>>>>
>>>> >> Tim
>>>>
>>>> >>
>>>>
>>>> >>
>>>>
>>>> >> On 9/5/20, Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>> >>> I'm in the process of re-architecting Axiom, of course.
>>>>
>>>> >>>
>>>>
>>>> >>> The primary research effort, as you know, is incorporating
>>>>
>>>> >>> proof technology.
>>>>
>>>> >>>
>>>>
>>>> >>> But in the process of re-architecting there are more things
>>>>
>>>> >>> to consider. Two of them are "front and center" at the moment.
>>>>
>>>> >>>
>>>>
>>>> >>> One concern is "Geometric Algebra". See
>>>>
>>>> >>> https://urldefense.proofpoint.com/v2/url?u=http-3A__geometricalgebra.net_&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=ZSIE2k7gRluHIWuMRbAKuxvuEhNW5fsAY_7JkHIt_6Y&e=
>>>>
>>>> >>>
>>>> https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtube.com_watch-3Fv-3D0fF2xToQmgs-26list-3DPLsSPBzvBkYjzcQ4eCVAntETNNVD2d5S79&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=ajUPImTLlq7Lp3ZyQySQVbWMzGahjwqMv3VbbDADxyc&e=
>>>>
>>>> >>>
>>>>
>>>> >>> Geometric algebra unifies a lot of mathematics. In particular,
>>>>
>>>> >>> it "cleans up" linear algebra, creating a "coordinate-free"
>>>>
>>>> >>> representation. This greatly simplifies and unifies a lot of
>>>>
>>>> >>> mathematics.
>>>>
>>>> >>>
>>>>
>>>> >>> So the question becomes, can this be used to "re-represent"
>>>>
>>>> >>> Axiom mathematics dependent on linear algebra? I don't
>>>>
>>>> >>> know but the idea has a lot of potential for simplification.
>>>>
>>>> >>>
>>>>
>>>> >>>
>>>>
>>>> >>> The second concern is "Category Theory". This theory
>>>>
>>>> >>> provides a simplification and a generalization of various
>>>>
>>>> >>> ideas in Axiom. It also puts constraints on things like an
>>>>
>>>> >>> Axiom "category" to Axiom "category" functors so that the
>>>>
>>>> >>> conversion preserves the mathematical "Category"
>>>>
>>>> >>> structure and properties.
>>>>
>>>> >>>
>>>>
>>>> >>> MIT has a "course" on "Programming with Categories"
>>>>
>>>> >>>
>>>> https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtube.com_playlist-3Flist-3DPLhgq-2DBqyZ7i7MTGhUROZy3BOICnVixETS&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=wAlbj134BiwAcAdG60K3dYfrkb5lDwA7M0swRlmjAU8&e=
>>>>
>>>> >>> which makes things rather more understandable.
>>>>
>>>> >>>
>>>>
>>>> >>> So one question is how to re-represent Axiom's type
>>>>
>>>> >>> structure so that it has a correct mathematical "Category"
>>>>
>>>> >>> structure. This, of course, raises the question of Group
>>>>
>>>> >>> Theory with Type Theory with Proof Theory with Category
>>>>
>>>> >>> Theory.
>>>>
>>>> >>>
>>>>
>>>> >>> Getting all of this "aligned" (and hopefully reasonably
>>>>
>>>> >>> correct) will give Axiom a solid mathematical foundation.
>>>>
>>>> >>>
>>>>
>>>> >>> Mathematics has changed a lot since Axiom was created
>>>>
>>>> >>> and many of those changes have shown that we need a
>>>>
>>>> >>> much stronger basis for ad-hoc things like coercion, etc.
>>>>
>>>> >>>
>>>>
>>>> >>>
>>>>
>>>> >>> Tim
>>>>
>>>> >>>
>>>>
>>>> >>>
>>>>
>>>> >>> On 8/21/20, Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>> >>>> A briliant essay:
>>>>
>>>> >>>>
>>>>
>>>> >>>> In exactly the same way a small change in axioms
>>>>
>>>> >>>> (of which we cannot be completely sure) is capable,
>>>>
>>>> >>>> generally speaking, of leading to completely different
>>>>
>>>> >>>> conclusions than those that are obtained from theorems
>>>>
>>>> >>>> which have been deduced from the accepted axioms.
>>>>
>>>> >>>> The longer and fancier is the chain of deductions
>>>>
>>>> >>>> ("proofs"), the less reliable is the final result.
>>>>
>>>> >>>>
>>>>
>>>> >>>> https://urldefense.proofpoint.com/v2/url?u=https-3A__www.uni-2Dmuenster.de_Physik.TP_-7Emunsteg_arnold.html&d=DwIFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8&s=b11uIoYmlhACkj0JDy8Bbl3aTCMbW6OC_caxDDDN2YU&e=
>>>>
>>>> >>>>
>>>>
>>>> >>>>
>>>>
>>>> >>>> On 8/8/20, Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>> >>>>> Mark,
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> You're right, of course. The problem is too large.
>>>>
>>>> >>>>> So what. is the plan to achieve a research result?
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> There are 3 major restrictions on the effort (so far).
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> First, the focus is on the GCD in NonNegativeInteger.
>>>>
>>>> >>>>> Volume 13 is basically a collection of published thoughts
>>>>
>>>> >>>>> by various authors on the GCD, a background literature
>>>>
>>>> >>>>> search. Build a limited system with essentially one user
>>>>
>>>> >>>>> visible function (the NNI GCD) and implement all of the
>>>>
>>>> >>>>> ideas there. This demonstrates inheritance of axioms,
>>>>
>>>> >>>>> specification of functions, pre- and post-conditions,
>>>>
>>>> >>>>> proof integration, provisos, the new compiler, etc.
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> Second, make the SANE GCD work in the current Axiom
>>>>
>>>> >>>>> system by generating compatible code. This gives a
>>>>
>>>> >>>>> stepping-stone approach where things can be grounded.
>>>>
>>>> >>>>> Obviously none of the new proof ideas will be expected
>>>>
>>>> >>>>> to work in the current system but it "gives a place to stand".
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> Third, develop a lattice of functions. The idea is to attack the
>>>>
>>>> >>>>> functions that  depend on almost nothing, prove them correct,
>>>>
>>>> >>>>> and use them to prove functions that only depend on the
>>>>
>>>> >>>>> prior layer. I did this with the category structure when I first
>>>>
>>>> >>>>> got the system since it was necessary to bootstrap Axiom
>>>>
>>>> >>>>> without a running system (something that was not possible
>>>>
>>>> >>>>> with the IBM/NAG version). That effort took several months
>>>>
>>>> >>>>> so I expect that function-lattice to take about the same time.
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> This makes the research "incremental" so that a result can
>>>>
>>>> >>>>> be achieved in one lifetime. Like a PhD thesis, it is initially
>>>>
>>>> >>>>> intended as a small step forward but still be a valid instance
>>>>
>>>> >>>>> of "computational mathematics", deeply combining proof and
>>>>
>>>> >>>>> computer algebra.
>>>>
>>>> >>>>>
>>>>
>>>> >>>>> Tim
>>>>
>>>> >>>>>
>>>>
>>>> >>>>
>>>>
>>>> >>>
>>>>
>>>> >>
>>>>
>>>> >
>>>>
>>>>
>>>>
>>>> --
>>> Ricardo Corral C.
>>> --------------------------------------------
>>>
>>
>
>