Ralf Hemmecke wrote on Wed, 05 Apr 2006 12:23:36 +0200: > > Dear William, > > I like most of what you have written, but I must oppose against a few > things. >
> > I assume you want MatroidCat to be the category of all matroids, in which > > case, > > the dual operation is actually a domain constructor. That is, the above > > signature cannot do what you are aiming for: > > > > MatroidCat():Category == ... with > > dual: % -> % > > > > because the % refers to a particular implementation of a domain which is a > > matroid, not the category itself. > > Sorry, I have not yet read about Matroids, but in simple terms it is that > dual: % -> % > transforms a concrete matroid M=(E, I) to M^D=(E, I^D) but doing this by > assuming I^D = I (and thus M=M^D) which need of course not be the case). > > So clearly that signiture is wrong. There seems to be some confusion in this chain of emails about the word "dual". I think Martin originally meant the dual of a matroid, not the dual of an element of a matroid (whatever that means). So in the quoted setting, dual:%->% is incorrect. It also does not mean constructing the dual of M=(E,I) with M^D=(E, I), or anything else. > > The argument to dual is an element of a > > matroid. A plausible signature is: > > > > dual:() -> MatroidCat() > > > > which associates a matroid to the current matroid. You are quoting the above out of context. Here is what I wrote: "I assume you want MatroidCat to be the category of all matroids, in which case, the dual operation is actually a domain constructor. That is, the above signature cannot do what you are aiming for: MatroidCat():Category == ... with dual: % -> % because the % refers to a particular implementation of a domain which is a matroid, not the category itself. The argument to dual is an element of a matroid. A plausible signature is: dual:() -> MatroidCat() which associates a matroid to the current matroid." I was explaining that in the displayed code above, the argument to dual is an element x of a matroid and it would return an element y of the same matroid, called the dual of x (whatever that mean). The next sentence, "A plausible ..." is to give a more correct signature for what Martin has in mind, constructing the dual of the domain, which is a matroid. Thus: MatroidCat():Category == ... with dual:() -> MatroidCat() It is much like the object oriented approach that associates other objects to objects in the form M.dual (which refers to a constructor giving M^D), except in Axiom syntax, it is dual() in the domain constructor of M. > That sounds promising but here I must oppose. The reason is that the > resulting dual domain will probably be not very useful. The usefulness depends on what one does with the dual of the matroid in computations. Usefulness has nothing to do with the implementation. > But let's analyse this... > > > MatroidCat(): Category == Finite with > > underlyingSet: () -> Finite > > underlyingFamily: () -> Set % > > span: Set % -> Set % > > defining?: % -> Boolean -- true if set is in underlyingFamily() > > independent?: Set % -> Boolean > > circuit?: Set % -> Boolean > > ... > > dualSet: () -> Set % -- constructs I^D > > dual: () -> MatroidCat() > > dual()==Matroid(underlyingSet(), dualSet()) > > ... > > Clearly, that category is very much involved and cannot be compiled > without knowing about the constructor Matroid(E, I). But it's not that > what I find problematic. It is the appearance of MatroidCat within the > "with" expression. What comes after the == depends on what comes before. > I cannot say, that I like this very much. Would you do something like > that in (mathematical) category theory? The "with" expression alone is > not a value until MatroidCat is known. All that MatroidCat() spells out is basically an (incomplete, declarative) definition of a matroid, plus a bunch of operations and functions that are useful for computations. Domains like the proposed Matroid(E,I) constructs actual matroids and implements those operations and functions. So the signature: dual:()->MatroidCat() simply says attach a new matroid to a given matroid. In terms of language design and computer science, self-referencing (more generally, circular references) and the much related recursion technique is what gives languages like Axiom their power. It is the equivalent to induction in mathematics. I can find you many examples in Axiom where this is the case. For example, see expr.spad and trace the representation Rep of EXPR INT (if you are lazy, just go to [SandBox Trace Analyzed], which is still a work-in-progress page, but good enough to illustrate this.) > > What else is bad is that the dual is always constructed by the domain > constructor Matroid. You don't allow other implementations (other > constructors). I don't think you are right, and indeed, quite the contrary. To construct the dual matroid M^D from a given matroid M, you must start with some given data of M. While it is conceivable you can have two different constructions of M^D with the *same* data, it is rarely the case, and a different set of data representing the same matroid M would necessarily require a different construction for its dual. What Axiom allows, in the above scheme, is to give a categorical way of constructing duals of matroids that use the same type of data representations. Remember also, the above is an idealized version. In reality, the data for M must be passed also the the MatroidCat. You should also note that I did not like this approach: I prefer using a domain constructor Dual instead. > > Alternatively, instead of using functions dual(), you can have a domain > > constructor: > > > > DualSet(M:MatroidCat): Set Set underlyingSet M == ... > > > > Dual(M:MatroidCat):MatroidCat == > > E:= underlyingSet(M) > > I:=underlyingFamily(M) > > J:=DualSet(M) > > Matroid(E, J) > > Well, that demonstrates what I mean by "the resulting dual domain will > probably be not very useful" above. > > Suppose you create a very special matroid M which inherits from > MatroidCat but additionally from many other categories. If you now say > > N == Dual(M) > > you will get something that is constructed by the constructor Matroid > (which might actually not be that what you want -- remember there are > also several implementations of polynomials and they are all good for > something). You are correct, but there is nothing to prevent you from having another domain constructor that construct duals! I was using one example. You can put subscripts to Dual and Matroid if you like (and in fact, some may not be using underlyingSet or underlyingFamily, depending on how a matroid is given). Again, that is the great flexibility of Axiom. > So the next idea would be something like > > Dual(M: MatroidCat, MAT: ??? -> MatroidCat): MatroidCat == > MAT(underlyingSet M, DualSet M); > > Well, what can you do if you now say > > N == Dual(M, MyMatroid) > > ? Actually not much, since that N is of type MatroidCat and nothing > more. No additional features are available even if MyMatroid would > return something of category MyMatroidCat that is much richer than > MatroidCat itself. I have to remind you that MatroidCat can take parameters. Your example of POLYCAT is exactly the right analogy. If we put MatroidCat(E:SetCategory, I:Set Set E), then we can have in effect many matroid categories when the parameters E and I are constructed by some set domain constructors, themselves possibly parametrized. The additional features will be reflected this way, much like the features of SUP, UP, SMP, POLY, etc. > With the above Dual constructor, you explicitly restrict the exports to > MatroidCat. And I would have no other idea to add features than to use > "pretend". Brrrrrhhh. Again, MatroidCat can take parameters, so extra features are not restricted. The extra features are added because there are *many* MatroidCat's, just like there are many POLYCAT's (may be we should call MatroidLitters?) There are extra features in each of SUP, UP, SMP, and POLY and only *one* POLYCAT category constructor! > > A more practical implementation may have this outline: > > > > MatroidCat(E:Finite, I:Set Set E): Category == Finite with > > span: Set % -> Set % > > independent?: Set % -> Boolean > > circuit?: Set % -> Boolean > > ... > > > > > > Matroid(E: SetCategory, I:Set Set E):MatroidCat(E,I) == ... with > > > > DualSet(E:SetCategory, I:Set Set E):List List E == > > > > Dual(E:SetCategory, I:Set Set E):MatroidCat(E, DualSet(E,I)) == ... > > I like that somehow much better, but the same "restriction process" as > above takes place. Things are not so easy with a dual functor. I don't think I was planning to exhaust all possibilities. You are right to point out that. But we can have *many* Dual constructors based on *other* parameters. Again, the analogy is the *other* parameters for construction of polynomial rings, as in DMP(vl:List Symbol, R:Ring) and the parameters for the corresponding POLYCAT is constructed from vl and R. > > If you do NOT want to implement dual as a domain constructor, then you may > > try > > implementing Matroid as the DOMAIN of all matroids. However, Axiom does not > > allow dependent types at the code level (only at the declaration level for > > constructors). > > > > Matroid(): SetCategory == ... > > > > Rep:= Record(E:SetCategory, I:Set Set E) > > > > probably won't work in Axiom, but Aldor may. > > Did you really mean SetCategory? Yes I do. This says Matroid() constructs a set, and if you use (E,I) to represent a matroid, then Matroid() constructs a set of some (E,I)'s where E, I would vary subject to I being a subset of the power set of E. > So to create a new element you would > write a function. > > matroid(A: SetCategory, B: Set Set A): % == per [A, B]; > > and call it with > > matroid(Integer, [[1,2], [3,4,5]]); Yes. > That sounds to me as follows: If E' \supset E and I \subseteq Power(E) > then the matroids (E, I) and (E', I) are the same. I cannot believe that. Why? By definition, (E, I) and (E', I) are different matroids. The Rep above shows they are different if E is not E'. However, they are clearly isomorphic as matroids. (That's why the ambient set E is not of much importance as long as all the elements of I are subsets of E. We may as well use the union over all sets in I as the set E. If you read the definition of a matroid I gave, nothing in E outside of this union matters. There is also no requirement of any algebraic structure on E. The whole essense of matroids depends on the set relations among a (finite) family of finite subsets. William _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer