%======= Characterizations of attributes and keys ======= %?defAs( flagDom(A,Flag), un(dom(A),opp(Flag)) ). defAs( flagDom(_;zero), u ). defAs( flagDom(A;one), dom(A) ). defThAs( 'Attr'(A,C,Y,Mandatory), % 0 means optional, 1 means mandatory [ 'RUniq'(A), % an attribute is a function, subseteq(dom(A),C), % defined on certain entities of its realm, subseteq(img(A),Y), % and whose values are individuals (no tuples) subseteq(C,flagDom(A,Mandatory)) ] ). defAs( keyPlH([_]), z ). defAs( keyPlH([P,A|As]), un(int(P,img(A)), keyPlH([P|As])) ). defFoAs( isKeyPlH(PAs), z_keyPlH(PAs) ). defThAs( 'KeyPlH'([P]), 'Coll'(P) ). defThAs( 'KeyPlH'([P,A|As]), [z_int(P,img(A)) | 'KeyPlH'([P|As])] ). defAs(keyFunc(([A],L,R;I)), circ(succth(L,R,I),rev(A))). defAs(keyFunc(([A0,A1|As],L,R;decr(I))), int(circ(th(L,R,I), rev(A0)), keyFunc([A1|As],L,R,I))). defThAs( 'Key'([P,L,R|As]), ['RUniq'(keyFunc(As,L,R,0)) | 'KeyPlH'([P|As])] ). %======= Uniqueness conditions for placeholders ========= defAs( lBoth(R,S), int( rA(R), rA(S) )). defFoAs( 'NoLLBoth'(P,R,S), z_int(lBoth(R,S), P) ). defFoAs( 'NoLRBoth'(P,R,S), 'NoLLBoth'(P,R,rev(S)) ). defFoAs( 'NoTogether'(P,R), z_int(int(rA(P),lA(P)),R) ). %% Ernst Doberkat's proposal %% defFoAs( 'RXcl'(P,R), z_int(int(lA(P),rA(opp(P))), bros(R)) ). %% R has no two pairs [a,*], [a,b] with: %% "*" a placeholder and "b" not a placeholder %% defFoAs( 'LXcl'(P,R), 'RXcl'(P,rev(R)) ). %% R has no two pairs [*,b], [a,b] with: %% "*" a placeholder and "a" not a placeholder %% Eugenio Omodeo's proposal defFoAs( 'RXcl'(P,R), z_int(mult(R),lA(P)) ). defFoAs( 'LXcl'(P,R), 'RXcl'(P,rev(R)) ). defThAs( 'NoTwice'([P]), true(P) ). defThAs( 'NoTwice'([P,R|T]), [ 'RUniq'(P,R), % a placeholder occurs at most once in the domain of R 'LUniq'(P,R), % a placeholder occurs at most once in the image of R 'NoTogether'(P,R), % no pair in R has placeholders on both sides 'RXcl'(P,R), % R has no two pairs [a,*], [a,b] with: % "*" a placeholder, and "b" different from "*" 'LXcl'(P,R) % R has no two pairs [*,b], [a,b] with: % "*" a placeholder and "a" different from "*" | 'NoTwice'([P|T]) ]). defThAs( 'NoLRBoth'([P,R]), true([P,R])). defThAs( 'NoLRBoth'([P,R,S|T]), [ 'NoLLBoth'(P,R,S), % there is no placeholder occurring on the left % of a pair both in R and in S 'NoLRBoth'(P,R,S), % there is no placeholder occurring on the left % of a pair in R and on the right of a pair in S 'NoLRBoth'(P,S,R) % there is no placeholder occurring on the left % of a pair in S and on the right of a pair in R | 'NoLRBoth'([P,R|T]) ]). defThAs( 'NoBoth'([P]), true(P) ). defThAs( 'NoBoth'([P,R|T]), [ 'NoLRBoth'(P,R,R) % no placeholder occurs both as a first and as a second % component in R | { 'NoLRBoth'([P,R|T]), 'NoBoth'([P|T]) } ] ). defThAs( 'PlaceHolders'([P,R|T]), % it is understood that 'Coll'(Y)... % ...so that 'Coll'(P) will hold as well {'NoTwice'([P,R|T]),'NoBoth'([P,R|T])} ). %=== Entities relative to a collection P of placeholders: === defThAs( 'Entity'(P,E), ['Coll'(E), 'Disj'(E,P) ] ). % the following predicate treats an IsA-chain defThAs( 'IsA'([Y,P,F]), [id], [ % it is understood that 'Coll'(Y)... subseteq(F,Y), 'Disj'(F,P) % ...so that 'Entity'(P,F) ]). defThAs( 'IsA'([Y,P,E,F|T]), [id], [ subseteq(E,F) | 'IsA'([Y,P,F|T]) ]). %=== Bi-total relation between two entities: === defThAs( 'DotDot'( P, E, R, F ), % it is understood that 'Coll'(E), 'Coll'(F)... [ 'Betw'( symm(E,P), R, symm(F,P) ), subseteq( F, lA( R ) ), % ...hence isSurj( R, F )... subseteq( E, rA( rev( R ) ) ) % ...hence isSurj( R, E ) ]). defThAs( 'DotDot'( [P, E, R, F] ), 'DotDot'(P,E,R,F) ). %=== Entity-Relationship modeling: ======================== defThAs( 'LUniqs'([]), [] ). defThAs( 'LUniqs'([Func|Funcs]), [ 'LUniq'(Func) | 'LUniqs'(Funcs) ]). defThAs( 'RUniqs'([]), [] ). defThAs( 'RUniqs'([Func|Funcs]), [ 'RUniq'(Func) | 'RUniqs'(Funcs) ]). defThAs( 'Uniqs'(L,R), [ true([L,R]) | {'LUniqs'(L), 'RUniqs'(R)} ]). defThAs( 'IsAChains'([Y,P]), true([Y,P])). defThAs( 'IsAChains'([Y,P,IsACh|IsAChs]), [ true(Y) | {'IsA'([Y,P|IsACh]), 'IsAChains'([Y,P|IsAChs])} ]). defThAs( 'DotDots'([P]), true(P)). defThAs( 'DotDots'([P,Dom,Rel,Img|DtDts]), [ 'DotDot'(P,Dom,Rel,Img) | 'DotDots'([P|DtDts]) ]). defThAs( 'Attrs'([Y]), true(Y)). defThAs( 'Attrs'([Y,At,En,Ma|As]), [ true(Y) | {'Attr'(At,En,Y,Ma), 'Attrs'([Y|As])} ]). defThAs( 'Keys'([P,L,R]), true([P,L,R])). defThAs( 'Keys'([P,L,R,As|FurtherKeys]), [ true(P) | {'Key'([P,L,R|As]), 'Keys'([P,L,R|FurtherKeys])} ]). defThAs( 'Attrs'(Ats,Kys), [ true([Ats,Kys]) | {'Attrs'(Ats), 'Keys'(Kys) } ]). % TEMPORARY, UNTIL SOME CURRENT LIMITATIONS OF Anamorpho ARE ELIMINATED: defThAs( 'IsAChains'(YN,PN,IsAChns,DotsDots), [ true([YN,PN]) | {'IsAChains'([YN,PN|IsAChns]), 'DotDots'([PN|DotsDots])} ]). % TEMPORARY, UNTIL SOME CURRENT LIMITATIONS OF Anamorpho ARE ELIMINATED: defThAs( 'Uniqs'(YN,PN,IsAChns,DotsDots,LeftUniques,RightUniques), [ true([YN,PN]) | {'IsAChains'(YN,PN,IsAChns,DotsDots), 'Uniqs'(LeftUniques, RightUniques)} ]). % TEMPORARY, UNTIL SOME CURRENT LIMITATIONS OF Anamorpho ARE ELIMINATED: defThAs( 'Uniqs'(YN,PN,IsAChns,DotsDots,LeftUniques,RightUniques, Attributes,LN,RN,Kys), [ true([YN,PN]) | {'Uniqs'(YN,PN,IsAChns,DotsDots,LeftUniques,RightUniques), 'Attrs'([YN|Attributes],[PN,LN,RN|Kys])} ]). % MOST IMPORTANT FOR THE TRANSLATION OF ER-models INTO MAPALGEBRA: defThAs( 'ERmodel'(IsAChns, Relations,DotsDots, LeftUniques,RightUniques, Attributes,Kys, PlHolders,Left,Right,Individuals,NullTup,PN,LN,RN,YN,NN), [ defAs( @(PN), PlHolders ), defAs( @(LN), Left ), defAs( @(RN), Right ), defAs( @(YN), Individuals ), defAs( @(NN), NullTup ), 'HdTlFlat'(PN,LN,RN,YN,NN) | { 'PlaceHolders'([PN|Relations]), 'Uniqs'(YN,PN,IsAChns,DotsDots,LeftUniques,RightUniques, Attributes,LN,RN,Kys) } ]).