[Aldor-l] Aldor-Meet

[Ralf Hemmecke]

Hello Bill,

On 11/20/2007 03:38 PM, Bill Page wrote:
> On 11/20/07, Ralf Hemmecke wrote:
>> Bill Page wrote:
>>> Also I notice that apparently 'Meet' does not interact with 'has' as
>>> one might expect:
>>>
>>> define M12:Category == Meet(C1,C2);
>>>
>>> D1: C1 == add {
>>>   f: Integer == 1;
>>>   g: Integer == 2;
>>> }
>>>
>>> D2: C2 == add {
>>>   f: Integer == 1;
>>>   h: Integer == 3;
>>> }
>>>
>>> Both D1 has M12 and D2 has M12 evaluate as False. If Meet is the
>>> intersection like Join is the union of two categories then I think
>>> they should both return True, i.e. that C1 and C2 should be
>>> subcategories of Meet(C1,C2) like Join(C1,C2) is a subcategory of C1
>>> and C2. No?
>> I think that "D1 has M12" returns false is OK, since M12 is a new
>> category and D1 has not explicitly been declared to be a member of that
>> category.
>>
> 
> I remain a little confused over the use of 'define', but I think you
> are right. I must remind myself that Aldor treats differently *named*
> categories as distinct. I presume that you would agree that if I wrote
> this as a macro:
> 
>  macro M12 == Meet(C1,C2);
> 
> then D1 has M12 should be true?

Yes. That should have been the demonstration of the program below. 
Unfortunately, the compiler produces code that returns "false". A bug???

>> However, for the following program I would have expected (F, T, T).
>>
>> ---BEGIN aaa.as
>> #include "aldor"
>> #include "aldorio"
>> Z==>Integer;
>> define C1:Category == with {f: Z; g: Z}
>> define C2:Category == with {f: Z; h: Z}
>> define M12:Category == Meet(C1,C2);
>> D1: C1 == add {f: Z == 1; g: Z == 2}
>> D2: C2 == add {f: Z == 1; h: Z == 3}
>> D: M12 == add {f: Z == 4}
>> import from Boolean;
>> stdout << "D1 has M12  = " << (D1 has M12) << newline;
>> stdout << "D1 has Meet = " << (D1 has Meet(C1, C2)) << newline;
>> stdout << "D1 has f    = " << (D1 has with {f: Z}) << newline;
>> ---END aaa.as
>>
>>  >aldor -fx -laldor aaa.as
>>  >aaa
>> D1 has M12  = F
>> D1 has Meet = F
>> D1 has f    = T
>>
>> That looks like a bug---Well, it's not, because gave a clear definition
>> of "Meet".
> 
> ? I am not sure exactly what you meant to say here except perhaps to
> repeat that there is no formal definition of Meet. I think however
> that Oleg's approach is correct.

If we accept Oleg as the authority who defines the language then I must 
agree. I would have guessed exactly the same as Oleg. Would you accept 
me as someone who defines the Aldor language? I don't care what the 
compiler implements, I care about an official specification.

 > If there is such a category
> constructor as Meet, then surely we can deduce how it should operate
> based on some more general theory into which it would naturally fit.
> Probably that
> 
>   D1 has Meet(C1, C2)
> 
> does not return True is just an oversight - not so important since one
> can always write:
> 
>   D1 has C1 or D1 has C2
> 
> Similarly
> 
>   D1 has Join(C1,C2)
> 
> would be written
> 
>   D1 has C1 and D1 has C2
> 
> Right?

Looks right.

>> But as you said, Bill, I would also like to see a proper use case
>> for the "Meet" feature.

> Intuition says that this dual category constructor *should* be
> interesting but if experience with category theory is any guide, then
> we might need to be quite creative to find it's actual application.
> Speaking philosophically, I think this (usually) is a sign of a good
> language - one where a natural construction leads to a question about
> what it should mean.

> I suppose that Meet must have something to do with generalization
> since the Meet of two categories is a "larger" (more general)
> super-category as opposed to Join which is always something more
> specific, i.e. a sub-category. The reason for defining such a more
> general category is presumably because we wish to use it to define a
> domain in that category - something more general than the domains that
> are members of the component categories.

> It seems to me that specialization is the normal "top down" approach
> for designing categories and domains in Aldor (and in Axiom), but that
> generalization based on Meet might also be a useful "bottom-up"
> approach.

Maybe. "Meet" would allow to create more general categories based on
existing ones. That would allow to introduce categories in the middle of 
an Aldor category hierarchy. Oh... now I remember that Stephen said 
something in that direction at the 2007 Aldor workshop.

For example, you have Group, SemiGroup, and RingWithOne. Imagine now you 
have a lot of domains that export

SemiGroup with {1: %}

Maybe now you want to introduce a category Monoid with exactly those 
exports. Would you like to say

extend D1: Monoid == add;
...
extend Dn: Monoid == add;

for all the n domains that I mentioned above? Hopefully you don't forget 
one.

If you just would have to say

define Monoid: Category == Meet(Group, RingWithOne);

and all the "has" constructions would work properly, actually now I 
believe they should work as you asked for it initially, i.e.

The program from
   http://aldor.org/pipermail/aldor-l_aldor.org/2007-November/000815.html
should return "true" for all the three cases.

But now it is even more important that Meet gets a proper definition, 
since without an "extend", D1 would not explicitly have been declared to 
be of category "Monoid" and so "D1 has Monoid" should return false 
according to the AUG.pdf p. 81:

Quote:
   Note that Aldor is constructed so that a domain is only a member
   of a named category if it explicitly inherits from the category---not
   if it merely exports the same collection of (explicit) declarations.

Ralf