

last edited 6 months ago by test1 
1 2  
Editor: test1
Time: 2019/07/20 20:14:00 GMT+0 

Note: 
changed: Type equivalence of domains in Axiom and Aldor   *by Bill Page7 Oct 25, 2007; 09:10pm* Type equivalence of domains in FriCAS and Aldor *originally by Bill Page7 Oct 25, 2007; 09:10pm* changed: Axiom: FriCAS: changed: design the Axiom library so that this is satisfied. design the FriCAS library so that this is satisfied. changed: write and evaluate this expression in Axiom. write and evaluate this expression in FriCAS. changed: could appliy? could apply? added: 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. changed: intention of the semantics of categories in both Axiom and Aldor this intention of the semantics of categories in both Spad and Aldor this changed: which they occur. which they occur (no: anonymous types use structural equivalence). changed: As a mininum it would probably be necessary to introduce two new cateogies: StreamCat(S) and ProductCat(X,Y). Then it would seem that As a minimum it would probably be necessary to introduce two new categories: StreamCat(S) and ProductCat(X,Y). Then it would seem that changed: whtn A, B and C are still unknowns. Is this possible? when A, B and C are still unknowns. Is this possible? changed: approach to the design of the Axiom library domains makes sense. approach to the design of the FriCAS library domains makes sense. changed: library such as Axiom library. What is the "meaning" of 'Cat' if it library such as FriCAS library. What is the "meaning" of 'Cat' if it
originally by Bill Page7 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:
P:=Product(Stream Integer,Stream Integer)
(1) 
Q:=Stream Product(Integer,Integer)
(2) 
On reflection (pun intended) it seems that Stream
is a "sumlike"
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 typeequivalence of domains:
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 welldefined 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. 9 Names for 9 Operations in this Domain.  Operations 
?=? : (%,%) > Boolean coerce : % > OutputForm first : % > Stream(Integer) hash : % > SingleInteger latex : % > String second : % > Stream(Integer) ?~=? : (%, %) > Boolean construct : (Stream(Integer), Stream(Integer)) > % hashUpdate! : (HashState, %) > HashState
)sh Q
Stream(Product(Integer,Integer)) is a domain constructor. Abbreviation for Stream is STREAM This constructor is exposed in this frame. 85 Names for 109 Operations in this Domain.  Operations 
?=? : (%,%) > Boolean child? : (%, %) > Boolean children : % > List(%) coerce : % > OutputForm complete : % > % concat : List(%) > % concat : (%, %) > % concat! : (%, %) > % copy : % > % cycleEntry : % > % cycleSplit! : % > % cycleTail : % > % cyclic? : % > Boolean delay : (() > %) > % delete : (%, Integer) > % distance : (%, %) > Integer ?.rest : (%, rest) > % empty : () > % empty? : % > Boolean eq? : (%, %) > Boolean explicitEntries? : % > Boolean explicitlyEmpty? : % > Boolean explicitlyFinite? : % > Boolean extend : (%, Integer) > % hash : % > SingleInteger 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)) > % ?.first : (%, first) > Product(Integer, Integer) ?.last : (%, last) > Product(Integer, Integer) ?.value : (%, value) > Product(Integer, Integer) elt : (%, Integer, Product(Integer, Integer)) > Product(Integer, Integer) ?.? : (%, Integer) > Product(Integer, Integer) ?.? : (%, 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) hashUpdate! : (HashState, %) > HashState 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 typeequivalence 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 Page7 Oct 28, 2007; 06:26pm
No. I should have explicitly written "typeequivalent" 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 Aistleitner2 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 runtimedue 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 welldefined 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 ofProduct(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 "typeequivalent?" taking two Aldor entities and computing whether or not they are typeequivalent in the sense you presented in your last mail. What problem can you solve with it?
Kind regards, Christian