[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Embedding Axiom

From: Tim Daly
Subject: Re: [Axiom-developer] Embedding Axiom
Date: Mon, 16 Nov 2009 18:19:28 -0500
User-agent: Thunderbird (Windows/20090302)

C Y wrote:
On Sunday 15 November 2009 23:35:00 Tim Daly wrote:
This is a request for design discussion for those who are interested.
When it is done in this properly embedded fashion you should be able to
(mapcar #'(lambda (f) (integrate f x)) '((sin x) (cos x) ...
or use the Spad surface syntax to generate the same results.

At which point we can climb upward to a category-theoretic form...

And perform computational-mathematical proofs of algorithms...

Tim, a question here.  As I understand it (which I readily admit I don't well) the notion of what an "integral" is or for that matter what sine, cosine and 
even "x" are more or less "lives" at the category theory level.  Or, put another way, the category-theoretic level is where the "type" 
rules of category theory determine what is and is not a legal expansion of "integrate(sqrt(x),x)" - for example, if "x" is the set of positive real 
numbers integrating sqrt(x) may look a tad different in expansion to a "verbose" category theory typed set of calls than (say) negative real numbers (where 
sqrt is going to result in something not a real number).Axiom's user environment does some "type deduction" now as I understand it, to make user interaction 
more manageable, although the programming environment requires non-ambiguous specification of types.  Doesn't that imply that rather than "building up" to 
category-theoretic form the specification of the algebra
 needs to start at the category-theoretic form and have the requirements of that form dictate the 
required support structure(s) at the higher level language and Lisp levels?  And that other 
"simpler" expressions of mathematics for users would have to be layered on top of the 
robust category-theoretic foundation to support "translating" more casual user supplied 
problems (like integrate(sin(x),x) ) into statements with the rigor to be subject to formal proof? 
If I understand correctly, mathematical statements are made within the context of a series of 
axioms, such as (for example) the ZFC set theory axioms.  Category Theory provides (among other 
things) a framework with which to manage the axioms being used and what can be deduced based on the 
current operating set of axioms.  It seems to me like this conceptual framework and the language 
definitions being used to express concepts within that framework would need to be laid out before 
algebraic logic
 could really be "properly" defined in the system, but I could be wrong - have 
I misunderstood what is required for proof robustness?

That would lead to a hierarchy something like:

User-level syntax


Intermediate Layer(s)


Category Theoretic High Level Language (Spad?)


where the Category Theoretic Language would depend on Lisp behaviors, which 
would in turn depend on the machine assembly language level behaviors, etc.

This of course lends itself to the idea of languages within languages that Lisp provides, 
but the "rules" of the Category Theoretic language would essentially have to be 
the rules of category theory itself, which I'm guessing are probably some subset of the 
behaviors allowed by Lisp.

 Am I thinking about the problem incorrectly?


Axiom-developer mailing list

You are correct that category theory should underlie the Axiom type hierarchy.
My thought about "layering it above" is related to using the theory as part
of the proof process. Properly speaking it should instead be used for defining
functors and mappings. I am not nearly strong enough in category theory to
try to architect Axiom on top of it. I think that such a rebasing would be
a PhD thesis or two. You'd have to start way down deep with records as products
and unions as co-products.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]