On Mon, Sep 15, 2008 at 10:25 PM, Waldek Hebisch wrote: > ... I replied previously to the first part of this message in another thread "CAT(D) and extend" which dealt mostly with another subject.
> Bill Page wrote: >> The context of the discussion with Stephen was his presentation on >> "Domain, SubDomain, and categories". Stephen defined Domain as >> the set of all domains and Category as the power set of Domain (set >> of all subsets of Domain). In other words a category is a subset of >> Domain. >> >> There is one category in Category that corresponds to Domain. In >> Axiom we call this category Type. But in Category we will also find >> the *empty* category (not the same as Type!) which consists of the >> empty set of domains, and we will also find for each domain in >> Domain a corresponding singleton set containing just that domain >> in Category. >> > > I am afraid that this picture is very good to explain ideas, but can > not be taken too literally. I disagree. I think it is an important design principle of both Axiom and Aldor. It *should* be taken very literally and very seriously. It seems to me that the failure to do so is one of the reasons that the current type system of Axiom is so unclear and incomplete. > For one it ignores dynamic behavior (which is very important for > extend). It merely abstracts away from such dynamic behavior. At any given time there are only a finite number of "known" or declared domains in the Axiom library. How this changes over time is constrained by this picture of Domain and Category. > The second thing is that to better describe Axiom or Aldor type > system we need to assume that each category is infinite: > given category C you can always define domain which belongs > to this category, At any given time only a finite number of domains are known to belong to a category. > so all categories are non-empty. This does not follow logically. At any given time some categories are empty and others are not. One category (Type) is defined to consist of all domains, and another (unnamed) is *defined* to consist of no domains at all (in this sense it is by definition "empty"). > You can also define a new category C1 which adds a signature. > Of course, domain which has (belongs to C1) is different than > domain which merely belongs to C, but does not implement this > new signature. Inductively you can define an infinite sequence > of domains which are pairwise different and all belong to C. > > So "singleton" category can not be just one element set. ??? By *definition* it is a category that contains just one domain. Are saying that this definition is inconsistent? > And there is no reason to assume that given definitions: > > D : CatD == ... > > D2 : CatD == ... > > D3 : Cat(D) == ... > > that D3 will have some special relation to D which does not > hold for D2. Rather, Cat(D) would just spare you effort needed > to define CatD (of course in presence of parameters defining > CatD may be impossible). > Maybe one problem is that I have failed so far to mention one rather important formality concerning anonymous categories. In Aldor anonymous (unnamed) categories such as those introduced by the keyword 'with' are not reflexive, i.e. they are not "equal to themselves". So if I define to domains D1(): with ( foo: () -> % ) == add ... D2(): with ( foo: () -> % ) == add ... these domains necessarily and by definition belong to *different* categories. When I referred to 'Cat(D)' as the "singleton" category to which D and only D belongs, I should have specified that 'Cat(D)' is anonymous. So if I define a new domain NewD():Cat(D) == add ... the domains D and NewD do not belong to the same category because 'Cat(D)' is anonymous (just like 'with'). But still we have the weaker but sufficient condition NewD has X if and only if D has X for all categories X. And for consistency we required that NewD exports the same set of operations as D. 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 [email protected] 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 -~----------~----~----~----~------~----~------~--~---
