login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

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:

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

\label{eq1}\hbox{\axiomType{Product}\ } \left({{\hbox{\axiomType{Stream}\ } \left({\hbox{\axiomType{Integer}\ }}\right)}, \:{\hbox{\axiomType{Stream}\ } \left({\hbox{\axiomType{Integer}\ }}\right)}}\right)(1)
Type: Type
fricas
Q:=Stream Product(Integer,Integer)

\label{eq2}\hbox{\axiomType{Stream}\ } \left({\hbox{\axiomType{Product}\ } \left({\hbox{\axiomType{Integer}\ } , \: \hbox{\axiomType{Integer}\ }}\right)}\right)(2)
Type: Type

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:

fricas
)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)) -> %
fricas
)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




  Subject:   Be Bold !!
  ( 15 subscribers )  
Please rate this page: