[Aldor-l] Aldor-Meet

[Ralf Hemmecke]

Hi Oleg,

On 11/20/2007 07:40 PM, Oleg Golubitsky wrote:
> 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'.

OK, but then I would argue that Meet is not really useful.
I would rather like it to return "true".

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

Fine. We can stick to that rule, but then I don't see a good use case 
for "Meet".

> Extending a large number of existing domains to a new category
> automatically may be error-prone:

That might be true.

> 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 depends. Since both Group and RingWithOne export SemiGroup, we should 
at least have the SemiGroup property. That 1 is neutral with respect to 
the * operation should also be inherited. Unfortunately, Aldor does not 
naturally allow to specify axioms and that is a big minus. Anyway, I 
would argue that Monoid should inherit also the (currently 
aldor-invisible) axioms from the categories in the Meet.

Hopefully, David Casperson doesn't say something else. It seems that 
Meet is more problematic than I thought.

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

Good argument.

Ralf