Next: References Up: Finite Domains and Exclusions Previous: Conclusions

The RELFUN Meta-unify

Since this RELFUN unification meta-specification in RELFUN is deterministic (fortunately), there are many cuts (unfortunately) [2], which are, however, not needed for obtaining the first (and only) solution, just for preventing (meaningless) attempts to search for more solutions. Using RELFUN's relationalize command, this unify function would become a relation, also runnable in PROLOG, binding an additional first argument to the result substitution.


unify(X,Y,Environment) :-&
         unify-ua(ultimate-assoc(X,Environment),
                  ultimate-assoc(Y,Environment),
                  Environment).

unify-ua([bnd,Xvar,Xexpr],[bnd,Yvar,Yexpr],Environment) :-
         !& unify-bnd(Xexpr,Yexpr,Xvar,Yvar,Environment).
unify-ua([bnd,Xvar,Xexpr],Y,Environment) :-
         !& unify-bnd(Xexpr,Y,Xvar,[],Environment).
unify-ua(X,[bnd,Yvar,Yexpr],Environment) :-
         !& unify-bnd(X,Yexpr,[],Yvar,Environment).
unify-ua(X,Y,Environment) :- equal(X,Y) !& Environment.
unify-ua([vari|Namel],Y,Environment) :-
         !& [[[vari|Namel],Y]|Environment].
unify-ua(X,[vari|Namel],Environment) :-
         !& [[[vari|Namel],X]|Environment].
unify-ua([dom|Delem],[exc|Eelem],Environment) :-
         !& conjn(dom-exc([dom|Delem],[exc|Eelem]),Environment).
unify-ua([exc|Eelem],[dom|Delem],Environment) :-
         !& conjn(dom-exc([dom|Delem],[exc|Eelem]),Environment).
unify-ua([dom|Xdelem],[dom|Ydelem],Environment) :-
         !& conjn(dom-intersection([dom|Xdelem],[dom|Ydelem]),
                  Environment).
unify-ua([exc|Xeelem],[exc|Yeelem],Environment) :- !& Environment.
unify-ua([dom|Delem],Y,Environment) :-
         !& conjn(membern(Y,Delem),Environment).
unify-ua(X,[dom|Delem],Environment) :-
         !& conjn(membern(X,Delem),Environment).
unify-ua([exc|Eelem],Y,Environment) :-
         !& conjn(negn(membern(Y,Eelem)),Environment).
unify-ua(X,[exc|Eelem],Environment) :-
         !& conjn(negn(membern(X,Eelem)),Environment).
unify-ua(X,Y,Environment) :- atom(X) !& [].
unify-ua(X,Y,Environment) :- atom(Y) !& [].
unify-ua([Xfirst|Xrest],[Yfirst|Yrest],Environment) :-
         ! New-environment is unify(Xfirst,Yfirst,Environment) &
         conjn(New-environment,unify-args(Xrest,Yrest,New-environment)).

unify-args([],[],Environment) :- !& Environment.
unify-args([],Y,Environment) :- !& [].
unify-args(X,[],Environment) :- !& [].
% vertical-bar treatment omitted: generate list from "|"-rest
unify-args([Xfirst|Xrest],[Yfirst|Yrest],Environment) :-
         ! New-environment is unify(Xfirst,Yfirst,Environment) &
         conjn(New-environment,unify-args(Xrest,Yrest,New-environment)).

unify-bnd([dom|Delem],[exc|Eelem],Xvar,Yvar,Environment) :-
         ! Differ is dom-exc([dom|Delem],[exc|Eelem]) &
         conjn(Differ,unify-bnd-env(Differ,Xvar,Yvar,Environment)).
unify-bnd([exc|Eelem],[dom|Delem],Xvar,Yvar,Environment) :-
         ! Differ is dom-exc([dom|Delem],[exc|Eelem]) &
         conjn(Differ,unify-bnd-env(Differ,Xvar,Yvar,Environment)).
unify-bnd([dom|Xdelem],[dom|Ydelem],Xvar,Yvar,Environment) :-
         ! Inter is dom-intersection([dom|Xdelem],[dom|Ydelem]) &
         conjn(Inter,unify-bnd-env(Inter,Xvar,Yvar,Environment)).
unify-bnd([exc|Xeelem],[exc|Yeelem],Xvar,Yvar,Environment) :-
         !& unify-bnd-env(exc-union([exc|Xeelem],[exc|Yeelem]),
                          Xvar,
                          Yvar,
                          Environment).
