Re: Axiom musings...

[Tim Daly]

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