[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical stru
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical structures |
Date: |
Mon, 13 Mar 2006 14:33:34 +0100 |
User-agent: |
Thunderbird 1.5 (X11/20051201) |
Consider for example 'DirectProductCategory'
http://wiki.axiom-developer.org/axiom--test--1/src/algebra/VectorSpad/tangle
?submit=tangle&chunk=category+DIRPCAT+DirectProductCategory
It's paramters are:
DirectProductCategory(dim:NonNegativeInteger, R:Type)
but 'dim' does not appear in the signatures of the list of exports
as one can verify with:
')sh DIRPCAT
In fact 'dim' only to the right of the == some default functions
such as 'dimension' and 'size'.
One might predict using your analysis above that 'DIRPCAT(2,INT)'
and 'DIRPCAT(3,INT)' would be treated identically. But try this:
(1) -> DIRPROD(2,INT) has DIRPCAT(2,INT)
(1) true
Type: Boolean
(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.
And the behaviour above is not inherent to the interpreter. Otherwise
the following function call "foo()" would not return "true+false".
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!!!
-- begin dirprod.spad
)abbrev domain MYDOM MyDom
)abbrev category MYDPC DirProdCat
)abbrev domain MYDP DirProd
DirProdCat(n: Integer, R: Type): Category == with
fst: % -> R
DirProd(n: Integer, R: Type): DirProdCat(n, R) == add
Rep := List R -- dummy implementation
fst(x: %): R == first(x pretend List(R))$List(R)
MyDom: with
foo: () -> OutputForm
== add
foo(): OutputForm ==
b2: Boolean := (DirProd(2, Integer) has _
DirProdCat(2, Integer))
b3: Boolean := (DirProd(2, Integer) has _
DirProdCat(3, Integer))
(b2::OutputForm) + (b3::OutputForm)
-- end dirprod.spad
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.
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;
}
DirProd(n: Integer, R: Type): DirProdCat(n, R) == add {
Rep == List R; -- dummy implementation
import from Rep;
first(x: %): R == first(rep x);
}
main(): () == {
macro Z == Integer;
macro DP == DirProd(2, Z);
import from Z;
stdout << "2 has 2: " << (DP has DirProdCat(2, Z)) << newline;
stdout << "2 has 3: " << (DP has DirProdCat(3, Z)) << newline;
}
main();
--------end dirprod.as
- [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, (continued)
- [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/10
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/09
- RE: [Axiom-developer] Curiosities with Axiom mathematical structures, Bill Page, 2006/03/10
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/14
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/10
- [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/10
- RE: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Bill Page, 2006/03/11
- Re: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/11
- Re: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical structures,
Ralf Hemmecke <=
- RE: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures, Bill Page, 2006/03/13
- Re: [Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/14
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/10
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Martin Rubey, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Ralf Hemmecke, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, William Sit, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13
- Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Gabriel Dos Reis, 2006/03/13