Re: [Axiom-developer] A curious algebra failure

[Gabriel Dos Reis]

On Sat, 11 Aug 2007, Bill Page wrote:

| On 8/11/07, Gabriel Dos Reis wrote:
| > On Sat, 11 Aug 2007, Stephen Wilson wrote:
| >
| > | Gabriel Dos Reis <address@hidden> writes:
| > |
| > | > On Sat, 11 Aug 2007, Stephen Wilson wrote:
| > | >
| > | > | Gabriel Dos Reis <address@hidden> writes:
| > | > | > | Here, % certainly satisfies the conditions on the parameter type:
| > | > | > |
| > | > | > |    SetCategory with "*": (%,%)->%
| > | > | >
| > | > | > I don't think it does, in the sense of Spad.
| > | > | > I believe two unnamed categories define distinct categories 
irrespective of
| > | > | > their bodies.
| > | > |
| 
| No, that is *not* correct. Unnamed categories are just values of type
| Category.

But, that is not what Axiom Book says, section 12.12, page 525:

   The part of a category to the right of a with is also regarded as 
   a category -- an "anonymous category". [...]
   [ rewriting packages with named categories skipped ]
   There is no reason, however, to give this list of exports a name since no
   other domain of package exports it.  In fact, it is rare for a package to
   export a named category.  [...]

This, to me, suggest that the semantics described and intended in the 
Axiom Book is that two unnamed categories always yields different categories
irrespective of their bodies.

That may nto be what we want or would like, but I believe that is what was
intended in the Axiom Book.
   

| They are distinct only if the values are distinct. 'with' is
| used to form a category-valued expression.

I don't get this.  Please, could you give more Spad examples of what you mean? 

| 
| > | > | Are you saying that % is unnamed?
| > | >
| > | > `%' is not a category; it stands for the current domain.
| > | >
| > | > I'm saying that the category
| > | >
| > | >     SetCategory with "*": (%,%)->%
| > | >
| > | > is unnamed.
| > |
| 
| That is correct.
| 
| > | Right.  What I am saying is that in the type context
| > |
| > |     S : SetCategory with "*": (%, %) -> %
| > |
| > | when % denotes MONAD, the category of % (its `principle category' as I
| > | called it, since in the general case it is anonymous), satisfies the
| > | context.  Certainly MONAD has SetCategory and an export "*": (%, %) ->
| > | %.  The nominal/structural typing rules (not that I have tried to
| > | define them formally) are just my way of thinking about the issue.
| >
| > I think I understand what you're saying.  I'm not sure they match Spad 
typing
| > rules.  See the discussions in sections 12.8 and 12.12 of the Axiom book.
| > The short version is that
| >
| >     domains belong to categories by assertions.
| >
| >
| > | If this interpretation does not hold, what kind of expression could
| > | possibly satisfy the context S above?
| >
| > That is the whole problem. :-)
| >
| 
| This statement in the Axiom book should really say:
| 
|   "domains belong to *named* categories by assertions"
| 
| This does apply to anonymous categories.

Well, there is what we *would like* the Axiom Book to say, and what it
intended to say and what is implemented.

| > As you suggested, I suspect it should have been written like
| >
| >      if S has SetCategory and S has "*"
| >
| 
| No, I don't think that is what Stephen is saying.
| 
| > The trouble is that we don't want to test just for the name "*".  We
| > want to test for the signature
| >
| >           "*":(%, %) -> %
| >
| 
| That is precisely what is meant by a domain satisfying a category
| *value* (a so called "anonymous" category).

Except that is not what is described in the Axiom Book.

| > I don't know how to write that in Spad -- Ralf?
| >
| 
| I think that sometimes the best way to understand Spad is to look
| backwards from the definition of Aldor. A much more rigorous and
| consistent definition of Aldor concepts is given in the Aldor User
| Guide (AUG) and in most cases these concepts map backwards to Spad
| exactly as required.

Yes, I understand that Aldor is an evolution of Spad that fixes many issues. 
The issue right now is what the actual semantics is, that we must distinguish 
from what we would like it to say.  The distinction is very important so that
we measure the impact of the changes that will result (for the Alegbra --
hopefully, we don't have many cases like this).  The Axiom Book went on
greater details in section 12.8 (correctness) explaining why they reject
structural conformance -- even partial.

I'm not saying that is a good thing.  I'm trying to draw the line between 
what the intended semantics are and what we would like them to be.

| In this case I would strongly recommend that you (re-)read Chapter 7
| Types. Specifically take a look at Section 7.5 Subtypes for a
| discussion of category-valued expressions versus named categories and
| Section 7.7 Type Satisfaction. Also most of section 7.9 Categories
| especially to understand the use of 'define' to refer to
| category-valued constants (Note: define is not available in Spad).

Yes, but here we are discussing Spad :-)

| Unfortunately www.aldor.org is down :-( again!! ). Perhaps you have a
| copy of the pdf version of AUG?

Yes, I do.

| If not you can download a version of
| it here:
| 
| http://www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/documentation/axlugII.pdf

Thanks.

-- Gaby