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