Re: Axiom musings...

[Tim Daly]

Another thought is that Axiom is "not fully factored". There is
a logic and category theory concept called "the carrier". In
Axiom terms, this is the Rep aka the representation. Axiom
bundles the representation with the domain, which is reasonable.

However, representations are likely data structures with their
own specification, proof, and associated code. So it seems
reasonable to re-factor Axiom to separate the Rep from the
Domain and make it a parameter.

This has the effect of separating data structure proofs from
domain proofs. It also allows the axioms and theorems from
the Rep data structure to be used in domain function proofs.

The category is, as implemented, a "dictionary" of operations.
The SANE version has much more information, including
logical axioms and definitions.

So a domain is actually composed of (at least) 3 parts:

OPS: operations (from the category)
REP: representations (from data structures, aka Rep)
IMP: implementations (in the domain itself)

A domain is OPS x REP x IMP.
A package is OPS x IMP

Note that, as mentioned above, REP can itself be a domain.

The CLOS implementation needs to factor these into
class / instance objects that exist both at compile time
and at run time (since types, including new categories,
can be constucted at run time).

Tim


On 1/1/21, Tim Daly <axiomcas@gmail.com> wrote:
> One of the struggles of working with first-class dependent types
> is that they can be created "on the fly". Ideally, when used, the
> type information can be "factored out" to yield a specialized
> version that is more efficient. The idea is best described in a
> book, called Partial Evaluation, which used the type information
> to collapse and specialize a function.
>
> Jones, Gomard, and Sestoft "Partial Evaluation and Automatic
> Program Generation" (1993) Prentice Hall
>
>
> On 12/31/20, Tim Daly <axiomcas@gmail.com> wrote:
>> It's been a long, slow effort to "get up to speed" (or more
>> accurately "a slow crawl") on the various subjects one needs
>> to know to work on "computational mathematics" aka SANE.
>>
>> A reading knowledge of a lot of areas is needed, including
>> things like
>>
>> abstract algebra (to understand Axiom's category/domain)
>> type theory (to understand first-order dependent types)
>> proof theory (to understand Gentzen, sequents, etc.)
>> category theory (to understand catamorphs, functors, etc.)
>> metaobject protocol (to understand CLOS extensions)
>> number theory (to understand finite fields)
>> calculus (to understand field extensions for integration)
>> programming (to understand typeclasses, CLOS, etc)
>> philosophy (to understand polymorphic sets, etc)
>> CPU hardware (to understand "down to the metal", FPGA, etc.)
>> Specification (to understand consistancy, completness, etc)
>> Verification (to understand decision procedures, etc)
>> Proof tools (like Coq, Lean, etc.)
>>
>> and a few other subjects that won't come to mind at the
>> moment.
>>
>> The usual academic approach, that creates a special
>> "course of study", requiring classes in areas is probably
>> best. There are a lot of good online courses, such as
>> the UOregon summer school, that introduce the basic
>> ideas clearly. There are some good introductory books
>> like Troelstra and Schwichtenberg's "Basic Proof Theory"
>> that cover Gentsen, Hilbert, and Natural Deduction ideas.
>>
>> It seems worthwhile to put together a full course of study
>> with links to videos and books, so one can get up to speed
>> on required knowledge. I'll start an outline with links to
>> these on the axiom-developer.org website in the coming
>> weeks. It's sort-of an "Axiom University" major in
>> computational mathematics.
>>
>> (There are no degrees :-) But one does mathematics and
>> programming for the joy of it anyway so who cares?)
>>
>> I welcome suggestions and online links.
>>
>> Tim
>>
>