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

[William Sit]

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