axiom-math
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: Bill Page
Subject: [Axiom-math] Type equivalence of domains in Axiom and Aldor
Date: Thu, 25 Oct 2007 20:10:43 -0400

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.




reply via email to

[Prev in Thread] Current Thread [Next in Thread]