Unification - Infinité de résultats

Question

Je développe (en Java), pour le plaisir, une application qui utilise un algorithme d'unification.

J'ai choisi que mon algorithme d'unification renvoie toutes les unifications possibles. Par exemple, si je tente de résoudre

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

il retourne

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

Cependant, dans certains cas, il existe un nombre infini de possibles Unifications (par exemple X> Y = vrai).

Est-ce que quelqu'un connaît un algorithme permettant de déterminer si un nombre infini d'unifications peut être rencontré?

Merci à l'avance

Answer 1

Dans le contexte de Prolog, quand vous dites que "l'unification", vous voulez dire généralement unification syntaxique. Par conséquent, ajoutez (X, Y) et succ (succ (0)), ne vous unifiez pas (comme termes), parce que leurs foncteurs et arités diffèrent. Vous semblez faire référence à des théories modulo d'unification, où des termes distincts comme add (X, Y) et succ (succ (0)) peuvent être unifiés à condition que certaines équations ou prédicats supplémentaires soient satisfaits. L'unification syntaxique est décidable, et le nombre d'unificateurs possibles est infini si, après avoir appliqué l'unificateur le plus général, vous avez toujours des variables dans les deux termes. Les théories de l'unification modulo ne sont généralement pas décidables. Pour voir que les questions de base peuvent être difficiles, on peut par exemple considérer le problème d'unification N> 2, X^N + Y^N = Z^N sur les entiers, qui, si vous pouviez facilement déterminer si une solution existait ou non , si les termes sont unifiables modulo entier arithmétique), réglerait immédiatement le dernier théorème de Fermat. Considérons aussi le théorème de Matiyasevich et les résultats similaires d'indécidabilité.

Answer 2

Dans certains constraint logic programming systems, vous pouvez facilement voir si l'ensemble de la solution est infinie ou non. Par exemple, dans certaines implémentations CLP (FD), SWI-Prolog, Jekejeke Minlog, d'autres implémentations comme GNU Prolog et B-Prolog, puisqu'ils supposent une limite supérieure/inférieure finie, un certain degré de raisonnement avec des ensembles d'entiers infinis est donc pris en charge. Ceci est vu par les notations d'intervalle tels que (SWI-Prolog):

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

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

Mais il y a un inconvénient de ces ensembles, ils ne peuvent pas être utilisées dans l'étiquetage CLP (FD) où sont énumérés les éléments de l'ensemble et un une tentative supplémentaire de résoudre les équations instanciées est faite. Il serait également contraire au résultat suivant, si quelque chose pouvait être fait en général de décider CLP (FD) requêtes:

« En 1900, en reconnaissance de leur profondeur, David Hilbert a proposé la résolubilité de tous Diophantine problèmes comme le dixième de son problèmes célèbres.En 1970, un nouveau résultat dans la logique mathématique connu sous le théorème de Matiyasevich réglé le problème négativement: en problèmes diophantiens généraux sont insolubles. " (article de Wikipédia sur Diophantine equations)

Une autre programmation logique de contrainte qui peut habituellement traiter aussi avec des ensembles de solutions infinies est CLP (R). Le raisonnement parmi les équations est un peu plus fort là.Par exemple CLP (FD) ne détecte pas l'incohérence suivante (dépend du système, c'est le résultat pour SWI-Prolog, dans Jekejeke Minlog vous verrez immédiatement un non pour la deuxième requête, et GNU Prolog boucle pendant environ 4 secondes puis dire Non):

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

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

d'autre part CLP (R) trouveront:

?- use_module(library(clpr)). 

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

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

travail systèmes de contrainte en mettant en œuvre des algorithmes de la théorie des nombres, l'algèbre linéaire, analyse, etc .. selon sur le domaine qu'ils modélisent, c'est-à-dire ce que * désigne dans la notation CLP (*). Ces algorithmes peuvent aller aussi loin que quantifier elimination.

Au revoir