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
address@hidden
http://lists.nongnu.org/mailman/listinfo/axiom-developer