On Wed, Jul 9, 2008 at 7:19 AM, Gabriel Dos Reis wrote:
> Bill Page writes:
> | In a previous email you said you thought SubDomain was "half-baked".
>
> Indeed.
>
> | If you meant this in the sense of "not fully implemented" then I agree
>
> Not just fully implemented, but also not fully specified, and in fact
> the semantics seems fuzzy (at best) once one starts using it. For
> example, the SubDomain constructor takes two arguments: The
> parent domain and the predicate that test whether to consider an
> object a member of the subdomain. Yet, you have use it with only
> one argument without specficifying what that would mean.
>
Are we talking about the same "SubDomain constructor"? The one to
which I was referring is produced by Axiom and FriCAS when you create
a value referring to a category. E.g.
(1) -> c:=INS
(1) IntegerNumberSystem
Type: SubDomain Domain
As far as I can see 'SubDomain' here is is a category constructor that
takes only one argument.
There is another "subdomain constructor" that one can find in the source
code for PositiveInteger and NonNegativeInteger:
PositiveInteger: Join(OrderedAbelianSemiGroup,Monoid) with
gcd: (%,%) -> %
++ gcd(a,b) computes the greatest common divisor of two
++ positive integers \spad{a} and b.
commutative("*")
++ commutative("*") means multiplication is commutative
: x*y = y*x
== SubDomain(NonNegativeInteger,#1 > 0) add
This construction presumably returns a domain.
I think these are related, as I speculated in my previous email, but
they are certainly not the same.
> ...
> | I argued that Type is just Domain as a category and the OpenAxiom
> | interpret already returns:
> |
> | (1) -> Domain has Type
> |
> | (1) true
> | Type: Boolean
>
> I don't think this is evidence that Type is just Domain.
>
> In fact we have been through the argument that Type is a domain
> before and I do not remember we reached a definite conclusion.
I am sorry to be confusing but I did not mean to imply that Type is
just domain. It is very clear that in all versions of Axiom Type is a
category. Would you say that (2) and (3) below are identical?
(2) -> universe()$Set(IntegerMod 3)
(2) {1,2,0}
Type: Set IntegerMod 3
(3) -> IntegerMod 3
(3) IntegerMod 3
Type: Domain
Since SubDomain is a power set constructor like Set, 'Type' is a
category like 'universe()$SubDomain(Domain)' just as {1,2,0} is
'IntegerMod 3' as a set.
> ...
> | So having Type extend SetCategory and define Domain and Category
> | in terms of Type seemed to make sense. However I also wanted Type
> | to be the top of the category hierarchy (supremum of the lattice) so
> | I guess this is half-baked (ill-conceived). All we really need is
>
> Well, I do not understand why everything T satisfies
>
> T has Type
>
> should have an equality. That is my point.
>
You are right. What I wrote in my previous email about extending Type
was incorrect.
Regards,
Bill Page.
-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at http://www.sourceforge.net/community/cca08
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
