RE: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures

[Bill Page]

On March 13, 2006 8:34 AM Ralf Hemmecke wrote:
> ...
> Bill Page wrote:
> > 
> > (2) -> DIRPROD(2,INT) has DIRPCAT(3,INT)
> > 
> >    (2)  false
> >    Type: Boolean
> > 
> > -------
> > 
> > How does Axiom know that (2) is false?
> 
> Because Axiom tries to be smart. It uses information it does not
> have.

Perhaps you mean *should not have*. Obviously it does have this
information.

> 
> And the behaviour above is not inherent to the interpreter.
> Otherwise the following function call "foo()" would not return
> "true+false".

Thanks for testing this.

> 
> Look further below and you find that dirprod.spad and dirprod.as
> are programs where the spad and the aldor compiler produce code
> with different semantics. TOO BAD!!!
> 

Hmmm... surely this must have been considered in the design of
Aldor. Are there no Aldor categories like DIRPCAT that take a
member of a domain as a parameter? This seems like a natural
mathematical construction to me.

> ... 
> Well, as I said at the bottom of my "explanation mail"
http://lists.nongnu.org/archive/html/axiom-developer/2006-03/msg00097.html, 
> the information seems to be available also in a compiles Aldor 
> library, but it is not used.
>
> And in some way I would not really like it to be used, because
> then I would not understand the concept of a function application
> anymore.
>
> So although the output of the following program might seem strange
> at first sight,
>
>  aldor -laldor -grun dirprod.as
>  2 has 2: T
>  2 has 3: T
>
> it can be understood with my previous explanation.

I don't know what semantics to associate with the use of a member
of some domain on the right-hand side of 'has'. In Axiom I only
see

  if <domain> has <category>

In the Aldor documentation I have read a discussion of how a
domain is said to "satisfy" a category, but I do not know how
to apply this in your example above.

> If you look at DirProdCat as a function then clearly
>   DirProdCat(2,Z) = DirProd(3,Z) = with{first:%->Z}
> so why would one want another output?
>
> ----------- dirprod.as
> #include "aldor"
> #include "aldorio"
>
> define DirProdCat(n: Integer, R: Type): Category == with {
>    first: % -> R;
> }

Well, clearly the application of the category 'DIRPCAT(2,INT'
makes good sense in Axiom, don't you think? How else would you
propose to define this category? How could we do without it
in defining the domain 'DIRPROD(2,INT)'? To me this is the
reason why we want another output from your example Aldor
program. I would conclude that in fact internally (as you
already said above):

  DirProdCat(2,Z) ~= with{first:%->Z}

There must be something additional on the right-hand side
that is not reflected in the syntax of the category constant
'with' clause.

Regards,
Bill Page.