Re: Axiom musings...

[Tim Daly]

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