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

[William Sit]

Dear Martin:

Martin Rubey wrote:

> The general case
> 
> We have a category A with an operation op: % -> %. However, there are natural
> subdomains of domains of A, which are no longer closed under op.
> 
> Can you propose a "natural" hierarchy of categories for this situation?  Since
> this occurs so often, I hope that there is a nice solution...
> 

There are many such cases already in very simple domains. For example, in
Integer, we have - (minus), but not / (divide). Also minus is not close under
PositiveInteger or NonNegativeInteger. In Axiom, NNI has
CancellationAbelianMonoid under +, 
PI has Monoid under *. Integer has Ring.  So if the analogy is the category A is
Ring, the op is minus or divide, the domain of A is Integer, the subdomains are
NNI and PI. To answer your questions, we have simply to analyse how Axiom set up
such hierarchy.

What Axiom does is to let the subdomains belong to a more general category B for
which the category A belongs. In the above, B is either the
CancellationAbelianMonoid category or the Monoid category. In the category B,
Axiom exports op or opIfCan. For example,  Monoid exports recip:%->(%,"failed"),
and CancellationAbelianMonoid exports subtractIfCan. Also, IntegralDomain
exports exquo (which could have been named divideIfCan). 



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

Let's review one definition of a matroid. According to Lawler (Combinatorial
Optimization, Networks and Matroids), p. 268, a matroid is a pair (E, I), where
E is a finite set, and I is a family of subsets of E satisfying two axioms:
(1) the empty set is in I, and every proper subset of a set in I is in I.
(2) If A and B are sets in I with p and p+1 elements respectively, then there is
a b in B, not in A such that A union {b} is in I.

Then given a matroid (E, I), there is always a dual matroid M^D = (E, I^D)
(Theorem 8.1, p. 280).

A matroid M therefore is really given by I, a set of subsets of E. We may
therefore think of "elements" of M as subsets of E. In order to construct the
dual of an arbitrary matroid, you need to be able to capture the defining sets E
and I. So, ideally (reading % to mean Set E)

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

You can construct domains in MatroidCat, for example:
    
    Matroid(E:Finite, I:Set Set E):MatroidCat == ... with
      ...
      Rep:= Record(elist: Set E)

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)

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

   
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.
 
> However, a very important class of matroids, called "graphic matroids", do 
> have
> this operation only if the matroid is "planar". (In fact, "graphic matroids"
> are simply undirected, unweighted graphs)
> 
> Since "graphic matroids" are so important, I would like to have a category
> "GraphicMatroidCat", and since they are matroids I'd like to have it inherit
> from "MatroidCat". But this is impossible, since the class is not closed under
> duality.

This needs some clarification.
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.

This means two domain constructors:

    GraphicMatroid(G: GraphCat):MatroidCat == ...

    CographicMatroid(G: GraphCat):MatroidCat == ...
    
Note: graphic matroids are matroids.

> Or, maybe even better, the dual of a graphical non-planar matroid would simply
> yield a general matroid.

This is what I understand from Lawler: Given a planar graph G, there corresponds
non-uniquely a plane graph (not a graph, but a drawing) from which one can
construct a geometric dual G*, which may be a graph or a multigraph. If G* is
planar, it is called a dual graph of G and denoted by G^D. (p. 33). If G has a
dual graph G^D, then the graphic matroid of G is the cographic matroid of G^D
and vice versa. A graph G is planar if and only if its graphic matroid is
cographic, which is if and only if its cographic matroid is graphic. (p. 281).

This means more domain constructors:

   Planar?(G:GraphCat):Boolean == ...  (in other words, G has Planar)

   Draw(G:GraphCat): ??? == ... (this is not practical!)

   GeometricDual(G:GraphCat):GraphCat == ... 

   Dual(G:GraphCat):GraphCat == ...

   Equal(G1:GraphCat, G2:GraphCat): Boolean == ...

Again, ideally, we can do this:

   GraphCat(...):Category == ...
     nodeSet: () -> Finite
     arcSet: () -> List DirectProduct(2, nodeSet())
     graphicMatroid:() ->MatroidCat
     cographicMatroid:() ->MatroidCat
     planar?: () -> Boolean
     geometricDual:() -> Union(GraphCat, "failed")
     dual: () -> Union(GraphCat, "failed")
     equal: DirectProduct(2, GraphCat) -> Boolean

One last comment: this has little to do with the closure problem.    
 
> Example 2, Differential Equations
> 
> A Holonomic function is a function f -- say in one variable x -- that 
> satisfies
> a differential equation with polynomial coefficients:
> 
>   p_k(x) f^(k) (x) + ... + p_2(x) f''(x) + p_1(x) f'(x) + p_0(x) f(x) = q(x)
> 
> where f^(k) is the k_th derivative of f and p_i and q are polynomials.
> 
> It is quite easy to see that the class of holonomic functions is closed under
> integration, i.e., integrating a holonomic function yields again a holonomic
> function. This is quite an important property, of course, so a priori, I'd 
> like
> to export it in "HolonomicCat".
> 
> If we take k=0 in the equation above we obtain the class of rational
> functions. Since rational functions are so important, I'd like to have a
> category "RatCat". However, we all know that the class of rational functions 
> is
> *not* closed under integration, the simplest example being 1/x.

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.

The two examples you gave present two different problems.

William