%%% version 1.0-6 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % {log} standard library for dealing with % binary relations and partial functions % Version 1.0 % % (requires {log} with partial functions - setlog482-2 or newer) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % by Maximiliano Cristia' and Gianfranco Rossi % % Last update: January 2022 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- consult_lib. %%%%%%%%%%%%%% General predicates for dealing with binary relations %%%%%%%%%%%%%% and partial functions %%% in_dom(X,Rel): true if Rel is a relation and X belongs to %%% its domain in_dom(X,Rel) :- set(Rel) & [X,_] in Rel. %%% nin_dom(X,R): true if X does not belong to the domain of the %%% binary relation R nin_dom(X,R) :- forall(P in R, exists([X1],fst(P,X1) & X neq X1)). %%% dom_list(L,Dom): true if L is a list of n elements (n >= 0) %%% and Dom is the interval int(1,n) (n > 0) or the empty set (n = 0). dom_list(L,Dom) :- prolog_call((nonvar(Dom),!,R = int ; R = set)) & (R == int & dom_list3(L,Dom) or R == set & dom_list2(L,Dom) ). dom_list2([],Dom) :- Dom = {}. dom_list2([X|L],Dom) :- length([X|L],SList) & call(Dom = int(1,SList)). %%% dom_list3(?L,+Dom) dom_list3([],Dom) :- eq(Dom,{}). dom_list3(L,Dom) :- Dom = int(1,B) & 1 =< B & length(L,B). %%% ddom_list(L,Dom): same as dom_list/2 but delayed if nonvar(L) & nonvar(Dom) ddom_list(L,Dom) :- delay(dom_list(L,Dom), nonvar(L) & nonvar(Dom)). %%% ran_list(S,R) ran_list(S,R) :- list_to_set(S,R). %%% Composition of binary relations. circ(Q,R,QR) is true if %%% [X,Y] in R & [Y,Z] in Q <==> [X,Z] in QR circ(Q,R,S) :- comp(R,Q,S). %%% foplus(F,X,Y,G) %%% g = f \oplus \{(x,y)\} \land \{(x,x)\} \comp f = \{(x,\_)\} foplus(F,X,Y,G) :- (F = {[X,Y1]/F1} & [X,Y1] nin F1 & comp({[X,X]},F1,{}) & G = {[X,Y]/F1} or comp({[X,X]},F,{}) & G = {[X,Y]/F} ). %%% the negation of applyTo n_applyTo(F,X,Y) :- ncomp({[X,X]},F,{[X,Y]}). %%% the negation of comppf n_comppf(R,S,T) :- ncomp(R,S,T) or delay(npfun(R),false) or delay(npfun(S),false) or delay(npfun(T),false). %%% the negation of drespf n_drespf(A,R,S) :- ndres(A,R,S) or delay(npfun(R),false) or delay(npfun(S),false). %%% F is a bijective function %%% note that when F is finite, bijective and injective is the same bij(F) :- pfun(F) & inv(F,M1) & pfun(M1). %%% the negation of bij nbij(F) :- npfun(F) or (inv(F,M1) & npfun(M1)). %%% F is a total bijective function from A to B t1to1(F,A,B) :- pfun(F) & dom(F,A) & ran(F,B) & inv(F,M1) & pfun(M1). %%% R is an equivalence relation on E equivalence(R,E) :- subset(R,cp(E,E)) & comp(R,R,M1) & subset(M1,R) & id(E,M2) & subset(M2,R) & inv(R,R). %%% Y is the relational image of X through F %%% when F is a function fimg(F,X,Y) :- pfun(F) & id(X,M1) & comppf(M1,F,M2) & ran(M2,Y). %%% alternate definition for rimg rimg2(R,X,Y) :- id(X,M1) & comp(M1,R,M2) & ran(M2,Y). %%% domain functional restriction %%% same as dres but for functions dfes(X,F,G) :- pfun(F) & id(X,M1) & comppf(M1,F,G). %%% the negation of dfes ndfes(X,F,G) :- pfun(F) & id(X,M1) & ncomp(M1,F,G). %%%%%%%%%%%%%% General predicates for dealing with relations and lists %%% list_to_rel(L,R): true if L is a list of n elements e_1,...,e_n (n>=0) %%% and R is a binary relation of the form {[1,e_1],...,[n,e_n]} list_to_rel([],{}). list_to_rel([X|List],Rel) :- Rel = {[1,X]/R} & [1,X] nin R & list_to_rel0(List,R,2). %%% list_to_rel0(L,R,N): same as list_to_rel(L,R) but R is a binary %%% relation of the form {[N,e_1],...,[N+n,e_n]} list_to_rel0([],{},N). list_to_rel0([X|List],Rel,N) :- Rel = {[N,X]/R} & K is N + 1 & list_to_rel0(List,R,K). %%% squash(S,L): true if S is a set of ordered pairs whose first %%% components are natural numbers >= 1, L is a list containing %%% the elements Y, for all [X,Y] in S, and L is ordered according %%% to the values of X (e.g., squash({[2,a],[7,b],[4,c]},L) ==> %%% [a,c,b]) squash({},[]). squash(Rel,List) :- Rel neq {} & List neq [] & dom(Rel,D) & set_to_list(D,LD) & prolog_call(sort(LD,SLD)) & squash0(Rel,SLD,List). squash0(Rel,[],[]). squash0(Rel,[N|List],NewList) :- [N,X] in Rel & NewList = [X|L] & squash0(Rel,List,L). %%%%%%%%%%%%%%%%%% Auxiliary predicates fst([X,Y],X). snd([X,Y],Y). %%%%%%%%%%%%%% Labeling predicates for relations and partial functions %%% rel(F,N): true if F is a binary relation, N is an integer constant %%% and |F| =< N rel(F,N) :- delay(mk_rel(F,N),nonvar(F)). mk_rel(F,N) :- nonvar(N) & solve(M in int(0,N) & mkset_term(F,M)) & rel(F). %%% pfun(F,N): true if F is a partial function, N is an integer constant %%% and |F| =< N pfun(F,N) :- delay(mk_pfun(F,N),nonvar(F)). mk_pfun(F,N) :- nonvar(N) & solve(M in int(0,N) & mkset_term(F,M)) & pfun(F). mkset_term({},0). mkset_term(S,N) :- N > 0 & eq(S,{_/R}) & N1 is N-1 & mkset_term(R,N1). label(pfun,F,N) :- % for backward compatibility delay(mk_pfun(F,N),nonvar(F)). %%% label(set,L): true if S is a partial function %%% when S is a variable, used to generate all partial functions of increasing %%% cardinality (starting from {}) label(pfun,S) :- nonvar(S) & pfun(S). label(pfun,S) :- var(S) & is_pfun(S). %%% is_rel(R): true if R is a binary relation, i.e. a set %%% of ordered pairs [X,Y]; %%% if R is a variable, then R is instantiated to inceasingly larger sets is_rel(R) :- forall(P in R, pair(P)). %%% dis_rel(R): same as is_rel(R), but delayed if nonvar(R) dis_rel(R) :- delay(is_rel(R), nonvar(R)). %%% is_pfun(F): true if R is a partial function, i.e. a set %%% of ordered pairs [X,Y] with distinct first components; %%% if F is a variable, then F is instantiated to inceasingly larger sets is_pfun(F) :- forall(P1 in F, forall(P2 in F, nofork(P1,P2))). nofork([X1,Y1],[X2,Y2]) :- (X1 neq X2 or (X1 = X2 & Y1 = Y2)).