"Bill Page" <[EMAIL PROTECTED]> writes:
| On Fri, Jul 4, 2008 at 7:40 AM, Gabriel Dos Reis wrote:
| > Bill Page writes:
| >
| > | On Thu, Jul 3, 2008 at 12:18 PM, Gabriel Dos Reis wrote:
| > | > ...
| > | > The fact that `Type' is a category, but not a domain is something
| > | > that OpenAxiom inherits from the base AXIOM system. On many
| > | > occasions I've found it a blessing and a curse.
| > | >
| > |
| > | It is not clear to me when it might be a blessing... :-) As I see it,
| > | the main purpose of a category in OpenAxiom is to stand for some
| > | mathematical (or datastructure-like) concept.
| >
| > See the definition of the various collections. They have a heading
| > like
| >
| > HomogeneousAggregate(S: Type): Category ==
| > ^^^^^^^
| >
| > A most general category is needed here. The `magic' that is applied
| > to Category and Domain could be applied to Type, but that would
| > pose its own set of problems e.g. in the case of Aggregate.
| >
|
| Although Type is a domain in Aldor, exactly this sort of construction
| is used there without a problem (notwithstanding a separate issue
| raised by Ralf concerning the use of 'has' in Aldor). Why do you think
| it is a problem in SPAD?
What are the reasons that make you believe that it is a separate issue?
|
| > [...]
| >
| > | There is a related problem with the definition of the domain
| > | 'Category' - is it a domain or a category?
| >
| > Category is conceptually a category, just like Domain is conceptually
| > a category.
|
| What do you mean by "conceptually a category"? As far as I can see
| Domain is a domain - not conceptually a category at all.
Why?
| > Note that in the base AXIOM system, those don't have
| > representations and that can prove problematic on more than one
| > occasion. Categories and domains are objects; the ability to pass
| > them around and return them as function values, requires that we have
| > a representation for them.
|
| Yes, this is clear. A representation of categories and domains as
| values (objects) is definitely required. As I understand it, in Axiom
| objects belong only to domains. So categories and domains must be
| domains.
|
| > Therefore Category and Domain do have domain definition, but they
| > are conceptually categories.
| >
|
| I think that before we can make sense of what it means to be
| "conceptually a category" it is necessary to first define
| unambiguously what is a "category". Stephen Watt defined it as I
| quoted below:
|
| >
| > | I think the way out of this mess was correctly identified by Stephen
| > | Watt in the description of Aldor when he wrote: (ibid.):
| > |
| > | "Each domain is itself a value belonging to the domain Type. Domains
| > | may additionally belong to some number of subtypes (of Type), known as
| > | categories."
| >
| > This is already the case of all flavors of AXIOM, I think.
| >
|
| That is not clear to me. I think at best this might be implemented in
| different flavors of Axiom in different ways and in a more or less
| consistent manner.
|
| > | I.e. 'Type' is a Domain. Categories are subtypes of Type, but as such
| > | Type (being itself a subtype of Type) is also a category unless we
| > | consider only proper subtypes.
| >
| > The quote you gave does not itself impose that Type must be a domain.
|
| To me the phrase: "... the *domain* Type" (my emphasis **) says
| specifically that Type is a domain. How else can I understand it?
OK, let me rephrase my question. We are trying to understanding why
`Type' *must* be a domian (your position). To arrive at that
conclusion, we should not start with the axiom that 'Type' is a
domain. That is why I zapped the first sentence, concentrating on the
semantics specification. Now, that is cleared. I would like to
understand why `Type' must be a domain. Nothing in the semantics
specification (the quote above without the first sentence) requires
Type to be a domain.
|
| > All it says is a semantics requirement on the value of
| >
| > x has Type
| >
| > for all domains x.
| >
|
| The quotation from Stephen Watt makes no reference to 'has'.
I appreciate that. However, the quote is also plain English, not
executable. Therefore useless.
I was trying to make it executable. Apparantly that attempt is wrong.
Could you supply an executable semantics for the plain English quote?
| 'has' is
| defined elsewhere in the Aldor documentation under the subject of type
| satisfaction. In both Aldor and Axiom the thing to the right of 'has'
| must be a category, so in Aldor it is not possible to write:
|
| x has Type
|
| because Type is a domain - not a category.
OK. What is the executable semantics content of your quote?
|
| > The decision to make Type a domain is a separate one.
|
| If I want to be able to write:
|
| x:Type := ...
|
| then it seems very clear that Type must be a domain.
If it is so very clear to you, then you must be able to explain the
reasons so very simply.
Why is it so fundamental that Type must be a domain, and that reason
does not carry to Ring?
After all, why can't one write
y: Ring := Integer
?
[...]
| But I agree that it may be possible to find another
| solution. In particular in OpenAxiom you have introduced a new domain
| called Domain that plays a similar role to Type in Aldor.
In OpenAxiom, I can say
x: Domain := Integer
but not
y: Domain := Ring
Is it the case that you can say
x: Type := Integer
but not
y: Type := Ring
in Aldor?
| That allows
| you to retain then name 'Type' for something else - a category. I
| proposed in my previous message that what it turns out to be is just
| Domain considered as a subdomain of itself.
Maybe; I'm not familiar with your notion of `subdomain'. Could you explain?
| As far as I know Aldor has
| no name for this although Stephen Watt's definition would apparently
| allow it, i.e. the subtype of Type consisting of exactly all of Type.
|
| > One I have considered many times in the past, mostly when I
| > decided to give Domain and Category definitions.
|
| Yes I understand. I would argue similarly that writing in OpenAxiom
|
| x:Domain := ...
| x:Category := ...
|
| implies that Domain and Category are domains.
So, if you could write
x: Ring := ...
Would Ring cease to be a category?
[...]
| > The fact that we have a two-level system implies that somewhere this
| > kind of problem will surface again, so just giving Type a domain definition
| > is not necessarily a solution to the fundamental problem.
| >
|
| I agree that just giving Type a domain definition is not a solution. I
| think the solution to the problem has to do with defining more
| precisely what is a "category" (i.e. in the case of Aldor a categories
| are subtypes of Type, domains are objects of Type and therefore via
| the subtype relation domains are also objects of categories).
Depending on ones notion of `subtype', it is already the case that
a category is a subtype of Type -- if by x is subtype of Type one
means that the query
x has Type
is well formed and yields true.
| That Type and subtypes of Type (categories) are also domains is not a
| central part of the resolution of the problem but rather more a matter
| of convenience. It means that this "two-level system" is essentially
| flat.
|
| > |
| > | In OpenAxiom we now have the domain named 'Domain' so we should be
| > | able to say: "Each domain is itself a value belonging to the domain
| > | 'Domain'. Categories are sub-domains of 'Domain'. Then 'Type' is just
| > | Domain as a whole considered as a category."
| >
| > Why *should* we be able to say that? Especialy, that
| >
| > # Categories are sub-domains of 'Domain'
| >
| > ?
|
| That is a key part of the definition give by Stephen Watt:
|
| "... subtypes (of Type), known as categories."
Concretely, what does not mean? I'm asking the question from an
operational semantics point of view. What does it mean to be a
subtype of?
| Unlike OpenAxiom, Aldor does not define 'Domain' as a domain, but
| 'Type' is literally a domain. Domains are all objects of a
| distinquished domain called 'Type'. (Quote: "Each domain is itself a
| value belonging to the domain Type."). As I see it, OpenAxiom has used
| the name 'Domain' in the same way that Aldor used the name 'Type'. So
| in OpenAxiom we may write:
|
| x:Domain := Domain
|
| but in Aldor we would say:
|
| x:Type := Type;
|
| So finally in OpenAxiom we should say:
|
| "Categories are sub-domains of 'Domain."
|
| The most recent revision of Open-Axiom gives these results:
|
| (1) -> x:Domain:=Domain
|
| (1) Domain
| Type: Type
| (2) -> y:Category:=IntegerNumberSystem
|
| Category is a category, not a domain, and declarations require
| domains.
Again, this error can be reproduced in all versions of AXIOMs. I do
not find it fundamental to resolve the question.
| (2) -> y:Domain:=IntegerNumberSystem
|
| (2) IntegerNumberSystem
| Type: Category
| (3) -> z:Domain:=Integer
|
| (3) Integer
| Type: Domain
| (4) -> w:=Domain:=Category
|
| You have used the abbreviation Domain of the constructor Domain on
| the left-hand side of an assignment expression. This is not
| allowed.
This is correct behaviour. Domain and Category are constants.
| (4) -> w:Domain:=Category
|
| (4) Category
| Type: Type
|
| --------
|
| I think that 'Type: Type' does not make sense
Why?
| and (2) and (4) above should not be errors.
|
| >
| > | 'Domain' is a domain, but are sub-domains of domain also domains?
| >
| > Exactly what do you mean by this?
| >
|
| Stephen Watt's definition does not require that sub-types of Type are
| domains - only that Type itself is a domain.
Then, what does it mean to be `subtype of'?
| However in Aldor (and
| Axiom) we also want categories to be values (object) belonging to some
| domain called Category.
|
| > | So again, what is Category?
| >
| > See my answer above. It is the type of all category objects.
|
| I think that is ok provided Category is itself a domain. But it misses
| an important aspect: Objects of type Category are subtypes of Type
| (subdomains of Domain).
I do not understand this observation. Please, could you clarify?
|
| >
| > | For example IntegerNumberSystem is a category. Right now OpenAxiom
| > | says:
| > |
| > | (1) -> I:=Integer
| > |
| > | (1) Integer
| > | Type: Domain
| > |
| > | (2) -> x:=IntegerNumberSystem
| > |
| > | (2) IntegerNumberSystem
| > | Type: Category
| > |
| > | But in FriCAS (and Axiom), we still get:
| > |
| > | (1) -> I:=Integer
| > |
| > | (1) Integer
| > | Type: Domain
| > |
| > | (2) -> x:=IntegerNumberSystem
| > |
| > | (2) IntegerNumberSystem
| > | Type: SubDomain Domain
| > |
| > | ------
| > |
| > | which I guess is technically correct, unfortunately 'Domain' and
| > | 'SubDomain' where never defined as domain constructors in either
| > | Axiom or FriCAS. OpenAxiom corrected that problem but it
| > | introduced 'Category' as a domain (sometimes) instead of defining
| > | 'SubDomain'.
| >
| > What is SubDomain?
| >
|
| I am guessing and trying to fill-in the blanks since as far as I know
| there is no written documentation in Axiom about this, but it seems to
| me that SubDomain must be a domain constructor that takes a domain as
| argument. Specify we need
|
| Category = SubDomain(Domain)
|
| But Domain is itself a domain so maybe one should be able to write, for
example:
|
| x:SubDomain(Integer) := PositiveInteger
|
| ??
Maybe.
In the base AXIOM system and in FriCAS I do not recall seeing Domain
as being defined as a domain -- in fact, it has no definition at all.
|
| > | I guess I am still a little confused about all of this. :-)
| >
| > The problem, as I see it, is fundamentally that of bridging the gap
| > between two level systems.
| >
|
| Ok, I agree. I think that is exactly what Stephen Watt's definition
| accomplishes by: "Domains are objects of the domain Type and
| Categories are subtypes of Type". The difference between the two
| levels is one of membership versus subsets.
That still leaves an undefined notion that you have based your
arguments on: subtype. What is it?
OpenAxiom's take is that to bridge the pag between the two level, one
would realy on satisfaction of properties defined through the `has'
operator.
-- Gaby
-------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
