Re: [Axiom-developer] Embedding Axiom

[C Y]

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

Lisp

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?

Cheers,
CY