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

[Saul Youssef]

Hi Bill,

      I unfortunately couldn't make it to the Aldor workshop and I
haven't touched the language in a few years, but I do have a comment.

      Your questions have definite answers in category theory and
since Aldor is *almost* doing category theory, it's tempting to think
that the categorical answers to your questions are really what should
naturally fit into the language.  I wrote up something trying this out
for the 2001 workshop

http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

I still think that this is a good way to look for flaws in the
language - implement category theory and see what goes wrong.

Best regards,

    Saul Youssef

On 10/25/07, Bill Page <address@hidden> wrote:
> Dear Friends of Axiom and Aldor,
>
> As a result of the recent message thread about "iterators and
> cartesian product" in the Axiom library I have been thinking again
> about type equivalence. For example consider the following domains in
> Axiom:
>
> (1) -> P:=Product(Stream Integer,Stream Integer)
>
>    (1)  Product(Stream Integer,Stream Integer)
>                                                         Type: Domain
> (2) -> Q:=Stream Product(Integer,Integer)
>
>    (2)  Stream Product(Integer,Integer)
>                                                        Type: Domain
>
> On reflection (pun intended) 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.
>
> Thus we should have
>
>    P = Q
>
> Side Note: Perhaps with an extension of the domain 'Domain' that Gaby
> recently introduced in OpenAxiom it would actually be possible to
> write and evaluate this expression in Axiom.
>
> I understand that neither Spad nor Aldor actually evaluate type
> expressions like P and Q above so it does not make sense to ask for
> "value" equality of these two domains. But perhaps EQUAL in the Lisp
> sense (ref: http://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node74.html)
> could appliy?
>
> 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.
>
> It seems that in principle it should be possible to give an efficient
> decision procedure for this test if it is not already implemented
> somewhere in the Spad and Aldor compilers. I would like to understand
> this better from the point of view of the compiler and iterpreter
> design.
>
> Obviously it makes sense to require that two equivalent domains must
> provide the same set of exported operations (the same interface)
> having the same names and same signatures. 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. That is the reason
> for explicitly referring to satisfaction of categories in the
> definition above. Further since domains can also explicitly include
> exported operations in the 'with' clause (i.e. "anonymous categories"
> as defined in the Aldor user's guide), if this mathematical meaning is
> carried only by the named categories, such anonymous categories must
> always be assumed to represent different categories in each domain in
> which they occur.
>
> With this definition it is easy to show that the current definitions
> of 'Product' and 'Stream' do not satisfy the expected distributive
> property. Right now both 'Stream' and 'Product' have explicit exports,
> further the actual list of exported operations does not match at all:
>
> (3) -> )sh P
>  Product(Stream Integer,Stream Integer) is a domain constructor.
>  Abbreviation for Product is PRODUCT
>  This constructor is not exposed in this frame.
>  Issue )edit 
> /usr/local/lib/axiom/target/i686-suse-linux/../../src/algebra/PRODUCT.spad
> to see algebra source code for PRODUCT
>
> ------------------------------- Operations --------------------------------
>
>  ?*? : (Integer,%) -> %                ?*? : (PositiveInteger,%) -> %
> ...
>
> (3) -> )sh Q
>  Stream Product(Integer,Integer) is a domain constructor.
>  Abbreviation for Stream is STREAM
>  This constructor is exposed in this frame.
>  Issue )edit 
> /usr/local/lib/axiom/target/i686-suse-linux/../../src/algebra/STREAM.spad
> to see algebra source code for STREAM
>
> ------------------------------- Operations --------------------------------
>
>  #? : % -> NonNegativeInteger          ?=? : (%,%) -> Boolean
> ...
>
> As a mininum it would probably be necessary to introduce two new
> cateogies: StreamCat(S) and ProductCat(X,Y). Then it would seem that
> would be necessary add code along the lines of
>
>    Product(A: SetCategory,B: SetCategory): ProductCat(A,B) with
>      if A has StreamCat(S) and B has StreamCat(S) then
>         StreamCat(S)
>
> And
>
>   Stream(S:Type): StreamCat(S) with
>     if S has ProductCat(A,B) then
>        ProductCat(A,B)
>
> for some set of allowed domains A, B and S, including for example
> 'Integer'. Of course there is a problem here about specifying the
> specific list of domains for A, B and C. It would be desirable I
> think, if the compiler could produce generic code which would apply
> whtn A, B and C are still unknowns. Is this possible?
>
> Of course we also need the implementations of the associate operations.
>
> With these changes we would be able to satisfy the definition of the
> type-equivalence of P and Q above.
>
> I would like to know if other developers think this more algebraic
> approach to the design of the Axiom library domains makes sense.
> Comments and criticisms are invited.
>
> Regards,
> Bill Page.
>
> _______________________________________________
> Aldor-l mailing list
> address@hidden
> http://aldor.org/mailman/listinfo/aldor-l_aldor.org
>
>