[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Embedding Axiom
From: |
C Y |
Subject: |
Re: [Axiom-developer] Embedding Axiom |
Date: |
Mon, 16 Nov 2009 15:04:26 -0800 (PST) |
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
- Re: [Axiom-developer] Embedding Axiom, (continued)
- Re: [Axiom-developer] Embedding Axiom, Tim Daly, 2009/11/17
- Message not available
- [Axiom-developer] Embedding Axiom (Hickey and fold/unfold), Tim Daly, 2009/11/20
- Re: [Axiom-developer] Embedding Axiom (Hickey and fold/unfold), Martin Baker, 2009/11/21
- [Axiom-developer] Embedding Axiom (Hickey and fold/unfold) and rule based programming, Tim Daly, 2009/11/21
- [Axiom-developer] Embedding Axiom (Hickey and fold/unfold) and Reifying time, Tim Daly, 2009/11/21
- [Axiom-developer] Embedding Axiom (Hickey and fold/unfold) Folding and generalization, Tim Daly, 2009/11/21
- [Axiom-developer] Re: Embedding Axiom (Hickey and fold/unfold) Folding and generalization, Martin Baker, 2009/11/21
- [Axiom-developer] Re: Embedding Axiom (Hickey and fold/unfold) Folding and generalization, Tim Daly, 2009/11/21
- [Axiom-developer] Re: Embedding Axiom (Hickey and fold/unfold) Folding and generalization, Tim Daly, 2009/11/21
- [Axiom-developer] Embedding Axiom, Tim Daly, 2009/11/30
Re: [Axiom-developer] Embedding Axiom,
C Y <=