[Axiom-math] Re: Type equivalence of domains in Axiom and Aldor

[Francois Maltey]

Thanks Bill, 

> Dear Friends of Axiom and Aldor,
> 
> I have been thinking again about type equivalence. 
> For example consider the following domains in Axiom:
> 
> (1) -> P:=Product(Stream Integer,Stream Integer)
> (2) -> Q:=Stream Product(Integer,Integer)
>                                                        Type: Domain

Can I understand that as the relationship between 
Complex Fraction Integer and Fraction Complex Integer ?
[I don't find any surprising effect done by this coerce.]

> It seems that 'Stream' is a "sum-like" domain constructor so 
> that we might reasonably expect algebraically that a 'Product' 
> distributes over a 'Stream' and therefore wish to
> design the Axiom library so that this is satisfied.

I know that cartesian product of set is the set of brace 
   E x F = {(x,y) | x in E and y in F}.
   Product (Set XX, Set YY) is Set Product (XX, YY)

> Thus we should have P = Q.

Do you identify Set and Stream ?
but a stream can repeat its elements [1,2,3,1,2,3,1,...
Perhaps I mismatch the Domain << Stream Integer >> and the use of one Stream.

> I understand that neither Spad nor Aldor actually evaluate type
> expressions like P and Q.

1.. x 1.. may be [(1,1), (1,2),(2,1), (1,3),(2,2),(3,1), ...

> But perhaps EQUAL in the Lisp sense could apply?

A semi-decidable equal ? 
The answer is false when view tests shows that the results are differents.
The answer is true when the inner built are equal.
The answer is unknown in the other cases.

It's not a problem : 
1 - 2*sin^2 x and 2*cos^2 x - 1 are differents for most (or all) systems.

> Therefore I would propose the following definition of type-equivalence
> of domains:
> 
>   Def: Two domains P and Q are equivalent if and only if 
>   both domains satisfy exactly the same set of categories: 
>   (P has x) = (Q has x) for all Category expressions x 
>   *and* neither P nor Q has any explicit exports that are not
>         provided by some named category.

I don't understand this last case.

> But as I understand the
> intention of the semantics of categories in both Axiom and Aldor this
> is not enough. We want categories to represent abstract concepts
> usually with a well-defined mathematical meaning. 

Product in for-loop isn't exactly the product of 2 sets.

In a for-loop [a,b,a] x [1,2] gives [a,1],[b,1],[a,1],[a,2],[b,2],[a,2].
types can be differents. A for-loop might also works for [a,b] x [1..].

Does your product can be understand 
for cartesian products of set and for for-loop ? 

> I would like to know if other developers think this more algebraic
> approach to the design of the Axiom library domains makes sense.

Martin almost convinces me that the algebraic 
               [f (u,v) for (u,v) in [a,b,c] X [1,2,3]] 
is better than [f (u,v) for u in [a,b,c] repeat for v in [1,2,3]]

but I expect a syntax suggar and automatic coerce.

The * isn't the better operator because this locks
    {1,2,3} * {1,2,3} = {1,2,3,4,6,9} 
and {1,2,3} + {1,2,3} = {2,3,4,5,6}

I hope I don't appear too stupid !

F.