On Thu, Jun 5, 2008 at 4:16 AM, Robert Bradshaw wrote:
>
> On Jun 4, 2008, at 7:35 PM, Bill Page wrote:
> ...
> Types are all about the implementations of things, they
> synonymous with the "classes" of Object Oriented programming,
> and are insufficient (and the wrong vehicle) to carry deeper
> mathematical structure.
That is precisely the claim that I am trying to dispute. Axiom for
example specifically takes the point of view that mathematical
structure should be implemented as types in a sufficiently rich
programming language, i.e. one where types are first order objects. I
think that Axiom (and later the programming language Aldor that was
originally implemented as the "next generation" library compiler for
Axiom) has demonstrated that this view is viable.
> For example, an element of Z/5Z and an element of Z/7Z have
> the same type (i.e. they're instances of the same class, with
> the same methods, internal representation, etc), but not the same
> parent (which is data).
>
I think Gonsalo Tornaria in this thread has demonstrated that this
need not be the case.
> ...
>> "SymbolicRing" is another thing that worries me a little. Exactly what
>> (mathematically) is a symbolic ring? E.g. Why is it a ring and not a
>> field? Operations like 'sin(sin(sin(x))).parent()' doesn't look much
>> like a ring to me. Probably most other computer algebra systems
>> would just call this an "expression tree" or AST or something like
>> that.
>
> Most symbolic systems (Magma and Axiom excluded) have very
> little notion of algebras, rings, modules, etc.--virtually everything is
> an expression or list of expressions. SymbolicRing is a way to fit
> these abstract "expression trees" into a larger framework of Sage.
> It not only keeps engineers and calculus students happy, it keeps
> me happy when just want to sit down and "solve for x" or compute
> a symbolic integral. It's also a statement that rigor should not get
> in the way of usability (an important component of being a viable
> alternative to the M's).
>
It seems to me that symbolic computation need not lack rigor. And in a
computer algebra system rigor should not compromise usability. These
are design challenges that we face. This is one of the things that
strongly-typed systems like Axiom and Magma (and now Sage) offer over
these other systems.
> ...
>>
>> To the best of my knowledge, the formal concept of "representation"
>> in a computer algebra systems is unique to Axiom. Each domain
>> has a specified 'Rep'consisting of some domain expression. E.g.
>>
>> Rep == Integer
>>
>> or
>>
>> Rep == Union(Record(car:%, cdr:%), "nil")
>>
>> % stands for "this domain", so this definition amounts to some
>> recursive structure. Of course recursively defined classes are also
>> possible in Python but they require much more discipline on the
>> part of the programmer.
>>
>> Now there are two operators 'rep' and 'per' that provide coercion to
>> and from Rep. So we might say for example that some operation *
>> in this domain is implemented by * from Rep:
>>
>> x * y == per( rep(x) * rep(y) )
>>
>> The trouble is: I don't see anything here that could be called a
>> "parent". Or perhaps, they are all "parents" except for those
>> initial domains for which we never explicitly specify a Rep.
>
> Nope, nothing I see here could reasonably be called a Parent.
> Is there an object that formally represents "the ring of integers"
> that one could pass to a function?
>
Sure. For example in OpenAxiom one can write:
(1) -> Integer has Ring
(1) true
Type: Boolean
(2) -> Pick(x,A,B)==if x=0 then A else B
Type: Void
(3) -> i:=1
(3) 1
Type: PositiveInteger
(4) -> n:Pick(i,Integer,Float):=1
Compiling function Pick with type (PositiveInteger,Domain,Domain)
-> Domain
(4) 1.0
Type: Float
And of course even easier in Sage :-)
sage: category(IntegerRing())
Category of rings
sage: def Pick(x,A,B):
if x==0:
return A
else:
return B
....:
sage: i=1
sage: n=Pick(i,IntegerRing(),RealField())(1)
sage: n; parent(n)
1.00000000000000
Real Field with 53 bits of precision
> ...
>>
>>> One of the changes in this latest coercion push is to allow
>>> Parents to belong to several categories.
>>>
>>
>> That sounds good. So does this mean that the 'category' method
>> now returns a list?
>
> There are two methods, category (returning the first cat in the
> list) and categories (returning the whole list). The set of categories
> is an ordered list, and things are attempted in the first category
> (and its supercategories) before moving on to the next. Most
> objects, of course, will belong to one category (not including its
> super categories).
>
Here is something to consider: Instead of having two methods, one that
return a list, you could implement some operations on categories that
yield new categories. One such operation (because the categories form
a lattice) might be 'Join'. Then if a parent belongs to more than one
category you could just return their Join. One of the methods provided
with category could be one that lists it's component categories, or
more generally the expression (if any) that created it.
>From category theory it is easy to imagine other operations that one
might want to perform on categories to create new categories.
> ...
Regards,
Bill Page.
--~--~---------~--~----~------------~-------~--~----~
To post to this group, send email to sage-devel@googlegroups.com
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at http://groups.google.com/group/sage-devel
URLs: http://www.sagemath.org
-~----------~----~----~----~------~----~------~--~---
