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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer