Re: Axiom musings...

[Tim Daly]

Today's Headline:

Axiom finalizing agreements for private astronaut mission to space station

https://spaceflightnow.com/2020/09/23/axiom-finalizing-agreements-for-private-astronaut-mission-to-space-station/

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://www.youtube.com/watch?v=oyLBGkS5ICk
>>>
>>> > 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://www.amazon.com/End-Error-Computing-Chapman-Computational/dp/1482239868
>>>
>>> >>
>>>
>>> >> 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
>>>
>>> >>> http://geometricalgebra.net/
>>>
>>> >>>
>>> https://www.youtube.com/watch?v=0fF2xToQmgs&list=PLsSPBzvBkYjzcQ4eCVAntETNNVD2d5S79
>>>
>>> >>>
>>>
>>> >>> 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://www.youtube.com/playlist?list=PLhgq-BqyZ7i7MTGhUROZy3BOICnVixETS
>>>
>>> >>> 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://www.uni-muenster.de/Physik.TP/~munsteg/arnold.html
>>>
>>> >>>>
>>>
>>> >>>>
>>>
>>> >>>> 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.
>> --------------------------------------------
>>
>