On Tue, Aug 5, 2008 at 4:20 PM, Gabriel Dos Reis wrote:
>
>
> The category SetAggregate exports a partial ordering operation for
> set inclusion under the name "<".  I consider this harmful.  The
> principal reason is that since set inclusion is a *partial ordering*,
> its spelling should not be tied to "<", or any other usual relational
> comparison because the interpreter (and the compiler in older
> versions of Axiom) do *syntactic* replacements of x >= y by
> not (x < y) -- and my other misguided syntactic transformations,
> -- which is true only if we had a total ordering.
>
> Thoughts?
>

As you said: simple syntactic transformations of this kind are
"misguided". I think that first of all such transformations should be
eliminated. On the other hand, it seems to me that the issue is not
the name of the operation but rather the category to which the
operation belongs. 'SetAggregate' does have an *attribute* named
'partiallyOrderedSet'. I do not understand why this is an attribute
and not a category with specific exports.

I agree that explicitly exporting '<'  from SetAggregate is harmful.
Similarly explicitly exporting 'subset?' is also wrong. It is
conventional to use a symbol such as '<=' for partial ordering, and I
think it would be usefully represented as an export of a category
'PartiallyOrderedSet' that satisfies the axioms:

    * a <= a (reflexivity);
    * if a <= b and b <= a then a = b (antisymmetry);
    * if a <= b and b <= c then a <= c (transitivity).

for all a, b, and c in P, where P has PartiallyOrderedSet. Then
SetAggregate should be a subcategory of PartiallyOrderedSet which in
turn is a subcategory of SetCategory  (which provides the equivalence
relations '=' and '~=' from BasicType). Similarly if some domain has
the category 'OrderedSet' and exports the symbols '<', '<=', '>' and
'>=' then it makes sense that a default implementation of 'x >= y' can
be given by 'not (x < y)'.

It seems to me that this sort of mathematical knowledge (semantics) is
correctly captured by the appropriate design of the Axiom library. In
general I think it should not be built-in to either the compiler or
the interpreter. But *if* (and I am not sure that this antecedent
really applies) there is some important optimization that could be
done if such knowledge if more directly available to either the
compiler or the interpreter, then I think it *might* be appropriate if
some built-in knowledge of the associated categories was assumed which
would enable such transformations.

Regards,
Bill Page.

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Reply via email to