unify-bnd([dom|Delem],Y,Xvar,Yvar,Environment) :-
         neq([vari|Namel],Y) !&
         conjn(membern(Y,Delem),unify-bnd-env(Y,Xvar,Yvar,Environment)).
unify-bnd(X,[dom|Delem],Xvar,Yvar,Environment) :-
         neq([vari|Namel],X) !&
         conjn(membern(X,Delem),unify-bnd-env(X,Xvar,Yvar,Environment)).
unify-bnd([exc|Eelem],Y,Xvar,Yvar,Environment) :-
         neq([vari|Namel],Y) !&
         conjn(negn(membern(Y,Eelem)),
               unify-bnd-env(Y,Xvar,Yvar,Environment)).
unify-bnd(X,[exc|Eelem],Xvar,Yvar,Environment) :-
         neq([vari|Namel],X) !&
         conjn(negn(membern(X,Eelem)),
               unify-bnd-env(X,Xvar,Yvar,Environment)).
unify-bnd([vari|Namel],Y,Xvar,Yvar,Environment) :-
         ! New is unify([vari|Namel],Y,Environment) &
         conjn(New,unify-bnd-env([vari|Namel],Xvar,Yvar,New)).
unify-bnd(X,Y,Xvar,Yvar,Environment) :-
         ! New is unify(X,Y,Environment) &
         conjn(New,unify-bnd-env(Y,Xvar,Yvar,New)).

unify-bnd-env(Val,[vari|Xvarnamel],[vari|Yvarnamel],Environment) :-
         !& appfun(conjn(negn(equal([vari|Xvarnamel],[vari|Yvarnamel])),
                         [[[vari|Xvarnamel],[vari|Yvarnamel]]]),
                   [[[vari|Yvarnamel],Val]|Environment]).
unify-bnd-env(Val,Xvar,Yvar,Environment) :-
         !& appfun(appfun(conjn(Xvar,[[Xvar,Val]]),
                          conjn(Yvar,[[Yvar,Val]])),
                   Environment).


dom-intersection([dom|Xdelem],[dom|Ydelem]) :-&
         mk-dom(intersection(Xdelem,Ydelem)).
exc-union([exc|Xeelem],[exc|Yeelem]) :-& mk-exc(union(Xeelem,Yeelem)).
dom-exc([dom|Delem],[exc|Eelem]) :-& mk-dom(set-difference(Delem,Eelem)).

ultimate-assoc([vari|Namel],Environment) :-
         !& ultimate-assoc-binding([vari|Namel],
                                   assoc([vari|Namel],Environment),
                                   Environment).
ultimate-assoc(X,Environment) :- !& X.

ultimate-assoc-binding([vari|Namel],[],Environment) :- !& [vari|Namel].
ultimate-assoc-binding([vari|Namel],
                       [[vari|Namel],[dom|Delem]],
                       Environment)
     :- !& [bnd,[vari|Namel],[dom|Delem]].
ultimate-assoc-binding([vari|Namel],
                       [[vari|Namel],[exc|Eelem]],
                       Environment)
     :- !& [bnd,[vari|Namel],[exc|Eelem]].
ultimate-assoc-binding([vari|Namel],[[vari|Namel],Y],Environment) :-
         !& ultimate-assoc(Y,Environment).

mk-dom([]) :- !& [].
mk-dom([D]) :- !& D.
mk-dom([D|Ds]) :-& [dom,D|Ds].

mk-exc([]) :- !& _.
mk-exc(Eelem) :-& [exc|Eelem].

neq(X,X) :- !& false.
neq(X,Y).

negn([]) :- !.
negn(X) :-& [].

membern(E,[]) :- !& [].
membern(E,[E|Rest]) :- !& [E|Rest].
membern(X,[Y|Rest]) :-& membern(X,Rest).

assoc(N,[]) :- !& [].
assoc(N,[[N,V]|Ar]) :- !& [N,V].
assoc(N,[Af|Ar]) :-& assoc(N,Ar).

% conjn(X,Y)   acts like   if neq([],X) then Y else []
% appfun   is the normal functional append
% equal, intersection, union, set-difference   are built-ins: ground args
appendix

sloppypar


Harold Boley & Michael Sintek (sintek@dfki.uni-kl.de)