[Aldor-l] Aldor-Meet

[Bill Page]

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?

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

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

> See also my modifications to
> http://axiom-wiki.newsynthesis.org/SandBoxAldorJoinAndMeet
>

Thanks.

Regards,
Bill Page.