Unification - Infinity of results

I'm developing (in Java), for fun, an applic开发者_如何学Cation which uses an unification algorithm.

I have chosen that my unification algorithm returns all the possible unifications. For example, if I try to solve

add(X,Y) = succ(succ(0))

it returns

{X = succ(succ(0)), Y = 0}, {X = succ(0), Y = succ(0)}, {X = 0, Y = succ(succ(0))}

However, in some cases, there exists an infinite number of possible unifications (e.g. X > Y = true).

Does someone know am algorithm allowing to determine if an infinite number of unifications may be encountered?

Thanks in advance

In the context of Prolog, when you say "unification", you usually mean syntactic unification. Therefore, add(X, Y) and succ(succ(0)), do not unify (as terms), because their functors and arities differ. You seem to be referring to unification modulo theories, where distinct terms like add(X, Y) and succ(succ(0)) can be unified provided some additional equations or predicates are satisfied. Syntactic unification is decidable, and the number of possible unifiers is infinite if, after applying the most general unifier, you still have variables in both terms. Unification modulo theories is in general not decidable. To see that already basic questions can be hard consider for example the unification problem N > 2, X^N + Y^N = Z^N over the integers, which, if you could easily algorithmically decide whether or not a solution exists (i.e., whether the terms are unifiable modulo integer arithmetic), would immediately settle Fermat's Last Theorem. Consider also Matiyasevich's theorem and similar undecidability results.

In certain constraint logic programming systems you can easily see if the solution set is infinite or not. For example in some CLP(FD) implementations (i.e. SWI-Prolog, Jekejeke Minlog, other implementations such as GNU Prolog and B-Prolog not, since they assume a finite upper/lower bound) a certain degree of reasoning with infinite integer sets is thus supported. This is seen by interval notations such as (SWI-Prolog):

?- use_module(library(clpfd)).
true.

?- X #\= 2.
X in inf..1\/3..sup.

But there is a disadvantage of those sets, they cannot be used in CLP(FD) labeling where the elements of the set are enumerated and a further attempt to solve the instantiated equations is made. It would also run counter to the following result, if something could be done in general to decide CLP(FD) queries:

"In 1900, in recognition of their depth, David Hilbert proposed the solvability of all Diophantine problems as the tenth of his celebrated problems. In 1970, a novel result in mathematical logic known as Matiyasevich's theorem settled the problem negatively: in general Diophantine problems are unsolvable." (From Wikipedia on Diophantine equations)

Another constraint logic programming that can usually also deal with infinite solution sets is CLP(R). The reasoning among equations is a little stronger there. For example CLP(FD) does not detect the following inconsistency (depends on the system, this is the result for SWI-Prolog, in Jekejeke Minlog you will immediately see a No for the second query, and GNU Prolog will loop for around 4 secs and then say No):

?- X #> Y.
Y#=<X+ -1.

?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.

On the other hand CLP(R) will find:

?- use_module(library(clpr)).

?- {X > Y}.
{Y=X-_G5542, _G5542 > 0.0}.

?- {X > Y, Y > X}.
false.

Constraint systems work by implementing algorithms from number theory, linear algebra, analysis, etc.. depending on the domain they model, i.e. what * denotes in the notation CLP( * ). These algorithms can go as far as quantifier elimination.

Bye