On Mon, Sep 8, 2008 at 6:03 PM, Waldek Hebisch wrote: > > Bill Page wrote: >> >> Or look at it this way: Let C be a set of categories. The set of >> domains that satisfies Join(C) is the intersection taken over sets >> of domains that satisfy each of the categories in C. If C is the >> empty set, then this intersection is empty. >> > > Here you are confused: intersection of empty familiy of sets give > you the whole universe (here duality my help: sum of empty familiy > of sets is clearly empty set, so duality give you the universe as > intersection). >
You are correct. I am sorry that it took me so long to understand. My confusion is because in the lattice of subsets, intersection does *not* represent lattice Join - rather it's dual! http://en.wikipedia.org/wiki/Lattice_(order) "For any set A, the collection of all subsets of A (called the power set of A) can be ordered via subset inclusion to obtain a lattice bounded by A itself and the null set. **Set intersection and union interpret meet and join, respectively**." As Stephen Watt presented at the Aldor/Axiom workshop, the relationship between categories and domain can be described as follows: Each Category corresponds to a subset of Domain (the set of all domains), sat : Category -> 2^Domain namely those domains that satisfy the category sat(C) = { d for d in Domain | d has C } In particular in Axiom we have that category Type satisfied by all domains sat(Type) = Domain Then if in Axiom we define C:Category == Join(A,B) we have sat(C) = { d for d in Domain | d has A and d has B } = sat(A) intersect sat(B) So in terms of the lattice of subsets of Domain, the "Join" of two categories actually corresponds to the "Meet" of the sets corresponding to these categories. It is just the choice of name that is confusing. Do you agree that I have it correct now? > There is another source of confusion: FriCAS Join does _not_ > work like lattice operation. But it does work like a lattice operation - just not the lattice join operation. > Your definition > > Foo() : Category == Type > > is related to this. Namely except for name equivalent definition > is > > Foo() : Category == Join(Type) > > Note equivalent means that Spad compiler internally converts the > first to the second one. I agree that these two definitions are equivalent. > But > > Foo1(): Category == Join(Type) > > Foo2(): Category == Join(Type) > > gives you two different categories Yes they are different because of the name. Suppose we define: Foo() : Category == Join(Foo1,Foo2) Then all we can say is that for any domain D which declares D():Foo the expression 'D has Foo' is true. The right hand side also implies that both 'D has Foo1' and 'D has Foo2' are true. >> -- so when we use Join it behave as if it was not a mathematical >> function (actually, the Foo1 and Foo2 are different, because they >> know their names and the names are different). It seems to me that Join behaves exactly like propositional conjunction (and). > Now, I think that we should decide what to do with Join(). I see > the following possibilities: > > 1) If we want to pretend than Join is a lattice operation, than > we should return Type. > 2) To be consistent with other cases we can return empty > category with name 'Join()', which while being almost like > type is different because of different name. > 3) We can decide that 'Join()' is of little use and just throw > error > I prefer number 1. I do not think it is correct to say that 'Join()' is a category but rather that it is an expression to be evaluated as *part* of a category or domain definition. E.g. in the domain definition D():Join(Foo1,Foo2) And both Foo() : Category == Type Foo() : Category == Join() should be equivalent ways of defining an "empty" category. > I feel that current behaviour, that is getting Lisp error during > execution should be fixed. Namely, at high safety setting user > just gets strange error message. But a low safety Join() probably > can crash the system. > I agree. Regards, Bill Page. --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to fricas-devel@googlegroups.com To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en -~----------~----~----~----~------~----~------~--~---
