[Aldor-l] Aldor-Meet

[Oleg Golubitsky]

Hi Ralf,

> define C: Category == Meet(C1,C2);
> D1: C1 == add {...}
>
> should
>    a) "D1 has C"            give true or false,
False, I think, because `D1' has not been explicitly declared
a member of the named category `C'.
>    b) "D1 has Meet(C1,C2)"  give true or false?
True, regardless of whether we use definition "1)" or "2)"
above, because category `Meet(C1,C2)' is unnamed and
by analogy with the semantics of "Dom has Join(Cat1, Cat2)".

> > i. if we use definition "1)" then it might be hard to find
> >    good examples for `Meet', because one can always
> >    define category `C' first, and then define `C1' and `C2'
> >    both as `C with { something }' instead of defining first
> >    `C1' and `C2' and using `C == Meet(C1,C2)'.
>
> That is simply wrong. I'll write a library abc, and give you the file
> libabc.al. In abc I define the categories
> Group, SemiGroup, and RingWithOne and domains D1:Cat1,..., Dn: Catn
> where each of Cati exports
>
> SemiGroup with {1:%}
>
> See
> http://aldor.org/pipermail/aldor-l_aldor.org/2007-November/000817.html
>
> Now you would like to define "Monoid". How can you do it *before*?
>
> Clearly, you could use "extend" for D1 up to Dn. But you would not like
> to do this if n is relatively big or changes with the next release of my
> library.
On the contrary, I might want to stick to the rule "domain `D' has
a named category `C' only if `D' has been explicitly declared to be
a member of `C' (either initially, or through a post facto extension)".
Extending a large number of existing domains to a new category
automatically may be error-prone: it may happen that all these
domains have the right exports, yet some of them do not satisfy
all the axioms that the new category presumes. By explicitly writing
`extend Di: Monoid' we can state that `Di' does satisfy all axioms
of monoids.

Note that `define Monoid == Meet(Group, RingWithOne)' is correct
only if we use definition "1)" of `Meet'. But that definition ignores
the names "Group" and "RingWithOne", since it would produce the
same (=indistinguishable) result if we used any other two categories
with the same intersection of exports. So it cannot imply that
members of the new category `Monoid' satisfy the axioms of monoids.

It is true that, if definition "2)" of `Meet' is chosen, there is no way
to define `Monoid' in terms of its subcategories `Group' and `RingWithOne'.
However, such a definition may also seem counter-intuitive (and in fact
it does not appear in text books). Unless we reverse it, i.e., interpret it as
follows:
  Let `Monoid' be a new category whose exports are functions
        exported by `Group' and `RingWithOne';
  Let `Group' now be declared post-facto to be a subcategory of `Monoid';
  Let also `RingWithOne' now be declared post-facto to be a
subcategory of 'Monoid'.
But, since this changes the meaning of `Group and `RingWithOne',
shouldn't the latter rather appear in the left-hand-side of the definition?

If I were to define Monoid post facto, I would prefer to use difference,
rather than `Meet', i.e., say something like:
   define Monoid: Category == Group without { inverse: % -> % }
But I am not sure if difference is a legitimate operation, i.e.,
if it can in principle be efficiently implemented.
(Stephen, do I remember it correctly that you mentioned once that
 the difference operation makes the "has" test NP-complete?)

> > ii. for definition "2)" there is an example.
> >     A bivariate polynomial can be viewed as an element of
> >      a) R[x,y]    (free module with the monomial basis)
> >      b) R[x][y]   (polynomial ring over the univariate polynomial ring)
> >     So one could define the category of bivariate polynomials
> >     as the `Meet' of "a)" and "b)".
>
> That doesn't sound too convincing. I rather have an inefficient
>    deg: % -> N^n
> function than non at all.
It is true that R[x][y] will not export such a function.
However, it is conceivable to have conversions between various
views of a polynomial (call them `coerce').
In which case we could say `(deg coerce p)@N^2' for a polynomial
`p' belonging to a domain that is a member of R[x][y].
Note also that the signature
     deg: % -> N^n
does not generalize to polynomials in infinitely many variables,
e.g. differential polynomials. One might want to have the total
degree function
    tdeg: % -> N
exported by all kinds of polynomials. But that is be doable
for R[x][y], if one defines the total degree of a univariate
monomial `r*x^i' over a graded ring to be 'i+deg(r)'.

Oleg