On Mon, Dec 8, 2008 at 6:04 PM, Ralf Hemmecke wrote:
> Bill Page wrote:
>> The interesting situation is more like this:
>>
>> Bar(R: Ring, S: CatOfR): ...
>>
>> Here I mean that I require S to be from the *same category* as R.
>> Because R can belong to many other categories besides Ring this
>> is not quite the same thing as saying
>>
>> Bar(R: Ring, S: Ring): ...
>
> I agree with this observation, but I still would like to see a concrete
> example where the situation
>
> Bar(R: Ring, S: CatOf(R)): ...
>
> is really necessary.
The original use case that I presented in another thread involved a
different use of "CatOf(R)". If it were possible to refer directly to
the category to which a domain belongs, then implementing something
similar to Aldor 'extend' would be easy in Spad
MyInteger():CatOf(Integer) with
...
== Integer add
...
The domain MyInteger is then an extension of Integer. Note: Trying to
use 'SubsetCategory' in the same position as CatOf above leads to a
compiler abort.
> All I can think of for this abstract setting is that knowing that S
> belongs to exactly the same category as R means that if in Bar
> there is something like
>
> if R has Monoid then SomeCode;
>
> then in SomeCode the compiler would not complain if you write
>
> s: S := s1 * s2;
>
> where s1 and s2 are of type S. I don't consider that a really big
> advantage, since I could easily have written
>
> if R has Monoid and S has Monoid then SomeCode;
>
> in order to make everything totally clear in SomeCode. (And I would even
> prefer this explicit "and S has Monoid".)
>
In less abstract terms 'S:CatOf(Integer)' simply means that everywhere
I use 'S' I can treat it exactly like 'Integer' even though it may be
a conceptually distinct domain. An example of something like this
already in the the FriCAS library is 'RomanNumeral'.
>> I would much prefer that we have some theory and a model for Spad
>> for which we can (at least in principle) prove that it provides at least
>> the generality that is necessary to express a very large part of modern
>> mathematics. As you know, I have frequently promoted the idea that
>> mathematical category theory provides such a model. And it turns out
>> that the concept of SubDomain is a very critical part of such a model.
>
> Can you somehow turn your ideas into code? Suppose you have a
> perfect SPAD (call it SPAD-CAT).
Yes, I am continuing to think about that. For example I have given an
example on axiom-wiki of Spad code that implements data structures
similar to Record and Union based on categorical products and
co-products.
http://axiom-wiki.newsynthesis.org/LimitsAndColimits
> How would a polynomial domain in infinitely many variables over
> some coefficient ring look like. Make it concrete.
Re: "polynomial domain in infinitely many variables" ??? Isn't that
exactly what the domain 'Polynomial' is FriCAS is already? I don't see
that as a concrete example of what I am talking about.
> Of course it will not compile since SPAD is not yet as categorical
> as you would like. But maybe from your code one sees how SPAD
> should develop. I don't know whether a polynomial domain is
> sufficiently complex enough to show the advantage of what you
> have in mind, but I guess doing it with infinitely many variables
> might involve some Limit construction.
>
No, not so far as I understand what you mean.
The concept of limits (and co-limits) in category theory involve what
are known as universal constructions. These are situations where the
axioms allow one to specify that some operation exists and is uniquely
defined.
http://en.wikipedia.org/wiki/Universal_construction
For example, in the case of 'Product(X,Y)' the operation that is
required to exist and be uniquely defined is
product: (A:Type, A->X,A->Y) -> (A->%)
for any domain A and functions A->X, A->Y.
Regards,
Bill Page.
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en
-~----------~----~----~----~------~----~------~--~---
