Elixir LiveView offers a nice way to interact with the br=
owser. I=E2=80=99ve been playing rendering OpenAI Atari frames from their P=
ython objects (using erlport), so it seems like a plausible option for inte=
racting 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:

I'm experimenting with a browser front end that has an Axiom

editor that runs Axiom in the background. This isn't really

Using the = browser has the advantage of integrating the

compiler, interpreter, = graphics, and documentation in one

interface.

I manag= ed to get the editor-in-browser working.

Axiom already has a= browser connection (book volume 11)

designed to replace hyperdoc an= d 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=3DoyLBGkS= 5ICk

> which, like all of Hickey's talks, is worth watchi= ng.

>

> He talks about programs breaking due to things = like

> library changes. Around minute 30 he started to talk

>

> I realized this years ago an= d changed Axiom to use

> the date of the release. It provides the= same sort of

> "non-information" but it is easy to fin= d in the changelog.

>

> Tim

>

>

=

> On 9/5/20, Tim Daly <axiomcas@gmail.com> wrote:

>> Geometric a= lgebra 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 c= hanging BLAS to use

>> John Gustafson's UNUM representatio= n, which eliminates a lot

>> of code because various "sta= ndard errors" cannot occur. See

>> his book "The End= Of Error"

>> https://www.amazon.com/End-Error-Computing-Chapman-Computationa= l/dp/1482239868

>>

>> But since Geometric alg= ebra is coordinate free, many of the

>> computations can be do= ne symbolically and then evalulated

>> in final form.

&= gt;>

>> BLAS re-caste in Geometric Algebra means that some = of the

>> errors, such as roundoff, cannot occur in the symbol= ic form.

>>

>> This has the potential to make Axi= om's BLAS and LAPACK

>> computations faster and more accur= ate.

>>

>> Tim

>>

>>

>> On 9/5/20, Tim Daly <axiomcas@gmail.com> wrote:

>>> I&= #39;m in the process of re-architecting Axiom, of course.

>>&g= t;

>>> The primary research effort, as you know, is incorpo= rating

>>> proof technology.

>>>

>= ;>> But in the process of re-architecting there are more things

>>>

>>> One concern is "G= eometric Algebra". See

>>> http://geometricalgebra.= net/

>>> https://www.youtube.com/watch?v=3D0fF2xToQmgs&list= =3DPLsSPBzvBkYjzcQ4eCVAntETNNVD2d5S79

>>>

>&g= t;> Geometric algebra unifies a lot of mathematics. In particular,

>>> representation. This greatly simpli= fies and unifies a lot of

>>> mathematics.

>>&= gt;

>>> So the question becomes, can this be used to "= re-represent"

>>> Axiom mathematics dependent on linea= r algebra? I don't

>>> know but the idea has a lot of p= otential for simplification.

>>>

>>>

>>> The second concern is "Category Theory". This theor= y

>>> provides a simplification and a generalization of var= ious

>>> ideas in Axiom. It also puts constraints on things= like an

>>> Axiom "category" to Axiom "cate= gory" functors so that the

>>> conversion preserves th= e mathematical "Category"

>>> structure and prope= rties.

>>>

>>> MIT has a "course"= on "Programming with Categories"

>>> https://www.youtube.com/playlist?list= =3DPLhgq-BqyZ7i7MTGhUROZy3BOICnVixETS

>>> which makes t= hings rather more understandable.

>>>

>>> S= o 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

<= br>>>> Theory with Type Theory with Proof Theory with Category

=

>>> Theory.

>>>

>>> Getting al= l of this "aligned" (and hopefully reasonably

>>>= correct) will give Axiom a solid mathematical foundation.

>>&= gt;

>>> Mathematics has changed a lot since Axiom was creat= ed

>>> and many of those changes have shown that we need a<= br>

>>> much stronger basis for ad-hoc things like coercion, et= c.

>>>

>>>

>>> Tim

&= gt;>>

>>>

>>> On 8/21/20, Tim Daly &l= t;axiomcas@gmail.co= m> wrote:

>>>> A briliant essay:

>>&= gt;>

>>>> In exactly the same way a small change in a= xioms

>>>> (of which we cannot be completely sure) is ca= pable,

>>>> generally speaking, of leading to completely= different

>>>> conclusions than those that are obtained= from theorems

>>>> which have been deduced from the acc= epted axioms.

>>>> The longer and fancier is the chain o= f deductions

>>>> ("proofs"), the less reliabl= e 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 effo= rt (so far).

>>>>>

>>>>> First,= the focus is on the GCD in NonNegativeInteger.

>>>>>= Volume 13 is basically a collection of published thoughts

>>&= gt;>> by various authors on the GCD, a background literature

&= gt;>>>> search. Build a limited system with essentially one use= r

>>>>> visible function (the NNI GCD) and implement = all of the

>>>>> ideas there. This demonstrates inher= itance of axioms,

>>>>> specification of functions, p= re- and post-conditions,

>>>>> proof integration, pro= visos, the new compiler, etc.

>>>>>

>>&g= t;>> Second, make the SANE GCD work in the current Axiom

>&= gt;>>> system by generating compatible code. This gives a

&= gt;>>>> stepping-stone approach where things can be grounded.

>>>>> Obviously none of the new proof ideas will be ex= pected

>>>>> to work in the current system but it &qu= ot;gives a place to stand".

>>>>>

>>= ;>>> Third, develop a lattice of functions. The idea is to attack = the

>>>>> functions that=C2=A0 depend on almost nothi= ng, prove them correct,

>>>>> and use them to prove f= unctions that only depend on the

>>>>> prior layer. I= did this with the category structure when I first

>>>>&= gt; 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 severa= l months

>>>>> so I expect that function-lattice to t= ake about the same time.

>>>>>

>>>>= ;> This makes the research "incremental" so that a result can<= br>

>>>>> be achieved in one lifetime. Like a PhD thesis,= it is initially

>>>>> intended as a small step forwa= rd but still be a valid instance

>>>>> of "compu= tational mathematics", deeply combining proof and

>>>&= gt;> computer algebra.

>>>>>

>>>&g= t;> Tim

>>>>>

>>>>

>&= gt;>

>>

>

Ricardo Corral C.

-------------------------------------------= -

--000000000000d9acca05b0089157--
From MAILER-DAEMON Thu Sep 24 03:29:04 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1kLLge-00018a-O3
for mharc-axiom-developer@gnu.org; Thu, 24 Sep 2020 03:29:04 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:39902)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from -------------------------------------------= -