Re: [Axiom-developer] operations working in general, but not in special cases -- help needed

[Martin Rubey]

Dear William, *

thanks a lot for your answer. I think that you clarified the issue quite a bit,
but I still have to think about it.

A short reply...

William Sit <address@hidden> writes:

> > Example 1, Matroids
> > 
> > A "matroid" is a mathematical structure with one very, very important
> > operation, namely "dualizing" which transforms a given matroid into
> > another. Thus, one is tempted to have a category "MatroidCat", which 
> > exports an
> > operation "dual: % -> %".
> 
> I assume you want MatroidCat to be the category of all matroids, 

No, at least not originally. I wanted MatroidCat be the "category" (in the
sense of axiom/aldor) of those domains, which represent matroids. I.e., an
element of a domain which in turn belongs to MatroidCat would be a matroid.

> 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.

So, in your view, MatroidCat would contain all matroids, and a domain belonging
to MatroidCat would be a specific matroid?
 
> 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. The advantage is that this will
> allow domain constructors implemented as functions, and operations on
> matroids (not matroid elements) are also possible. So for example, one may
> test whether two matroids are equal or isomorphic.

That's what I had in mind.

> Given any (not necessarily planar) graph G = (N, A), where N is the node set 
> and
> A the arc set, there is always a corresponding matroid M = (E, I) called a
> graphic matroid. (Theorem 4.1, p. 271). Hence a graphic matroid always has a
> dual matroid called the cographic matroid. So there are TWO matroids for every
> graph G.

Well, yes. Usually one says that the graphic matroid corresponds to the graph,
though.
 
> This means two domain constructors:
> 
>     GraphicMatroid(G: GraphCat):MatroidCat == ...
> 
>     CographicMatroid(G: GraphCat):MatroidCat == ...

If I follow this route I should put all matroidal properties of graphs into
MatroidCat, and only those properties which are not matroidal into GraphCat I
think I like this idea.

> > Example 2, Differential Equations
> > 
> > It is quite easy to see that the class of holonomic functions is closed
> > under integration
> > 
> > However, we all know that the class of rational functions is *not* closed
> > under integration
> 
> The integrate operation is more like the minus or divide operation. Since
> they operate on elements (not domains), you can simply export integrateIfCan
> in RatCat.

yes. 

> The two examples you gave present two different problems.

It very much depends on how you view the problem(s). Of course, taking your
approach, these are different problems, but I do think that one can see them as
a single problem, too.

However, I do like your approach, so I will give it a try.

Thanks again,

Martin