[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [EXTERNAL] Re: Axiom musings...
From: |
William Sit |
Subject: |
Re: [EXTERNAL] Re: Axiom musings... |
Date: |
Fri, 25 Sep 2020 21:58:16 +0000 |
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.
>> --------------------------------------------
>>
>
- Re: Axiom musings..., Tim Daly, 2020/09/05
- Re: Axiom musings..., Tim Daly, 2020/09/05
- Re: Axiom musings..., Tim Daly, 2020/09/23
- Re: Axiom musings..., Tim Daly, 2020/09/24
- Re: Axiom musings..., Ricardo Corral C., 2020/09/24
- Re: Axiom musings..., Tim Daly, 2020/09/24
- Re: Axiom musings..., Tim Daly, 2020/09/24
- Re: [EXTERNAL] Re: Axiom musings...,
William Sit <=
- Re: [EXTERNAL] Re: Axiom musings..., Tim Daly, 2020/09/25
- Axiom musings..., Tim Daly, 2020/09/28
- Message not available
- Re: Axiom musings..., Tim Daly, 2020/09/28