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