Type equivalence of domains in FriCAS and Aldor

originally by Bill Page-7 Oct 25, 2007; 09:10pm

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 FriCAS:

(1) -> P:=Product(Stream Integer,Stream Integer)

(1)

Q:=Stream Product(Integer,Integer)

(2)

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 FriCAS 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 FriCAS.

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 apply?

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.

Note (by Waldek): such equivalence is usually called structural equivalence. Spad normally uses "name equivalence": two types are equivalent if and only if they have the same constructor and corresponding arguments are equivalent.

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 Spad 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 (no: anonymous types use structural equivalence).

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:

)sh P

 Product(Stream(Integer),Stream(Integer)) is a domain constructor.
 Abbreviation for Product is PRODUCT 
 This constructor is not exposed in this frame.
 7 Names for 7 Operations in this Domain.
------------------------------- Operations --------------------------------

 ?=? : (%, %) -> Boolean               coerce : % -> OutputForm
 first : % -> Stream(Integer)          latex : % -> String
 second : % -> Stream(Integer)         ?~=? : (%, %) -> Boolean
 construct : (Stream(Integer), Stream(Integer)) -> %

)sh Q

 Stream(Product(Integer,Integer)) is a domain constructor.
 Abbreviation for Stream is STREAM 
 This constructor is exposed in this frame.
 83 Names for 108 Operations in this Domain.
------------------------------- Operations --------------------------------

 ?=? : (%, %) -> Boolean               child? : (%, %) -> Boolean
 children : % -> List(%)               coerce : % -> OutputForm
 complete : % -> %                     concat : List(%) -> %
 concat : (%, %) -> %                  concat! : List(%) -> %
 concat! : (%, %) -> %                 copy : % -> %
 cycleEntry : % -> %                   cycleSplit! : % -> %
 cycleTail : % -> %                    cyclic? : % -> Boolean
 delay : (() -> %) -> %                delete : (%, Integer) -> %
 distance : (%, %) -> Integer          elt : (%, rest) -> %
 empty : () -> %                       empty? : % -> Boolean
 eq? : (%, %) -> Boolean               explicitEntries? : % -> Boolean
 explicitlyEmpty? : % -> Boolean       explicitlyFinite? : % -> Boolean
 extend : (%, Integer) -> %            index? : (Integer, %) -> Boolean
 indices : % -> List(Integer)          insert : (%, %, Integer) -> %
 latex : % -> String                   lazy? : % -> Boolean
 lazyEvaluate : % -> %                 leaf? : % -> Boolean
 maxIndex : % -> Integer               minIndex : % -> Integer
 node? : (%, %) -> Boolean             nodes : % -> List(%)
 possiblyInfinite? : % -> Boolean      qsetrest! : (%, %) -> %
 rest : % -> %                         rst : % -> %
 sample : () -> %                      setelt! : (%, rest, %) -> %
 setrest! : (%, Integer, %) -> %       setrest! : (%, %) -> %
 showAll? : () -> Boolean              showAllElements : % -> OutputForm
 tail : % -> %                         ?~=? : (%, %) -> Boolean
 coerce : List(Product(Integer,Integer)) -> %
 concat : (Product(Integer,Integer), %) -> %
 concat : (%, Product(Integer,Integer)) -> %
 concat! : (%, Product(Integer,Integer)) -> %
 cons : (Product(Integer,Integer), %) -> %
 construct : List(Product(Integer,Integer)) -> %
 cycleLength : % -> NonNegativeInteger
 delete : (%, UniversalSegment(Integer)) -> %
 elt : (%, first) -> Product(Integer,Integer)
 elt : (%, last) -> Product(Integer,Integer)
 elt : (%, value) -> Product(Integer,Integer)
 elt : (%, Integer, Product(Integer,Integer)) -> Product(Integer,Integer)
 elt : (%, Integer) -> Product(Integer,Integer)
 elt : (%, UniversalSegment(Integer)) -> %
 entries : % -> List(Product(Integer,Integer))
 fill! : (%, Product(Integer,Integer)) -> %
 filterUntil : ((Product(Integer,Integer) -> Boolean), %) -> %
 filterWhile : ((Product(Integer,Integer) -> Boolean), %) -> %
 find : ((Product(Integer,Integer) -> Boolean), %) -> Union(Product(Integer,Integer),"failed")
 findCycle : (NonNegativeInteger, %) -> Record(cycle?: Boolean,prefix: NonNegativeInteger,period: NonNegativeInteger)
 first : % -> Product(Integer,Integer)
 first : (%, NonNegativeInteger) -> %
 frst : % -> Product(Integer,Integer)
 insert : (Product(Integer,Integer), %, Integer) -> %
 last : % -> Product(Integer,Integer)
 last : (%, NonNegativeInteger) -> %
 leaves : % -> List(Product(Integer,Integer))
 less? : (%, NonNegativeInteger) -> Boolean
 map : (((Product(Integer,Integer), Product(Integer,Integer)) -> Product(Integer,Integer)), %, %) -> %
 map : ((Product(Integer,Integer) -> Product(Integer,Integer)), %) -> %
 map! : ((Product(Integer,Integer) -> Product(Integer,Integer)), %) -> %
 more? : (%, NonNegativeInteger) -> Boolean
 new : (NonNegativeInteger, Product(Integer,Integer)) -> %
 numberOfComputedEntries : % -> NonNegativeInteger
 qelt : (%, Integer) -> Product(Integer,Integer)
 qsetelt! : (%, Integer, Product(Integer,Integer)) -> Product(Integer,Integer)
 qsetfirst! : (%, Product(Integer,Integer)) -> Product(Integer,Integer)
 remove : ((Product(Integer,Integer) -> Boolean), %) -> %
 repeating : List(Product(Integer,Integer)) -> %
 repeating? : (List(Product(Integer,Integer)), %) -> Boolean
 rest : (%, NonNegativeInteger) -> %
 second : % -> Product(Integer,Integer)
 select : ((Product(Integer,Integer) -> Boolean), %) -> %
 setchildren! : (%, List(%)) -> %
 setelt! : (%, first, Product(Integer,Integer)) -> Product(Integer,Integer)
 setelt! : (%, last, Product(Integer,Integer)) -> Product(Integer,Integer)
 setelt! : (%, value, Product(Integer,Integer)) -> Product(Integer,Integer)
 setelt! : (%, Integer, Product(Integer,Integer)) -> Product(Integer,Integer)
 setelt! : (%, UniversalSegment(Integer), Product(Integer,Integer)) -> Product(Integer,Integer)
 setfirst! : (%, Product(Integer,Integer)) -> Product(Integer,Integer)
 setlast! : (%, Product(Integer,Integer)) -> Product(Integer,Integer)
 setvalue! : (%, Product(Integer,Integer)) -> Product(Integer,Integer)
 showElements : (NonNegativeInteger, %) -> OutputForm
 size? : (%, NonNegativeInteger) -> Boolean
 split! : (%, NonNegativeInteger) -> %
 stream : ((Product(Integer,Integer) -> Product(Integer,Integer)), Product(Integer,Integer)) -> %
 stream : (() -> Product(Integer,Integer)) -> %
 swap! : (%, Integer, Integer) -> Void
 third : % -> Product(Integer,Integer)
 value : % -> Product(Integer,Integer)

