login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBox Aldor Join and Meet revision 7 of 9

1 2 3 4 5 6 7 8 9
Editor: Bill Page
Time: 2007/11/21 11:32:36 GMT-8
Note: lattice absorption axioms fail to compile

added:

--Evaluating more complex Meet/Joint expressions causes seg fault:
--main5():Record(D1hasMeetJoin:Boolean, D1hasJoinMeet:Boolean) ==
--  [D1 has Meet(C1,Join(C1,C2)), D1 has Join(C1,Meet(C1,C2))];

added:
-- expect True, True
--main5()

Aldor-Meet

On Date: Nov 19, 2007 10:58 AM Oleg Golubitsky wrote to aldor-l <aldor-l@aldor.org>:

By analogy with 'Join', 'Meet(C1,C2)' should return a category which has the intersection of exports of 'C1' and 'C2'.

A simple test (see below) confirmed this semantics; I also could not find a description of 'Meet' in the guide.

begin{aldor} #include "aldor" define C1:Category == with {

f: Integer; g: Integer;

} define C2:Category == with {

f: Integer; h: Integer;

} D: Meet(C1,C2) == add {

f: Integer == 1; -- OK; if this line is commented out, error:
-- The domain is missing some exports. -- Missing f: AldorInteger?

} end{aldor}

The Axiom library apparently does not define 'Meet'. begin{aldor} #include "axiom" Meet(T: Tuple Category): Category == with;

define C1:Category == with {
f: Integer; g: Integer;

} D1: C1 == add {

f: Integer == 1; g: Integer == 2;

} define C2:Category == with {

f: Integer; h: Integer;

} D2: C2 == add {

f: Integer == 1; h: Integer == 3;

}

define M12:Category == Meet(C1,C2);

DM12: M12 == add {
f: Integer == 1; -- if this line is commented out, error:
-- The domain is missing some exports.

g: Integer == 2; h: Integer == 3;

}

define J12:Category == Join(C1,C2);

DJ12: J12 == add {
f: Integer == 1; g: Integer == 2; h: Integer == 3;

}

main1():Record(D1hasM12:Boolean,D2hasM12:Boolean) ==
[D1 has M12, D2 has M12]?;
main2():Record(M12hasC1:Boolean,DM12hasC2:Boolean) ==
[DM12 has C1, DM12 has C2]?;
main3():Record(DJ12hasC1:Boolean, DJ12hasC2:Boolean) ==
[DJ12 has C1, DJ12 has C2]?;
main4():Record(D1hasMeet:Boolean, D2hasMeet:Boolean, D1hasF:Boolean) ==
[D1 has Meet(C1,C2), D2 has Meet(C1,C2), D1 has with {f:Integer}]?;

--Evaluating more complex Meet/Joint expressions causes seg fault: --main5():Record(D1hasMeetJoin:Boolean, D1hasJoinMeet:Boolean) == -- [D1 has Meet(C1,Join(C1,C2)), D1 has Join(C1,Meet(C1,C2))]?; end{aldor}

begin{axiom} f()$DM12 -- expect not defined g()$DM12 -- expect not defined h()$DM12 f()$DJ12 g()$DJ12 h()$DJ12 end{axiom}

begin{axiom} -- expect False, False main1() end{axiom}

Comment of Ralf Hemmecke 20-Nov-2007: I would expect (false,false) for main2(), because, DM12 is not explicitly declared to be of type C1 or C2 even if its "add" domain has all the exports (except for the names C1 and C2). begin{axiom} -- expect True, True main2() -- expect True, True main3() -- expect True, True, True main4() -- expect True, True --main5() end{axiom} Comment of Ralf Hemmecke 20-Nov-2007: That main4() returns (false, false, true) should be considered a bug.