As a minimum it would probably be necessary to introduce two new categories: 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 when 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 FriCAS library domains makes sense. Comments and criticisms are invited.

by Saul Youssef Oct 26, 2007; 01:09am

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

by Ralf Hemmecke Oct 27, 2007; 05:53pm

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.

Let's see:

  Cat: Category == with {
     coerce: Integer -> %;
     coerce: % -> Integer;
     bar: (%, %) ->  %;
  }
  P: Cat == add {
     Rep == Integer; import from Rep
     coerce(x: Integer): % == per x;
     coerce(x: %): Integer == rep x;
     bar(x: %, y: %): % == per(rep x + rep y);
  }
  ----------------------------------^

  Q: Cat == add {
     Rep == Integer; import from Rep
     coerce(x: Integer): % == per x;
     coerce(x: %): Integer == rep x;
     bar(x: %, y: %): % == per(rep x - rep y);
  }
  ----------------------------------^

You are saying that P and Q are equivalent.

by Bill Page-7 Oct 28, 2007; 06:26pm

No. I should have explicitly written "type-equivalent" as I did elsewhere in that message. I would only want to say that their types are equivalent - that they necessarily represent the same kind of things. Something like: "they are both monoids".

I would also say that without giving more information about the use of the category Cat you are at risk of abusing the intention of defining a category - at least in the context of the design of a library such as FriCAS library. What is the "meaning" of Cat if it makes sense to give two rather different definitions of bar? I started my discussion by saying that I assumed that the intention of defining a category was to represent some specific aspect or common mathematical property of a as set of mathematical object(s). I do not want to think of a category as a mere syntactical convenience for example like a macro.

Regards, Bill Page.

Christian Aistleitner-2 Oct 29, 2007; 02:56am

Although it's trivial to see, I thought it might be good to explicitly say that this property can only be checked at runtime--due to Aldor's "extend".

If P and Q are type equivalent in the above sense, linking the code with a further library extending only P by another named category breaks type equivalence.

In a nutshell, you want each anonymous category to be different from any category.

My feeling about Aldor is different:

Important exports with well-defined semantics should be defined in named categories.

Unimportant exports, syntactic sugar and the like (so all the exports which do not represent some general mechanism and do not contribute to the essence of a domain) may go into unnamed categories.

Using such an intuition, unnamed categories and their current semantics for type satisfaction really fit the concept. Still, you could define type equivalence by just checking the named categories and ignoring the unnamed categories.

Currently, lots of domains do not stick to this intuition, but that's a different story.

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.

The code seems to somehow model a distributive law you described above. That's ok for me, but I cannot see how this relates to type equivalence. Assume, I give you a binary operator "type-equivalent?" taking two Aldor entities and computing whether or not they are type-equivalent in the sense you presented in your last mail. What problem can you solve with it?

Kind regards, Christian